MathlibAnnex/LinearAlgebra/Projectivization/Semilinear.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.CoordinateLift7import MathlibAnnex.LinearAlgebra.Basis.Semilinear8import Mathlib.LinearAlgebra.Finsupp.Defs9import Mathlib.SetTheory.Cardinal.Order10import Mathlib.Tactic.Abel11import Mathlib.Tactic.FieldSimp12import Mathlib.Tactic.Ring1314/-!15# Semilinear realization from finite projective incidence1617The normalized pencil equivalences are synchronized by three-coordinate18incidence. Multiplication and the identity `σ (1 - t) = 1 - σ t` are then derived19from actual subspace transport; together with bijectivity these imply addition.20No scalar regularity or linear realization of the point map is assumed.2122The resulting scalar ring isomorphism acts on finitely supported basis23coefficients to construct a semilinear equivalence. Affine-chart agreement is24proved coordinate by coordinate; the anchor-zero case is proved separately by25intersecting a two-dimensional span with the coordinate hyperplane. The final26existence theorem assumes only algebraic rank at least three, over fields.27The imported DivisionRing results are unchanged; this new coordinate realization28does not assert the noncommutative DivisionRing extension.29-/3031set_option autoImplicit false32noncomputable section33open Set34open scoped LinearAlgebra.Projectivization3536namespace Projectivization3738universe uK uL uV uW uI39variable {K : Type uK} {L : Type uL} {V : Type uV} {W : Type uW}40variable [Field K] [Field L]41variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module L W]42variable {ι : Type uI}4344local instance (σ : K ≃+* L) : RingHomInvPair σ.toRingHom σ.symm.toRingHom :=45  RingHomInvPair.of_ringEquiv σ46local instance (σ : K ≃+* L) : RingHomInvPair σ.symm.toRingHom σ.toRingHom :=47  RingHomInvPair.of_ringEquiv_symm σ4849/-- The affine coordinate plane has nonzero anchor coordinate, including when50one or both variable coefficients are zero. -/51theorem basis_add_smul_add_smul_ne_zero (b : Module.Basis ι K V)52    (o i j : ι) (hoi : o ≠ i) (hoj : o ≠ j) (a d : K) :53    b o + a • b i + d • b j ≠ 0 := by54  intro h55  have hc := congrArg (fun v : V => b.repr v o) h56  simpa [hoi, hoj, hoi.symm, hoj.symm] using hc5758/-- A point in the actual three-coordinate projective plane. -/59def basisPlanePoint (b : Module.Basis ι K V)60    (o i j : ι) (hoi : o ≠ i) (hoj : o ≠ j) (a d : K) : ℙ K V :=61  mk K (b o + a • b i + d • b j)62    (basis_add_smul_add_smul_ne_zero b o i j hoi hoj a d)6364section ScalarRigidity6566variable (e : ℙ K V ≃ ℙ L W)67variable (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,68  p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))69variable (b : Module.Basis ι K V) (c : Module.Basis ι L W)70variable (hbc : ∀ i, e (mk K (b i) (b.ne_zero i)) = mk L (c i) (c.ne_zero i))71include he hbc7273/-- The two variable coordinates of a normalized image are read from the two74anchor pencils, without assuming those two scalar maps agree. -/75theorem repr_coordinateRepresentative_image_basisPlanePoint76    (o i j : ι) (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j) (a d : K) :77    c.repr (coordinateRepresentative c o (e (basisPlanePoint b o i j hoi hoj a d))) i =78        pencilScalar e b c o i hoi a ∧79      c.repr (coordinateRepresentative c o (e (basisPlanePoint b o i j hoi hoj a d))) j =80        pencilScalar e b c o j hoj d := by81  have hv := basis_add_smul_add_smul_ne_zero b o i j hoi hoj a d82  have ho : b.repr (b o + a • b i + d • b j) o = 1 := by83    simp [hoi, hoj, hoi.symm, hoj.symm]84  constructor85  · simpa [basisPlanePoint, hoi, hoj, hij, hoi.symm, hoj.symm, hij.symm] using86      repr_coordinateRepresentative_image e he b c hbc o i hoi _ hv ho87  · simpa [basisPlanePoint, hoi, hoj, hij, hoi.symm, hoj.symm, hij.symm] using88      repr_coordinateRepresentative_image e he b c hbc o j hoj _ hv ho8990variable (o : ι)91variable (h1 : ∀ i (hoi : o ≠ i), pencilScalar e b c o i hoi 1 = 1)92include h19394/-- A pencil between two nonanchor axes has the same parameter map as the95anchor pencil ending at its second axis. A point with first coordinate one96provides the equality of parameters. -/97theorem pencilScalar_eq_anchor (i j : ι)98    (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j) (a : K) :99    pencilScalar e b c i j hij a = pencilScalar e b c o j hoj a := by100  have hv := basis_add_smul_add_smul_ne_zero b o i j hoi hoj 1 a101  have hvP : b o + (1 : K) • b i + a • b j ∈ coordinateHyperplane b i j a := by102    rw [mem_coordinateHyperplane_iff]103    simp [hoi, hoj, hij, hoi.symm, hoj.symm, hij.symm]104  have hP := coordinateRepresentative_image_mem_coordinateHyperplane e he b c hbc105    o i j hij a _ hv hvP106  rw [mem_coordinateHyperplane_iff] at hP107  have hc := repr_coordinateRepresentative_image_basisPlanePoint e he b c hbc108    o i j hoi hoj hij 1 a109  change c.repr (coordinateRepresentative c o110      (e (basisPlanePoint b o i j hoi hoj 1 a))) j =111    pencilScalar e b c i j hij a * c.repr (coordinateRepresentative c o112      (e (basisPlanePoint b o i j hoi hoj 1 a))) i at hP113  rw [hc.1, hc.2, h1 i hoi, mul_one] at hP114  exact hP.symm115116/-- All normalized anchor pencils agree pairwise. Distinctness is required only117for the three axes used in this proof, not for the ambient basis as a finite set. -/118theorem pencilScalar_eq_of_normalized (i j : ι)119    (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j) (a : K) :120    pencilScalar e b c o i hoi a = pencilScalar e b c o j hoj a := by121  have hv := basis_add_smul_add_smul_ne_zero b o i j hoi hoj a a122  have hvP : b o + a • b i + a • b j ∈ coordinateHyperplane b i j 1 := by123    rw [mem_coordinateHyperplane_iff]124    simp [hoi, hoj, hij, hoi.symm, hoj.symm, hij.symm]125  have hP := coordinateRepresentative_image_mem_coordinateHyperplane e he b c hbc126    o i j hij 1 _ hv hvP127  rw [mem_coordinateHyperplane_iff] at hP128  have hc := repr_coordinateRepresentative_image_basisPlanePoint e he b c hbc129    o i j hoi hoj hij a a130  change c.repr (coordinateRepresentative c o131      (e (basisPlanePoint b o i j hoi hoj a a))) j =132    pencilScalar e b c i j hij 1 * c.repr (coordinateRepresentative c o133      (e (basisPlanePoint b o i j hoi hoj a a))) i at hP134  rw [hc.1, hc.2, pencilScalar_eq_anchor e he b c hbc o h1 i j hoi hoj hij,135    h1 j hoj, one_mul] at hP136  exact hP.symm137138/-- Multiplication comes from the homogeneous equation `v_j = a v_i` in an139actual three-coordinate plane. No multiplication law is supplied as an input. -/140theorem pencilScalar_mul_of_normalized (i j : ι)141    (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j) (a t : K) :142    pencilScalar e b c o j hoj (a * t) =143      pencilScalar e b c o j hoj a * pencilScalar e b c o j hoj t := by144  have hv := basis_add_smul_add_smul_ne_zero b o i j hoi hoj t (a * t)145  have hvP : b o + t • b i + (a * t) • b j ∈ coordinateHyperplane b i j a := by146    rw [mem_coordinateHyperplane_iff]147    simp [hoi, hoj, hij, hoi.symm, hoj.symm, hij.symm]148  have hP := coordinateRepresentative_image_mem_coordinateHyperplane e he b c hbc149    o i j hij a _ hv hvP150  rw [mem_coordinateHyperplane_iff] at hP151  have hc := repr_coordinateRepresentative_image_basisPlanePoint e he b c hbc152    o i j hoi hoj hij t (a * t)153  change c.repr (coordinateRepresentative c o154      (e (basisPlanePoint b o i j hoi hoj t (a * t)))) j =155    pencilScalar e b c i j hij a * c.repr (coordinateRepresentative c o156      (e (basisPlanePoint b o i j hoi hoj t (a * t)))) i at hP157  rw [hc.1, hc.2, pencilScalar_eq_anchor e he b c hbc o h1 i j hoi hoj hij,158    pencilScalar_eq_of_normalized e he b c hbc o h1 i j hoi hoj hij] at hP159  exact hP160161/-- The affine line joining the normalized unit points gives preservation of162`1 - t`. Its target equation is derived from two actual image lines. -/163theorem pencilScalar_one_sub_of_normalized (i j : ι)164    (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j) (t : K) :165    pencilScalar e b c o j hoj (1 - t) = 1 - pencilScalar e b c o j hoj t := by166  let x := b o + b i167  let y := b o + b j168  let v := b o + t • b i + (1 - t) • b j169  have hx : x ≠ 0 := by simpa [x] using basis_add_smul_ne_zero b o i hoi (1 : K)170  have hy : y ≠ 0 := by simpa [y] using basis_add_smul_ne_zero b o j hoj (1 : K)171  have hv : v ≠ 0 := basis_add_smul_add_smul_ne_zero b o i j hoi hoj t (1 - t)172  let P : Submodule K V := (K ∙ x) ⊔ (K ∙ y)173  have hxP : x ∈ P := (show K ∙ x ≤ P from le_sup_left) (Submodule.mem_span_singleton_self x)174  have hyP : y ∈ P := (show K ∙ y ≤ P from le_sup_right) (Submodule.mem_span_singleton_self y)175  have hvP : v ∈ P := by176    have hs := P.add_mem (P.smul_mem t hxP) (P.smul_mem (1 - t) hyP)177    have heq : t • x + (1 - t) • y = v := by178      dsimp [x, y, v]179      simp only [smul_add, sub_smul, one_smul]180      abel181    exact heq ▸ hs182  have hpx : mk K x hx = basisPencilPoint b o i hoi 1 := by simp [x, basisPencilPoint]183  have hpy : mk K y hy = basisPencilPoint b o j hoj 1 := by simp [y, basisPencilPoint]184  have hmap : submoduleOrderIsoOfFiniteSpan e he P =185      (L ∙ (c o + c i)) ⊔ (L ∙ (c o + c j)) := by186    dsimp [P]187    rw [submoduleOrderIsoOfFiniteSpan_sup,188      submoduleOrderIsoOfFiniteSpan_span_singleton e he x hx,189      submoduleOrderIsoOfFiniteSpan_span_singleton e he y hy,190      hpx, hpy, image_basisPencilPoint e he b c hbc,191      image_basisPencilPoint e he b c hbc, h1 i hoi, h1 j hoj]192    simp only [basisPencilPoint, submodule_mk, one_smul]193  let M : Submodule L W := LinearMap.ker (c.coord i + c.coord j - c.coord o)194  have hPM : submoduleOrderIsoOfFiniteSpan e he P ≤ M := by195    rw [hmap]196    apply sup_le197    · apply (Submodule.span_singleton_le_iff_mem _ _).mpr198      change c.repr (c o + c i) i + c.repr (c o + c i) j - c.repr (c o + c i) o = 0199      simp [hoi, hoj, hij, hoi.symm, hoj.symm, hij.symm]200    · apply (Submodule.span_singleton_le_iff_mem _ _).mpr201      change c.repr (c o + c j) i + c.repr (c o + c j) j - c.repr (c o + c j) o = 0202      simp [hoi, hoj, hij, hoi.symm, hoj.symm, hij.symm]203  have hwP : (e (mk K v hv)).rep ∈ submoduleOrderIsoOfFiniteSpan e he P := by204    rw [mem_submoduleOrderIsoOfFiniteSpan_iff e he _ _ (rep_nonzero _),205      mk_rep, e.symm_apply_apply, Submodule.mk_mem_projectivization_iff]206    exact hvP207  have hw := hPM ((submoduleOrderIsoOfFiniteSpan e he P).smul_mem208    ((c.repr (e (mk K v hv)).rep o)⁻¹) hwP)209  change c.repr (coordinateRepresentative c o (e (mk K v hv))) i +210    c.repr (coordinateRepresentative c o (e (mk K v hv))) j -211    c.repr (coordinateRepresentative c o (e (mk K v hv))) o = 0 at hw212  have ho : c.repr (e (mk K v hv)).rep o ≠ 0 := by213    intro hz214    have hz' := (repr_image_rep_eq_zero_iff e he b c hbc v hv o).mp hz215    simpa [v, hoi, hoj, hoi.symm, hoj.symm] using hz'216  have hc := repr_coordinateRepresentative_image_basisPlanePoint e he b c hbc217    o i j hoi hoj hij t (1 - t)218  change c.repr (coordinateRepresentative c o (e (mk K v hv))) i = _ ∧219    c.repr (coordinateRepresentative c o (e (mk K v hv))) j = _ at hc220  rw [hc.1, hc.2, repr_coordinateRepresentative_self c o _ ho,221    pencilScalar_eq_of_normalized e he b c hbc o h1 i j hoi hoj hij] at hw222  apply eq_sub_iff_add_eq.mpr223  simpa only [add_comm] using (sub_eq_zero.mp hw)224225omit he hbc h1 in226private theorem add_of_mul_one_sub (s : K ≃ L)227    (h0 : s 0 = 0) (h1s : s 1 = 1)228    (hm : ∀ a d, s (a * d) = s a * s d)229    (hs : ∀ a, s (1 - a) = 1 - s a) :230    ∀ a d, s (a + d) = s a + s d := by231  have hne : ∀ a d, a + d ≠ 0 → s (a + d) = s a + s d := by232    intro a d had233    have ha : (a + d) * (a / (a + d)) = a := by field_simp [had] <;> ring234    have hd : (a + d) * (1 - a / (a + d)) = d := by field_simp [had] <;> ring235    calc236      s (a + d) = s (a + d) * s (a / (a + d)) +237          s (a + d) * s (1 - a / (a + d)) := by rw [hs]; ring238      _ = s ((a + d) * (a / (a + d))) +239          s ((a + d) * (1 - a / (a + d))) := by rw [hm, hm]240      _ = s a + s d := by rw [ha, hd]241  intro a d242  by_cases had : a + d = 0243  · obtain ⟨z, hz⟩ := s.surjective (-s a)244    have haz : a + z = 0 := by245      by_contra hn246      have hsaz := hne a z hn247      have heq : s (a + z) = s 0 := by simpa only [hz, add_neg_cancel, h0] using hsaz248      exact hn (s.injective heq)249    have hdz : d = z := add_left_cancel (had.trans haz.symm)250    rw [had, h0, hdz, hz, add_neg_cancel]251  · exact hne a d had252253/-- Addition is a consequence of three-coordinate incidence and the already254proved bijection/multiplication/complement laws, in every characteristic. -/255theorem pencilScalar_add_of_normalized (i j : ι)256    (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j) (a d : K) :257    pencilScalar e b c o j hoj (a + d) =258      pencilScalar e b c o j hoj a + pencilScalar e b c o j hoj d := by259  exact add_of_mul_one_sub (pencilEquiv e he b c hbc o j hoj)260    (pencilScalar_zero e he b c hbc o j hoj) (h1 j hoj)261    (pencilScalar_mul_of_normalized e he b c hbc o h1 i j hoi hoj hij)262    (pencilScalar_one_sub_of_normalized e he b c hbc o h1 i j hoi hoj hij) a d263264/-- The actual scalar isomorphism read from the given projective equivalence.265The only geometric hypotheses beyond finite incidence are the three distinct266axes and a target basis whose anchor pencils have been normalized. -/267def scalarRingEquiv (i j : ι) (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j) : K ≃+* L :=268  { pencilEquiv e he b c hbc o j hoj with269    map_mul' := pencilScalar_mul_of_normalized e he b c hbc o h1 i j hoi hoj hij270    map_add' := pencilScalar_add_of_normalized e he b c hbc o h1 i j hoi hoj hij }271272/-- Exact evaluation of the scalar isomorphism, not merely its existence. -/273@[simp]274theorem scalarRingEquiv_apply (i j : ι) (hoi : o ≠ i) (hoj : o ≠ j)275    (hij : i ≠ j) (a : K) :276    scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij a =277      pencilScalar e b c o j hoj a := rfl278279/-- Every other anchor pencil has this same scalar map, including the case280where the compared axis is the selected reference axis. -/281theorem pencilScalar_eq_scalarRingEquiv (i j : ι)282    (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j)283    (k : ι) (hok : o ≠ k) (a : K) :284    pencilScalar e b c o k hok a = scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij a := by285  by_cases hkj : k = j286  · subst k287    rfl288  · exact pencilScalar_eq_of_normalized e he b c hbc o h1 k j hok hoj hkj a289290end ScalarRigidity291292section Realization293294variable (e : ℙ K V ≃ ℙ L W)295variable (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,296  p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))297variable (b : Module.Basis ι K V) (c : Module.Basis ι L W)298variable (hbc : ∀ i, e (mk K (b i) (b.ne_zero i)) = mk L (c i) (c.ne_zero i))299variable (o : ι)300variable (h1 : ∀ i (hoi : o ≠ i), pencilScalar e b c o i hoi 1 = 1)301include he hbc h1302303/-- On the entire affine chart, the semilinear vector equals the normalized304representative of the specified projective image. -/305theorem coordinateRepresentative_image_eq_semilinearEquiv306    (i j : ι) (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j)307    (v : V) (hv : v ≠ 0) (hvo : b.repr v o = 1) :308    coordinateRepresentative c o (e (mk K v hv)) =309      Module.Basis.semilinearEquiv b c (scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij) v := by310  apply c.repr.injective311  ext k312  rw [Module.Basis.repr_semilinearEquiv]313  by_cases hok : o = k314  · subst k315    have ho : c.repr (e (mk K v hv)).rep o ≠ 0 := by316      intro hz317      exact one_ne_zero (hvo.symm.trans318        ((repr_image_rep_eq_zero_iff e he b c hbc v hv o).mp hz))319    rw [repr_coordinateRepresentative_self c o _ ho, hvo, map_one]320  · rw [repr_coordinateRepresentative_image e he b c hbc o k hok v hv hvo]321    exact pencilScalar_eq_scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij k hok _322323/-- Exact ray evaluation when the anchor coordinate is one. -/324theorem image_mk_eq_semilinearEquiv_of_repr_eq_one325    (i j : ι) (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j)326    (v : V) (hv : v ≠ 0) (hvo : b.repr v o = 1) :327    e (mk K v hv) =328      mk L (Module.Basis.semilinearEquiv b c (scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij) v)329        (by simpa only [map_zero] using330          (Module.Basis.semilinearEquiv b c (scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij)).injective.ne hv) := by331  have ho : c.repr (e (mk K v hv)).rep o ≠ 0 := by332    intro hz333    exact one_ne_zero (hvo.symm.trans334      ((repr_image_rep_eq_zero_iff e he b c hbc v hv o).mp hz))335  have h := (mk_coordinateRepresentative c o (e (mk K v hv)) ho).symm336  simpa only [coordinateRepresentative_image_eq_semilinearEquiv337    e he b c hbc o h1 i j hoi hoj hij v hv hvo] using h338339/-- Rescaling extends the affine-chart evaluation to every vector with nonzero340anchor coordinate. The rescaling is not assumed to fix the given point map. -/341theorem image_mk_eq_semilinearEquiv_of_repr_ne_zero342    (i j : ι) (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j)343    (v : V) (hv : v ≠ 0) (hvo : b.repr v o ≠ 0) :344    e (mk K v hv) =345      mk L (Module.Basis.semilinearEquiv b c (scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij) v)346        (by simpa only [map_zero] using347          (Module.Basis.semilinearEquiv b c (scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij)).injective.ne hv) := by348  let σ := scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij349  let U := Module.Basis.semilinearEquiv b c σ350  let v' := (b.repr v o)⁻¹ • v351  have hv' : v' ≠ 0 := smul_ne_zero (inv_ne_zero hvo) hv352  have hvo' : b.repr v' o = 1 := by simp [v', hvo]353  have hr : mk K v' hv' = mk K v hv :=354    (mk_eq_mk_iff' K v' v hv' hv).mpr ⟨(b.repr v o)⁻¹, rfl⟩355  have hu : U v ≠ 0 := by simpa only [map_zero] using U.injective.ne hv356  have hu' : U v' ≠ 0 := by simpa only [map_zero] using U.injective.ne hv'357  have hrU : mk L (U v') hu' = mk L (U v) hu := by358    apply (mk_eq_mk_iff' L _ _ hu' hu).mpr359    exact ⟨σ ((b.repr v o)⁻¹), (U.map_smulₛₗ _ v).symm⟩360  exact (congrArg e hr).symm.trans361    ((image_mk_eq_semilinearEquiv_of_repr_eq_one362      e he b c hbc o h1 i j hoi hoj hij v' hv' hvo').trans hrU)363364/-- Exact evaluation at every nonzero vector, including those on the omitted365hyperplane. In the zero-anchor case, the image ray lies in the line spanned by366the image of `b o + v` and the anchor, and its anchor coordinate vanishes. -/367theorem image_mk_eq_semilinearEquiv368    (i j : ι) (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j)369    (v : V) (hv : v ≠ 0) :370    e (mk K v hv) =371      mk L (Module.Basis.semilinearEquiv b c (scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij) v)372        (by simpa only [map_zero] using373          (Module.Basis.semilinearEquiv b c (scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij)).injective.ne hv) := by374  by_cases hvo : b.repr v o = 0375  · let σ := scalarRingEquiv e he b c hbc o h1 i j hoi hoj hij376    let U := Module.Basis.semilinearEquiv b c σ377    let z := b o + v378    have hzo : b.repr z o = 1 := by simp [z, hvo]379    have hz : z ≠ 0 := by380      intro hz381      have hc := congrArg (fun v : V => b.repr v o) hz382      have h10 : (1 : K) = 0 := by383        simpa only [hzo, map_zero, Finsupp.zero_apply] using hc384      exact one_ne_zero h10385    have huv : U v ≠ 0 := by simpa only [map_zero] using U.injective.ne hv386    have huz : U z ≠ 0 := by simpa only [map_zero] using U.injective.ne hz387    have hez : e (mk K z hz) = mk L (U z) huz :=388      image_mk_eq_semilinearEquiv_of_repr_eq_one389        e he b c hbc o h1 i j hoi hoj hij z hz hzo390    let P : Submodule K V := (K ∙ b o) ⊔ (K ∙ z)391    have hboP : b o ∈ P := (show K ∙ b o ≤ P from le_sup_left)392      (Submodule.mem_span_singleton_self _)393    have hzP : z ∈ P := (show K ∙ z ≤ P from le_sup_right)394      (Submodule.mem_span_singleton_self _)395    have hvP : v ∈ P := by396      have h := P.sub_mem hzP hboP397      simpa [z, add_sub_cancel_left] using h398    have hmap : submoduleOrderIsoOfFiniteSpan e he P =399        (L ∙ c o) ⊔ (L ∙ U z) := by400      dsimp [P]401      rw [submoduleOrderIsoOfFiniteSpan_sup,402        submoduleOrderIsoOfFiniteSpan_span_singleton e he _ (b.ne_zero o),403        submoduleOrderIsoOfFiniteSpan_span_singleton e he _ hz,404        hbc o, hez, submodule_mk, submodule_mk]405      rfl406    have hwP : (e (mk K v hv)).rep ∈ (L ∙ c o) ⊔ (L ∙ U z) := by407      rw [← hmap, mem_submoduleOrderIsoOfFiniteSpan_iff e he _ _ (rep_nonzero _),408        mk_rep, e.symm_apply_apply, Submodule.mk_mem_projectivization_iff]409      exact hvP410    obtain ⟨w₁, hw₁, w₂, hw₂, hw⟩ := Submodule.mem_sup.mp hwP411    obtain ⟨a, rfl⟩ := Submodule.mem_span_singleton.mp hw₁412    obtain ⟨d, rfl⟩ := Submodule.mem_span_singleton.mp hw₂413    have hwo : c.repr (e (mk K v hv)).rep o = 0 :=414      (repr_image_rep_eq_zero_iff e he b c hbc v hv o).mpr hvo415    have huzo : c.repr (U z) o = 1 := by416      change c.repr (Module.Basis.semilinearEquiv b c σ z) o = 1417      rw [Module.Basis.repr_semilinearEquiv, hzo, map_one]418    have had : a + d = 0 := by419      have hc := congrArg (fun w : W => c.repr w o) hw420      simp only [map_add, map_smul, Finsupp.add_apply, Finsupp.smul_apply,421        smul_eq_mul] at hc422      rw [huzo, hwo] at hc423      simpa using hc424    have huzv : U z = c o + U v := by425      change Module.Basis.semilinearEquiv b c σ (b o + v) = c o + U v426      rw [map_add, Module.Basis.semilinearEquiv_apply_basis]427    have hd : d • U v = (e (mk K v hv)).rep := by428      calc429        d • U v = (a + d) • c o + d • U v := by rw [had, zero_smul, zero_add]430        _ = a • c o + d • U z := by rw [huzv, smul_add, add_smul]; abel431        _ = (e (mk K v hv)).rep := hw432    exact (mk_rep (e (mk K v hv))).symm.trans433      ((mk_eq_mk_iff' L _ _ (rep_nonzero _) huv).mpr ⟨d, hd⟩)434  · exact image_mk_eq_semilinearEquiv_of_repr_ne_zero435      e he b c hbc o h1 i j hoi hoj hij v hv hvo436437end Realization438439section CanonicalRealization440441variable (e : ℙ K V ≃ ℙ L W)442variable (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,443  p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))444variable (b : Module.Basis ι K V) (o i j : ι)445variable (hoi : o ≠ i) (hoj : o ≠ j) (hij : i ≠ j)446447/-- The scalar isomorphism constructed from a given point equivalence and three448basis indices. The compatible normalized target basis is constructed, not assumed. -/449def scalarEquivOfFiniteSpan : K ≃+* L :=450  scalarRingEquiv e he b (normalizedBasisOfFiniteSpan e he b o)451    (image_mk_normalizedBasisOfFiniteSpan e he b o) o452    (pencilScalar_one_normalizedBasisOfFiniteSpan e he b o) i j hoi hoj hij453454/-- The actual semilinear equivalence realizing the specified projective map.455Its coefficients are the scalar isomorphism just constructed from incidence. -/456def semilinearEquivOfFiniteSpan :457    V ≃ₛₗ[(scalarEquivOfFiniteSpan e he b o i j hoi hoj hij).toRingHom] W :=458  Module.Basis.semilinearEquiv b (normalizedBasisOfFiniteSpan e he b o)459    (scalarEquivOfFiniteSpan e he b o i j hoi hoj hij)460461/-- Exact all-ray realization, including vectors whose anchor coordinate is zero. -/462theorem image_mk_eq_semilinearEquivOfFiniteSpan (v : V) (hv : v ≠ 0) :463    e (mk K v hv) = mk L (semilinearEquivOfFiniteSpan e he b o i j hoi hoj hij v)464      (by simpa only [map_zero] using465        (semilinearEquivOfFiniteSpan e he b o i j hoi hoj hij).injective.ne hv) :=466  image_mk_eq_semilinearEquiv e he b (normalizedBasisOfFiniteSpan e he b o)467    (image_mk_normalizedBasisOfFiniteSpan e he b o) o468    (pencilScalar_one_normalizedBasisOfFiniteSpan e he b o) i j hoi hoj hij v hv469470/-- Membership in the transported algebraic submodule is evaluated by the471actual inverse semilinear equivalence. The zero vector is treated separately. -/472theorem mem_submoduleOrderIsoOfFiniteSpan_iff_semilinearEquivOfFiniteSpan473    (P : Submodule K V) (w : W) :474    w ∈ submoduleOrderIsoOfFiniteSpan e he P ↔475      (semilinearEquivOfFiniteSpan e he b o i j hoi hoj hij).symm w ∈ P := by476  let U := semilinearEquivOfFiniteSpan e he b o i j hoi hoj hij477  by_cases hw : w = 0478  · subst w479    simp only [map_zero, Submodule.zero_mem, iff_self]480  · have hv : U.symm w ≠ 0 := by simpa only [map_zero] using U.symm.injective.ne hw481    have hr : e (mk K (U.symm w) hv) = mk L w hw := by482      have h := image_mk_eq_semilinearEquivOfFiniteSpan483        e he b o i j hoi hoj hij (U.symm w) hv484      exact h.trans ((mk_eq_mk_iff' L _ _ _ hw).mpr485        ⟨1, by rw [one_smul]; exact (U.apply_symm_apply w).symm⟩)486    have hr' : e.symm (mk L w hw) = mk K (U.symm w) hv := by487      rw [← hr, e.symm_apply_apply]488    rw [mem_submoduleOrderIsoOfFiniteSpan_iff e he P w hw, hr',489      Submodule.mk_mem_projectivization_iff]490491/-- Evaluation on every algebraic submodule, without replacing it by its492closure or by a finite-dimensional subspace. -/493theorem submoduleOrderIsoOfFiniteSpan_eq_map_semilinearEquivOfFiniteSpan494    (P : Submodule K V) :495    submoduleOrderIsoOfFiniteSpan e he P =496      P.map (semilinearEquivOfFiniteSpan e he b o i j hoi hoj hij).toLinearMap := by497  let U := semilinearEquivOfFiniteSpan e he b o i j hoi hoj hij498  ext w499  rw [mem_submoduleOrderIsoOfFiniteSpan_iff_semilinearEquivOfFiniteSpan500    e he b o i j hoi hoj hij]501  constructor502  · intro hw503    exact Submodule.mem_map.mpr ⟨U.symm w, hw, U.apply_symm_apply w⟩504  · rintro ⟨v, hv, rfl⟩505    change U.symm (U v) ∈ P506    rwa [U.symm_apply_apply]507508end CanonicalRealization509510/-- Fundamental semilinear realization over fields. The dimension hypothesis is511cardinal-valued algebraic rank. There is no finite-dimensionality, topology,512regularity, involutivity, or continuity hypothesis on the scalar isomorphism.513The conclusion realizes the given equivalence on every nonzero vector. -/514theorem exists_semilinearEquiv_of_finite_span515    (e : ℙ K V ≃ ℙ L W)516    (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,517      p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))518    (hdim : 3 ≤ Module.rank K V) :519    ∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W,520      ∀ (v : V) (hv : v ≠ 0), e (mk K v hv) =521        mk L (U v) (by simpa only [map_zero] using U.injective.ne hv) := by522  classical523  let b := Module.Free.chooseBasis K V524  have hcard : (3 : Cardinal) ≤ Cardinal.mk (Module.Free.ChooseBasisIndex K V) := by525    simpa only [Module.Free.rank_eq_card_chooseBasisIndex] using hdim526  obtain ⟨k⟩ : Nonempty (Fin 3 ↪ Module.Free.ChooseBasisIndex K V) :=527    Cardinal.lift_mk_le'.mp (by simpa using hcard)528  have h01 : k 0 ≠ k 1 := k.injective.ne (by decide)529  have h02 : k 0 ≠ k 2 := k.injective.ne (by decide)530  have h12 : k 1 ≠ k 2 := k.injective.ne (by decide)531  refine ⟨scalarEquivOfFiniteSpan e he b (k 0) (k 1) (k 2) h01 h02 h12,532    semilinearEquivOfFiniteSpan e he b (k 0) (k 1) (k 2) h01 h02 h12, ?_⟩533  exact image_mk_eq_semilinearEquivOfFiniteSpan e he b (k 0) (k 1) (k 2) h01 h02 h12534535/-- The same realization as equality of functions on the full projective space.536This is stronger than agreement merely on chosen basis rays. -/537theorem exists_map_eq_of_finite_span538    (e : ℙ K V ≃ ℙ L W)539    (he : ∀ (T : Set (ℙ K V)), T.Finite → ∀ p,540      p ∈ Subspace.span T ↔ e p ∈ Subspace.span (e '' T))541    (hdim : 3 ≤ Module.rank K V) :542    ∃ σ : K ≃+* L, ∃ U : V ≃ₛₗ[σ.toRingHom] W,543      Projectivization.map U.toLinearMap U.injective = e := by544  obtain ⟨σ, U, hU⟩ := exists_semilinearEquiv_of_finite_span e he hdim545  refine ⟨σ, U, ?_⟩546  funext p547  induction p using Projectivization.ind with548  | h v hv =>549    rw [Projectivization.map_mk]550    exact (hU v hv).symm551552end Projectivization