Matroid.ForMathlib.LinearAlgebra.Projective

source

theorem Projectivization.mk_apply_rep {K : Type u_4} {L : Type u_5} {V : Type u_6} {W : Type u_7} [DivisionRing K] [AddCommGroup V] [Module K V] [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) (x : Projectivization K V) :

mk L (f x.rep) ⋯ = map f hf x

source

def Projectivization.mapEquiv {K : Type u_4} {L : Type u_5} {V : Type u_6} {W : Type u_7} [DivisionRing K] [AddCommGroup V] [Module K V] [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] [RingHomInvPair τ σ] (f : V ≃ₛₗ[σ] W) :

Projectivization K V ≃ Projectivization L W

Equations

Projectivization.mapEquiv f = { toFun := Projectivization.map ↑f ⋯, invFun := Projectivization.map ↑f.symm ⋯, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem Projectivization.mapEquiv_symm_apply {K : Type u_4} {L : Type u_5} {V : Type u_6} {W : Type u_7} [DivisionRing K] [AddCommGroup V] [Module K V] [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] [RingHomInvPair τ σ] (f : V ≃ₛₗ[σ] W) (a✝ : Projectivization L W) :

(mapEquiv f).symm a✝ = map ↑f.symm ⋯ a✝

source

@[simp]

theorem Projectivization.mapEquiv_apply {K : Type u_4} {L : Type u_5} {V : Type u_6} {W : Type u_7} [DivisionRing K] [AddCommGroup V] [Module K V] [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] [RingHomInvPair τ σ] (f : V ≃ₛₗ[σ] W) (a✝ : Projectivization K V) :

(mapEquiv f) a✝ = map ↑f ⋯ a✝

source

@[simp]

theorem Projectivization.mapEquiv_symm {K : Type u_4} {L : Type u_5} {V : Type u_6} {W : Type u_7} [DivisionRing K] [AddCommGroup V] [Module K V] [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] [RingHomInvPair τ σ] (f : V ≃ₛₗ[σ] W) :

(mapEquiv f).symm = mapEquiv f.symm

source

@[simp]

theorem Projectivization.mapEquiv_mk {K : Type u_4} {L : Type u_5} {V : Type u_6} {W : Type u_7} [DivisionRing K] [AddCommGroup V] [Module K V] [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] [RingHomInvPair τ σ] (f : V ≃ₛₗ[σ] W) (x : V) (hx : x ≠ 0) :

(mapEquiv f) (mk K x hx) = mk L (f x) ⋯

source

@[simp]

theorem Projectivization.mapEquiv_symm_mapEquiv {K : Type u_4} {L : Type u_5} {V : Type u_6} {W : Type u_7} [Field K] [AddCommGroup V] [Module K V] [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] [RingHomInvPair τ σ] (f : V ≃ₛₗ[σ] W) (x : Projectivization K V) :

(mapEquiv f.symm) ((mapEquiv f) x) = x

source

@[simp]

theorem Projectivization.mapEquiv_mapEquiv_symm {K : Type u_4} {L : Type u_5} {V : Type u_6} {W : Type u_7} [DivisionRing K] [AddCommGroup V] [Module K V] [Field L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] [RingHomInvPair τ σ] (f : V ≃ₛₗ[σ] W) (x : Projectivization L W) :

(mapEquiv f) ((mapEquiv f.symm) x) = x

source

@[simp]

theorem Projectivization.mapEquiv_mk_symm_mk {K : Type u_4} {L : Type u_5} {V : Type u_6} {W : Type u_7} [Field K] [AddCommGroup V] [Module K V] [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] [RingHomInvPair τ σ] (f : V ≃ₛₗ[σ] W) (x : Projectivization K V) :

mk K (f.symm ((mapEquiv f) x).rep) ⋯ = x

source

@[simp]

theorem Projectivization.independent_comp_mk_iff {ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] (f : ι → V) (hf0 : ∀ (i : ι), f i ≠ 0) :

(Independent fun (i : ι) => mk K (f i) ⋯) ↔ LinearIndependent K f

source

theorem Projectivization.Independent.linearIndependent {ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {f : ι → V} {hf0 : ∀ (i : ι), f i ≠ 0} (h : Independent fun (i : ι) => Projectivization.mk K (f i) ⋯) :

LinearIndependent K f

source

theorem LinearIndependent.independent_comp_mk {ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {f : ι → V} (h : LinearIndependent K f) :

Projectivization.Independent fun (i : ι) => Projectivization.mk K (f i) ⋯

source

theorem Projectivization.mapEquiv_indep_iff {ι : Type u_1} {V : Type u_3} [AddCommGroup V] {W : Type u_4} {K : Type u_5} [Field K] [Module K V] [AddCommGroup W] [Module K W] (f : V ≃ₗ[K] W) (v : ι → Projectivization K V) :

Independent (⇑(mapEquiv f) ∘ v) ↔ Independent v

source

@[simp]

theorem Projectivization.independent_subsingleton {ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] [Subsingleton ι] (f : ι → Projectivization K V) :

Independent f

source

theorem Projectivization.independent_equiv {ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {ι' : Type u_4} (e : ι ≃ ι') {f : ι' → Projectivization K V} :

Independent (f ∘ ⇑e) ↔ Independent f

source

theorem Projectivization.independent_equiv' {ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {ι' : Type u_4} (e : ι ≃ ι') {f : ι' → Projectivization K V} {g : ι → Projectivization K V} (h_eq : f ∘ ⇑e = g) :

Independent g ↔ Independent f

source

theorem Projectivization.Independent.comp {ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {ι' : Type u_4} {v : ι → Projectivization K V} (hv : Independent v) (f : ι' → ι) (hf : Function.Injective f) :

Independent (v ∘ f)

source

@[simp]

theorem Projectivization.mk_smul_eq {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {u : V} (hu : u ≠ 0) (c : Kˣ) :

mk K (c • u) ⋯ = mk K u hu

source

theorem Projectivization.mk_smul_eq' {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {u : V} (hu : u ≠ 0) {c : K} (hc : c ≠ 0) :

mk K (c • u) ⋯ = mk K u hu

source

theorem Projectivization.exists_smul_mk_rep_eq (K : Type u_4) {V : Type u_5} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v ≠ 0) :

∃ (c : Kˣ), c • (mk K v hv).rep = v

source

theorem Projectivization.mem_submodule_iff' (K : Type u_4) {V : Type u_5} [DivisionRing K] [AddCommGroup V] [Module K V] {v : V} {w : Projectivization K V} (hv : v ≠ 0) :

v ∈ w.submodule ↔ mk K v hv = w

source

@[simp]

theorem Submodule.mk_rep_mem_iff_mem (K : Type u_4) {V : Type u_5} [DivisionRing K] [AddCommGroup V] [Module K V] {W : Submodule K V} {v : V} (hv : v ≠ 0) :

(Projectivization.mk K v hv).rep ∈ W ↔ v ∈ W

source

@[simp]

theorem Projectivization.independent_pair {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {u v : Projectivization K V} :

Independent fun (x : ↑{u, v}) => ↑x

source

@[simp]

theorem Projectivization.submodule_span_range_rep (K : Type u_4) (W : Type u_5) [DivisionRing K] [AddCommGroup W] [Module K W] :

Submodule.span K (Set.range Projectivization.rep) = ⊤

source

theorem Projectivization.Subspace.mem_span_iff_rep (K : Type u_7) {V : Type u_8} [Field K] [AddCommGroup V] [Module K V] (s : Set (Projectivization K V)) (b : Projectivization K V) :

b ∈ span s ↔ b.rep ∈ Submodule.span K (Projectivization.rep '' s)

source

theorem Projectivization.Subspace.mem_span_image_rep_iff (K : Type u_7) {V : Type u_8} [Field K] [AddCommGroup V] [Module K V] (s : Set (Projectivization K V)) {a : V} (ha : a ≠ 0) :

a ∈ Submodule.span K (Projectivization.rep '' s) ↔ Projectivization.mk K a ha ∈ span s

source

theorem Projectivization.Subspace.rep_mem_span_image_iff (K : Type u_7) {V : Type u_8} {ι : Type u_9} [Field K] [AddCommGroup V] [Module K V] {f : ι → Projectivization K V} (s : Set ι) {x : Projectivization K V} :

x.rep ∈ Submodule.span K (Projectivization.rep ∘ f '' s) ↔ x ∈ span (f '' s)

source

theorem Projectivization.Subspace.mem_span_image_iff (K : Type u_7) {V : Type u_8} {ι : Type u_9} [Field K] [AddCommGroup V] [Module K V] {f : ι → V} {hf : ∀ (i : ι), f i ≠ 0} (s : Set ι) {x : Projectivization K V} :

x ∈ span ((fun (i : ι) => Projectivization.mk K (f i) ⋯) '' s) ↔ x.rep ∈ Submodule.span K (f '' s)

source

noncomputable def Submodule.toProjSubspace {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (W : Submodule K V) :

Projectivization.Subspace K V

The projective subspace corresponding to a given submodule

Equations

W.toProjSubspace = { carrier := Projectivization.rep ⁻¹' ↑W, mem_add' := ⋯ }

Instances For

source

@[simp]

theorem Submodule.mem_toProjSubspace_iff {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (W : Submodule K V) (x : Projectivization K V) :

x ∈ W.toProjSubspace ↔ x.rep ∈ W

source

theorem Submodule.toProjSubspace_span_image_eq (K : Type u_7) {V : Type u_8} {ι : Type u_9} [Field K] [AddCommGroup V] [Module K V] {f : ι → V} {hf : ∀ (i : ι), f i ≠ 0} (s : Set ι) :

(span K (f '' s)).toProjSubspace = Projectivization.Subspace.span ((fun (i : ι) => Projectivization.mk K (f i) ⋯) '' s)

source

noncomputable def Projectivization.Subspace.toSubmodule {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :

Submodule K V

Equations

W.toSubmodule = Submodule.span K (Projectivization.rep '' ↑W)

Instances For

source

theorem Projectivization.Subspace.toSubmodule_coeSet_eq {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :

↑W.toSubmodule = insert 0 (⋃ x ∈ W, ↑x.submodule)

The submodule corresponding to a given projective subspace

source

theorem Projectivization.Subspace.mem_toSubmodule_iff {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) (x : V) :

x ∈ W.toSubmodule ↔ x = 0 ∨ ∃ (hx : x ≠ 0), Projectivization.mk K x hx ∈ W

source

theorem Projectivization.Subspace.toSubmodule_eq_span {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :

W.toSubmodule = Submodule.span K (Projectivization.rep '' ↑W)

source

@[simp]

theorem Submodule.toProjSubspace_toSubmodule {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (W : Submodule K V) :

W.toProjSubspace.toSubmodule = W

source

@[simp]

theorem Projectivization.toSubmodule_toProjSubspace {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :

W.toSubmodule.toProjSubspace = W

source

noncomputable def Projectivization.subspace_orderIso_submodule (K : Type u_7) (V : Type u_8) [Field K] [AddCommGroup V] [Module K V] :

Subspace K V ≃o Submodule K V

The natural isomorphism between the projective subspace lattice and the subspace lattice.

Equations

Projectivization.subspace_orderIso_submodule K V = { toFun := Projectivization.Subspace.toSubmodule, invFun := Submodule.toProjSubspace, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

Instances For

source

@[simp]

theorem Projectivization.subspace_orderIso_submodule_apply (K : Type u_7) (V : Type u_8) [Field K] [AddCommGroup V] [Module K V] (W : Subspace K V) :

(subspace_orderIso_submodule K V) W = W.toSubmodule

source

@[simp]

theorem Projectivization.subspace_orderIso_submodule_symm_apply (K : Type u_7) (V : Type u_8) [Field K] [AddCommGroup V] [Module K V] (W : Submodule K V) :

(RelIso.symm (subspace_orderIso_submodule K V)) W = W.toProjSubspace

source

@[simp]

theorem Submodule.toProjSubspace_top_eq (K : Type u_7) (V : Type u_8) [Field K] [AddCommGroup V] [Module K V] :

⊤.toProjSubspace = ⊤

source

@[simp]

theorem Projectivization.Subspace.toSubmodule_top_eq (K : Type u_7) (V : Type u_8) [Field K] [AddCommGroup V] [Module K V] :

⊤.toSubmodule = ⊤

source

@[simp]

theorem Submodule.toProjSubspace_eq_top_iff {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] {W : Submodule K V} :

W.toProjSubspace = ⊤ ↔ W = ⊤

source

@[simp]

theorem Projectization.Subspace.toSubmodule_eq_top_iff {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] {W : Projectivization.Subspace K V} :

W.toSubmodule = ⊤ ↔ W = ⊤

source

@[simp]

theorem Submodule.toProjSubspace_bot_eq (K : Type u_7) (V : Type u_8) [Field K] [AddCommGroup V] [Module K V] :

⊥.toProjSubspace = ⊥

source

@[simp]

theorem Projectivization.Subspace.toSubmodule_bot_eq (K : Type u_7) (V : Type u_8) [Field K] [AddCommGroup V] [Module K V] :

⊥.toSubmodule = ⊥

source

@[simp]

theorem Submodule.toProjSubspace_eq_bot_iff {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] {W : Submodule K V} :

W.toProjSubspace = ⊥ ↔ W = ⊥

source

@[simp]

theorem Projectization.Subspace.toSubmodule_eq_bot_iff {K : Type u_5} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] {W : Projectivization.Subspace K V} :

W.toSubmodule = ⊥ ↔ W = ⊥

source

theorem Submodule.span_toProjSubspace (K : Type u_7) {V : Type u_8} [Field K] [AddCommGroup V] [Module K V] (s : Set V) :

(span K s).toProjSubspace = Projectivization.Subspace.span (Set.range fun (x : ↑(s \ {0})) => Projectivization.mk K ↑x ⋯)

source

theorem Projectivization.Subspace.span_toSubmodule {K : Type u_7} {V : Type u_8} [Field K] [AddCommGroup V] [Module K V] (s : Set (Projectivization K V)) :

(span s).toSubmodule = Submodule.span K (Projectivization.rep '' s)