refactor(OnePoint/ProjectiveLine): use Pi instead of Prod

Author: loefflerd

Mathlib/LinearAlgebra/Projectivization/Action.lean

@@ -5,8 +5,10 @@ Authors: David Loeffler
 -/
 module
 
+public import Mathlib.Data.Matrix.Action
+public import Mathlib.LinearAlgebra.Eigenspace.Basic
+public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
 public import Mathlib.LinearAlgebra.Projectivization.Basic
-public import Mathlib.GroupTheory.GroupAction.Ring
 
 /-!
 # Group actions on projectivization
@@ -16,7 +18,7 @@ Show that (among other groups), the general linear group of `V` acts on `ℙ K V
 
 @[expose] public section
 
-open scoped LinearAlgebra.Projectivization Matrix
+open LinearAlgebra.Projectivization Matrix
 
 namespace Projectivization
 
@@ -46,4 +48,32 @@ lemma smul_mk (g : G) {v : V} (hv : v ≠ 0) :
 
 end DivisionRing
 
+section Field
+
+variable {K : Type*} [Field K]
+
+/-- The fixed points of an invertible linear map acting on the projectivization of a vector
+space are precisely the eigenspaces. -/
+theorem smul_eq_self_iff' {M : Type*} [AddCommGroup M] [Module K M]
+    {g : LinearMap.GeneralLinearGroup K M} {y : Projectivization K M} :
+    g • y = y ↔ ∃ a, y.submodule ≤ Module.End.eigenspace g a := by
+  induction y with | h y hy =>
+  simp only [Projectivization.smul_mk, Projectivization.mk_eq_mk_iff,
+    SetLike.le_def, Module.End.mem_eigenspace_iff, Projectivization.submodule_mk,
+    Submodule.mem_span_singleton, forall_exists_index]
+  constructor
+  · refine fun ⟨a, hay⟩ ↦ ⟨a, fun x b hxb ↦ ?_⟩
+    simp [← hxb, smul_comm _ b, ← a.smul_def, g.smul_def, hay]
+  · rintro ⟨a, ha⟩
+    refine ⟨.mk0 a (fun ha' ↦ hy ?_), (ha 1 (one_smul ..)).symm⟩
+    specialize ha 1 rfl
+    exact (smul_eq_zero_iff_eq g).mp (by aesop)
+
+theorem smul_eq_self_iff {ι : Type*} [Fintype ι] [DecidableEq ι]
+    {g : GL ι K} {y : Projectivization K (ι → K)} :
+    g • y = y ↔ ∃ a, y.submodule ≤ Module.End.eigenspace g.toLin a :=
+  smul_eq_self_iff' (g := g.toLin)
+
+end Field
+
 end Projectivization

Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean

@@ -15,15 +15,15 @@ public import Mathlib.Topology.Compactification.OnePoint.Basic
 # One-point compactification and projectivization
 
 We construct a set-theoretic equivalence between
-`OnePoint K` and the projectivization `ℙ K (K × K)` for an arbitrary division ring `K`.
+`OnePoint K` and the projectivization `ℙ K (Fin 2 → K)` for an arbitrary division ring `K`.
 
 TODO: Add the extension of this equivalence to a homeomorphism in the case `K = ℝ`,
 where `OnePoint ℝ` gets the topology of one-point compactification.
 
 
 ## Main definitions and results
 
-* `OnePoint.equivProjectivization` : the equivalence `OnePoint K ≃ ℙ K (K × K)`.
+* `OnePoint.equivProjectivization` : the equivalence `OnePoint K ≃ ℙ K (Fin 2 → K)`.
 
 ## Tags
 
@@ -40,20 +40,15 @@ section MatrixProdAction
 
 variable {R n : Type*} [Semiring R] [Fintype n] [DecidableEq n]
 
-instance : Module (Matrix (Fin 2) (Fin 2) R) (R × R) :=
-  (LinearEquiv.finTwoArrow R R).symm.toAddEquiv.module _
+@[simp] lemma Matrix.mulVec_fin_two (m : Matrix (Fin 2) (Fin 2) R) (v : Fin 2 → R) :
+    m *ᵥ v = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] := by
+  ext i
+  fin_cases i <;>
+  simp [mulVec_eq_sum]
 
-instance {S} [DistribSMul S R] [SMulCommClass R S R] :
-    SMulCommClass (Matrix (Fin 2) (Fin 2) R) S (R × R) :=
-  (LinearEquiv.finTwoArrow R R).symm.smulCommClass _ _
-
-@[simp] lemma Matrix.fin_two_smul_prod (g : Matrix (Fin 2) (Fin 2) R) (v : R × R) :
-    g • v = (g 0 0 * v.1 + g 0 1 * v.2, g 1 0 * v.1 + g 1 1 * v.2) := by
-  simp [Equiv.smul_def, smul_eq_mulVec, Matrix.mulVec_eq_sum]
-
-@[simp] lemma Matrix.GeneralLinearGroup.fin_two_smul_prod {R : Type*} [CommRing R]
-    (g : GL (Fin 2) R) (v : R × R) :
-    g • v = (g 0 0 * v.1 + g 0 1 * v.2, g 1 0 * v.1 + g 1 1 * v.2) := by
+@[simp] lemma Matrix.GeneralLinearGroup.fin_two_smul {R : Type*} [CommRing R]
+    (g : GL (Fin 2) R) (v : Fin 2 → R) :
+    g • v = ![g 0 0 * v 0 + g 0 1 * v 1, g 1 0 * v 0 + g 1 1 * v 1] := by
   simp [Units.smul_def]
 
 end MatrixProdAction
@@ -65,40 +60,39 @@ section DivisionRing
 variable (K : Type*) [DivisionRing K] [DecidableEq K]
 
 /-- The one-point compactification of a division ring `K` is equivalent to
-the projectivization `ℙ K (K × K)`. -/
-def equivProjectivization :
-    OnePoint K ≃ ℙ K (K × K) where
-  toFun p := p.elim (mk K (1, 0) (by simp)) (fun t ↦ mk K (t, 1) (by simp))
+the projectivization `ℙ K (Fin 2 → K)`. -/
+def equivProjectivization : OnePoint K ≃ ℙ K (Fin 2 → K) where
+  toFun p := p.elim (mk K ![1, 0] (by simp)) (fun t ↦ mk K ![t, 1] (by simp))
   invFun p := by
     refine Projectivization.lift
-      (fun u : {v : K × K // v ≠ 0} ↦ if u.1.2 = 0 then ∞ else ((u.1.2)⁻¹ * u.1.1)) ?_ p
-    rintro ⟨-, hv⟩ ⟨⟨x, y⟩, hw⟩ t rfl
+      (fun u : {v : Fin 2 → K // v ≠ 0} ↦ if u.1 1 = 0 then ∞ else ((u.1 1)⁻¹ * u.1 0)) ?_ p
+    rintro ⟨-, hv⟩ ⟨w, hw⟩ t rfl
     have ht : t ≠ 0 := by rintro rfl; simp at hv
-    by_cases h₀ : y = 0 <;> simp [h₀, ht, mul_assoc]
+    by_cases h₀ : w 1 = 0 <;> simp [h₀, ht, mul_assoc]
   left_inv p := by cases p <;> simp
   right_inv p := by
-    induction p using ind with | h p hp =>
-    obtain ⟨x, y⟩ := p
-    by_cases h₀ : y = 0 <;> simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true,
-      if_false, OnePoint.elim_infty, OnePoint.elim_some, Prod.smul_mk, Prod.mk.injEq, smul_eq_mul,
-      mul_zero, and_true]
-    · use x⁻¹
-      simp_all
-    · exact ⟨y⁻¹, rfl, inv_mul_cancel₀ h₀⟩
+    induction p using ind with | h w hw =>
+    by_cases h₀ : w 1 = 0 <;> simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true,
+        if_false, OnePoint.elim_infty, OnePoint.elim_some]
+    · have : w 0 ≠ 0 := fun h ↦ hw <| funext <| by simp_all
+      use (w 0)⁻¹
+      ext i
+      fin_cases i <;> simp_all
+    · exact ⟨(w 1)⁻¹, funext <| by simp [inv_mul_cancel₀ h₀]⟩
 
 @[simp]
 lemma equivProjectivization_apply_infinity :
-    equivProjectivization K ∞ = mk K ⟨1, 0⟩ (by simp) :=
+    equivProjectivization K ∞ = mk K ![1, 0] (by simp) :=
   rfl
 
 @[simp]
 lemma equivProjectivization_apply_coe (t : K) :
-    equivProjectivization K t = mk K ⟨t, 1⟩ (by simp) :=
+    equivProjectivization K t = mk K ![t, 1] (by simp) :=
   rfl
 
 @[simp]
-lemma equivProjectivization_symm_apply_mk (x y : K) (h : (x, y) ≠ 0) :
-    (equivProjectivization K).symm (mk K ⟨x, y⟩ h) = if y = 0 then ∞ else y⁻¹ * x := by
+lemma equivProjectivization_symm_apply_mk (v : Fin 2 → K) (h : v ≠ 0) :
+    (equivProjectivization K).symm (mk K v h) = if v 1 = 0 then ∞ else (v 1)⁻¹ * v 0 := by
   simp [equivProjectivization]
 
 end DivisionRing
@@ -112,9 +106,14 @@ with the `ℙ¹(K)` (which is given explicitly by Möbius transformations). -/
 instance instGLAction : MulAction (GL (Fin 2) K) (OnePoint K) :=
   (equivProjectivization K).mulAction (GL (Fin 2) K)
 
+lemma equivProjectivization_smul {g : GL (Fin 2) K} (x : OnePoint K) :
+    equivProjectivization K (g • x) = g • equivProjectivization K x := by
+  rw [Equiv.smul_def, Equiv.apply_symm_apply]
+
 lemma smul_infty_def {g : GL (Fin 2) K} :
-    g • ∞ = (equivProjectivization K).symm (.mk K (g 0 0, g 1 0) (fun h ↦ by
-      simpa [det_fin_two, Prod.mk_eq_zero.mp h] using g.det_ne_zero)) := by
+    g • ∞ = (equivProjectivization K).symm (.mk K ![g 0 0, g 1 0] (fun h ↦ by
+      simpa [det_fin_two, show g 0 0 = 0 from congr_fun h 0, show g 1 0 = 0 from congr_fun h 1]
+        using g.det_ne_zero)) := by
   simp [Equiv.smul_def, mulVec_eq_sum, Units.smul_def]
 
 lemma smul_infty_eq_ite (g : GL (Fin 2) K) :
@@ -146,6 +145,13 @@ namespace Matrix.GeneralLinearGroup
 
 variable {K : Type*} [Field K] [DecidableEq K]
 
+lemma smul_eq_self_iff {g : GL (Fin 2) K} {x : OnePoint K} :
+    g • x = x ↔ ∃ a : K,
+      (equivProjectivization K x).submodule ≤ Module.End.eigenspace (toLin g).val a := by
+  set y := equivProjectivization K x
+  rw [show g • x = x ↔ g • y = y by rw [← equivProjectivization_smul, (Equiv.injective _).eq_iff]]
+  apply Projectivization.smul_eq_self_iff
+
 /-- The roots of `g.fixpointPolynomial` are the fixed points of `g ∈ GL(2, K)` acting on the finite
 part of `OnePoint K`. -/
 lemma fixpointPolynomial_aeval_eq_zero_iff {c : K} {g : GL (Fin 2) K} :