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

At the moment `OnePoint.equivProjectivization` identifies the one-point compactification of `K` with the projective space on `K x K`. This is slightly inconvenient since most of mathlib's linear algebra prefers `Fin n → K`. This PR uses the Pi type instead of the product. This is preparatory to adding more material about fixed points of Moebius transformations, etc, in future PR's.

Author: loefflerd

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,21 +40,37 @@ section MatrixProdAction
 
 variable {R n : Type*} [Semiring R] [Fintype n] [DecidableEq n]
 
+@[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]
+
+@[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]
+
+@[deprecated "use Fin 2 → R instead" (since := "2026-04-19")]
 instance : Module (Matrix (Fin 2) (Fin 2) R) (R × R) :=
   (LinearEquiv.finTwoArrow R R).symm.toAddEquiv.module _
 
+@[deprecated "use Fin 2 → R instead" (since := "2026-04-19")]
 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) :
+@[deprecated "use Fin 2 → R instead" (since := "2026-04-19")]
+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]
+set_option linter.deprecated false in
+@[deprecated Matrix.GeneralLinearGroup.fin_two_smul (since := "2026-04-19")]
+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 [Units.smul_def]
+  simp [Units.smul_def, Matrix.fin_two_smul_prod]
 
 end MatrixProdAction
 
@@ -65,40 +81,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 +127,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) :