MathlibAnnex/LinearAlgebra/Projectivization/Dimension.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6import MathlibAnnex.LinearAlgebra.Projectivization.SubspaceEquiv7import Mathlib.LinearAlgebra.Projectivization.Independence8import Mathlib.LinearAlgebra.Basis.Basic9import Mathlib.LinearAlgebra.Dimension.Free10import Mathlib.RingTheory.Finiteness.Basic1112/-!13# Generation, independence and dimension under projective incidence1415The order map is the one already constructed from the given projective point16bijection. Independence is transported through Mathlib's lattice-theoretic17criterion. A basis is then transported by choosing representatives of its image18points and proving both independence and spanning. This does NOT construct a19semilinear realization of the point map.2021Finite generation is proved by induction on finite algebraic generation, not22by silently replacing arbitrary submodules by closed ones. Finite dimensionality23is explicit whenever `finrank` is interpreted as a dimension.24-/2526set_option autoImplicit false27noncomputable section28open Set29open scoped LinearAlgebra.Projectivization3031namespace Projectivization3233universe uK uL uV uW uI34variable {K : Type uK} {L : Type uL} {V : Type uV} {W : Type uW}35variable [DivisionRing K] [DivisionRing L]36variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module L W]37variable (e : ℙ K V ≃ ℙ L W)38variable (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,39  p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))4041include he in42/-- Independence of arbitrary indexed families, hence also of finite families,43is preserved and reflected by finite-span incidence. -/44theorem independent_comp_iff_of_finite_span {ι : Type uI} (p : ι → ℙ K V) :45    Independent (e ∘ p) ↔ Independent p := by46  rw [independent_iff_iSupIndep, independent_iff_iSupIndep]47  have hf : (fun i => (e (p i)).submodule) =48      submoduleOrderIsoOfFiniteSpan e he ∘ (fun i => (p i).submodule) := by49    funext i50    exact (submoduleOrderIsoOfFiniteSpan_submodule e he (p i)).symm51  change iSupIndep (fun i => (e (p i)).submodule) ↔ _52  rw [hf]53  exact iSupIndep_map_orderIso_iff (submoduleOrderIsoOfFiniteSpan e he)5455include he in56/-- The same independence statement on Mathlib's nonzero representatives. -/57theorem linearIndependent_rep_comp_iff_of_finite_span {ι : Type uI}58    (p : ι → ℙ K V) :59    LinearIndependent L (fun i => (e (p i)).rep) ↔60      LinearIndependent K (fun i => (p i).rep) := by61  simpa only [independent_iff, Function.comp_def] using62    independent_comp_iff_of_finite_span e he p6364/-- Finite generation of a submodule is preserved. The proof treats a zero65new generator separately and otherwise uses the actual image projective line. -/66theorem fg_submoduleOrderIsoOfFiniteSpan (P : Submodule K V) (hP : P.FG) :67    (submoduleOrderIsoOfFiniteSpan e he P).FG := by68  refine Submodule.fg_sup_span_induction69    (motive := fun Q _ => (submoduleOrderIsoOfFiniteSpan e he Q).FG) ?_ ?_ P hP70  · simpa only [submoduleOrderIsoOfFiniteSpan_bot] using71      (Submodule.fg_bot : (⊥ : Submodule L W).FG)72  · intro Q v hQ ih73    rw [submoduleOrderIsoOfFiniteSpan_sup]74    apply ih.sup75    by_cases hv : v = 076    · subst v77      simpa using (Submodule.fg_bot : (⊥ : Submodule L W).FG)78    · rw [submoduleOrderIsoOfFiniteSpan_span_singleton e he v hv, submodule_eq]79      exact Submodule.fg_span_singleton _8081/-- Finite generation is also reflected; the map here acts on all submodules. -/82theorem fg_submoduleOrderIsoOfFiniteSpan_iff (P : Submodule K V) :83    (submoduleOrderIsoOfFiniteSpan e he P).FG ↔ P.FG := by84  refine ⟨?_, fg_submoduleOrderIsoOfFiniteSpan e he P⟩85  intro hP86  have h := fg_submoduleOrderIsoOfFiniteSpan e.symm87    (Subspace.finite_span_symm_iff e he) (submoduleOrderIsoOfFiniteSpan e he P) hP88  rw [← submoduleOrderIsoOfFiniteSpan_symm e he,89    symm_apply_submoduleOrderIsoOfFiniteSpan] at h90  exact h9192/-- The points determined by any algebraic basis span the whole projective space.93The empty basis of a zero module is included. -/94theorem span_range_mk_basis_eq_top {ι : Type uI} (b : Module.Basis ι K V) :95    Subspace.span (range fun i => mk K (b i) (b.ne_zero i)) = ⊤ := by96  apply Subspace.submodule.injective97  rw [Subspace.submodule.map_top]98  apply top_unique99  rw [← b.span_eq]100  apply Submodule.span_le.mpr101  rintro _ ⟨i, rfl⟩102  exact (Subspace.mem_submodule_iff _ (b.ne_zero i)).mpr103    (Subspace.subset_span _ (mem_range_self i))104105include he in106/-- Representatives of the image of a projective spanning family span the107whole target vector space. No assumption on either dimension is made. -/108theorem span_range_rep_comp_eq_top_of_finite_span {ι : Type uI}109    (p : ι → ℙ K V) (hp : Subspace.span (range p) = ⊤) :110    Submodule.span L (range fun i => (e (p i)).rep) = ⊤ := by111  have hspan : Subspace.span (e '' range p) = ⊤ := by112    rw [← Subspace.orderIsoOfFiniteSpan_span e he, hp]113    exact (Subspace.orderIsoOfFiniteSpan e he).map_top114  have hrange : Projectivization.rep '' (e '' range p) =115      range (fun i => (e (p i)).rep) := by116    ext w117    constructor118    · rintro ⟨q, ⟨r, ⟨i, rfl⟩, rfl⟩, rfl⟩119      exact ⟨i, rfl⟩120    · rintro ⟨i, rfl⟩121      exact ⟨e (p i), ⟨p i, mem_range_self i, rfl⟩, rfl⟩122  rw [← hrange, ← Subspace.submodule_span_eq_span_rep_image, hspan,123    Subspace.submodule.map_top]124125/-- A basis of the source gives an actual basis of the target with the same126index type. This is a choice of image representatives, not a semilinear lift. -/127def basisOfFiniteSpan {ι : Type uI} (b : Module.Basis ι K V) : Module.Basis ι L W := by128  let p : ι → ℙ K V := fun i => mk K (b i) (b.ne_zero i)129  have hp : Independent p := Independent.mk b b.ne_zero b.linearIndependent130  have heP : Independent (e ∘ p) :=131    (independent_comp_iff_of_finite_span e he p).mpr hp132  have hlin : LinearIndependent L (fun i => (e (p i)).rep) :=133    independent_iff.mp heP134  have hspan : Submodule.span L (range fun i => (e (p i)).rep) = ⊤ :=135    span_range_rep_comp_eq_top_of_finite_span e he p (span_range_mk_basis_eq_top b)136  exact Module.Basis.mk hlin hspan.ge137138/-- The transported basis has exactly the chosen representative at each index. -/139@[simp]140theorem basisOfFiniteSpan_apply {ι : Type uI} (b : Module.Basis ι K V) (i : ι) :141    basisOfFiniteSpan e he b i = (e (mk K (b i) (b.ne_zero i))).rep := by142  unfold basisOfFiniteSpan143  rw [Module.Basis.mk_apply]144145/-- The basis realizes the given projective images on its basis vectors only. -/146@[simp]147theorem mk_basisOfFiniteSpan {ι : Type uI} (b : Module.Basis ι K V) (i : ι) :148    mk L (basisOfFiniteSpan e he b i) ((basisOfFiniteSpan e he b).ne_zero i) =149      e (mk K (b i) (b.ne_zero i)) := by150  simpa only [basisOfFiniteSpan_apply] using151    (mk_rep (e (mk K (b i) (b.ne_zero i))))152153include e he in154/-- If the source is finite dimensional, the target really is finite dimensional. -/155theorem finite_of_finite_span [Module.Finite K V] : Module.Finite L W :=156  Module.Finite.of_basis (basisOfFiniteSpan e he (Module.finBasis K V))157158include e he in159/-- Finite dimensionality is equivalent, including the zero-dimensional case. -/160theorem finite_iff_of_finite_span : Module.Finite K V ↔ Module.Finite L W := by161  constructor162  · intro hV163    letI : Module.Finite K V := hV164    exact finite_of_finite_span e he165  · intro hW166    letI : Module.Finite L W := hW167    exact finite_of_finite_span e.symm (Subspace.finite_span_symm_iff e he)168169include e he in170/-- Dimension equality with an actual finite-dimensional hypothesis. In an171infinite-dimensional space `finrank = 0` is not used to infer triviality. -/172theorem finrank_eq_of_finite_span [Module.Finite K V] :173    Module.finrank K V = Module.finrank L W := by174  have h := Module.finrank_eq_card_basis175    (basisOfFiniteSpan e he (Module.finBasis K V))176  simpa only [Fintype.card_fin] using h.symm177178include e he in179/-- Either finite-dimensionality hypothesis suffices, without privileging a side. -/180theorem finite_and_finrank_eq_of_finite_span181    (hfinite : Module.Finite K V ∨ Module.Finite L W) :182    Module.Finite K V ∧ Module.Finite L W ∧183      Module.finrank K V = Module.finrank L W := by184  have hV : Module.Finite K V := hfinite.elim id (finite_iff_of_finite_span e he).mpr185  letI : Module.Finite K V := hV186  exact ⟨hV, finite_of_finite_span e he, finrank_eq_of_finite_span e he⟩187188end Projectivization