feat(LinearAlgebra/Projectivization): GL(V) action (#26811)

Some API around projective spaces and general linear groups:

- an equiv between V and W gives an equiv between GL(V) and GL(W)
- GL(V) acts on the projectivization of V
- GL 2 K acts on `OnePoint K` (which is the projectivization of `K x K`)

I am adding these because I need them to define cusps in modular form theory, but they are hopefully something of general usefulness beyond that.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: loefflerd

Mathlib.lean

@@ -4210,6 +4210,7 @@ import Mathlib.LinearAlgebra.Pi
 import Mathlib.LinearAlgebra.PiTensorProduct
 import Mathlib.LinearAlgebra.Prod
 import Mathlib.LinearAlgebra.Projection
+import Mathlib.LinearAlgebra.Projectivization.Action
 import Mathlib.LinearAlgebra.Projectivization.Basic
 import Mathlib.LinearAlgebra.Projectivization.Cardinality
 import Mathlib.LinearAlgebra.Projectivization.Constructions

Mathlib/LinearAlgebra/GeneralLinearGroup.lean

@@ -40,15 +40,20 @@ def toLinearEquiv (f : GeneralLinearGroup R M) : M ≃ₗ[R] M :=
     left_inv := fun m ↦ show (f.inv * f.val) m = m by rw [f.inv_val]; simp
     right_inv := fun m ↦ show (f.val * f.inv) m = m by rw [f.val_inv]; simp }
 
+@[simp] lemma coe_toLinearEquiv (f : GeneralLinearGroup R M) :
+    f.toLinearEquiv = (f : M → M) := rfl
+
 /-- An equivalence from `M` to itself determines an invertible linear map. -/
 def ofLinearEquiv (f : M ≃ₗ[R] M) : GeneralLinearGroup R M where
   val := f
   inv := (f.symm : M →ₗ[R] M)
   val_inv := LinearMap.ext fun _ ↦ f.apply_symm_apply _
   inv_val := LinearMap.ext fun _ ↦ f.symm_apply_apply _
 
-variable (R M)
+@[simp] lemma coe_ofLinearEquiv (f : M ≃ₗ[R] M) :
+    ofLinearEquiv f = (f : M → M) := rfl
 
+variable (R M) in
 /-- The general linear group on `R` and `M` is multiplicatively equivalent to the type of linear
 equivalences between `M` and itself. -/
 def generalLinearEquiv : GeneralLinearGroup R M ≃* M ≃ₗ[R] M where
@@ -64,6 +69,53 @@ theorem generalLinearEquiv_to_linearMap (f : GeneralLinearGroup R M) :
 theorem coeFn_generalLinearEquiv (f : GeneralLinearGroup R M) :
     (generalLinearEquiv R M f) = (f : M → M) := rfl
 
+section Functoriality
+
+variable {R₁ R₂ R₃ M₁ M₂ M₃ : Type*}
+  [Semiring R₁] [Semiring R₂] [Semiring R₃]
+  [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃]
+  [Module R₁ M₁] [Module R₂ M₂] [Module R₃ M₃]
+  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃}
+  {σ₂₁ : R₂ →+* R₁} {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁}
+  [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₁₃ σ₃₁]
+  [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomInvPair σ₃₁ σ₁₃]
+  [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
+
+/-- A semilinear equivalence from `V` to `W` determines an isomorphism of general linear
+groups. -/
+def congrLinearEquiv (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) :
+    GeneralLinearGroup R₁ M₁ ≃* GeneralLinearGroup R₂ M₂ :=
+  Units.mapEquiv (LinearEquiv.conjRingEquiv e₁₂).toMulEquiv
+
+@[simp] lemma congrLinearEquiv_apply (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (g : GeneralLinearGroup R₁ M₁) :
+    congrLinearEquiv e₁₂ g = ofLinearEquiv (e₁₂.symm.trans <| g.toLinearEquiv.trans e₁₂) :=
+  rfl
+
+@[simp] lemma congrLinearEquiv_symm (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) :
+    (congrLinearEquiv e₁₂).symm = congrLinearEquiv e₁₂.symm :=
+  rfl
+
+@[simp]
+lemma congrLinearEquiv_trans
+    {N₁ N₂ N₃ : Type*} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃]
+    [Module R N₁] [Module R N₂] [Module R N₃] (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃) :
+    (congrLinearEquiv e₁₂).trans (congrLinearEquiv e₂₃) = congrLinearEquiv (e₁₂.trans e₂₃) :=
+  rfl
+
+/-- Stronger form of `congrLinearEquiv.trans` applying to semilinear maps. Not a simp lemma as
+`σ₁₃` and `σ₃₁` cannot be inferred from the LHS. -/
+lemma congrLinearEquiv_trans' (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) :
+    (congrLinearEquiv e₁₂).trans (congrLinearEquiv e₂₃) =
+      congrLinearEquiv (e₁₂.trans e₂₃) :=
+  rfl
+
+@[simp]
+lemma congrLinearEquiv_refl :
+    congrLinearEquiv (LinearEquiv.refl R₁ M₁) = MulEquiv.refl (GeneralLinearGroup R₁ M₁) :=
+  rfl
+
+end Functoriality
+
 end GeneralLinearGroup
 
 end LinearMap

Mathlib/LinearAlgebra/Projectivization/Action.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2025 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+import Mathlib.LinearAlgebra.Projectivization.Basic
+import Mathlib.GroupTheory.GroupAction.Ring
+
+/-!
+# Group actions on projectivization
+
+Show that (among other groups), the general linear group of `V` acts on `ℙ K V`.
+-/
+
+open scoped LinearAlgebra.Projectivization Matrix
+
+namespace Projectivization
+
+section DivisionRing
+
+variable {G K V : Type*} [AddCommGroup V] [DivisionRing K] [Module K V]
+  [Group G] [DistribMulAction G V] [SMulCommClass G K V]
+
+/-- Any group acting `K`-linearly on `V` (such as the general linear group) acts on `ℙ V`. -/
+@[simps -isSimp]
+instance : MulAction G (ℙ K V) where
+  smul g x := x.map (DistribMulAction.toModuleEnd _ _ g)
+    (DistribMulAction.toLinearEquiv _ _ g).injective
+  one_smul x := show map _ _ _ = _ by simp [map_one, Module.End.one_eq_id]
+  mul_smul g g' x := show map _ _ _ = map _ _ (map _ _ _) by
+    simp_rw [map_mul, Module.End.mul_eq_comp]
+    rw [map_comp, Function.comp_apply]
+
+lemma generalLinearGroup_smul_def (g : LinearMap.GeneralLinearGroup K V) (x : ℙ K V) :
+    g • x = x.map g.toLinearEquiv.toLinearMap g.toLinearEquiv.injective := by
+  rfl
+
+@[simp]
+lemma smul_mk (g : G) {v : V} (hv : v ≠ 0) :
+    g • mk K v hv = mk K (g • v) ((smul_ne_zero_iff_ne g).mpr hv) :=
+  rfl
+
+end DivisionRing
+
+end Projectivization

Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean

@@ -3,9 +3,12 @@ Copyright (c) 2024 Bjørn Kjos-Hanssen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bjørn Kjos-Hanssen, Oliver Nash
 -/
-import Mathlib.LinearAlgebra.Projectivization.Basic
+import Mathlib.Data.Matrix.Action
+import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
+import Mathlib.LinearAlgebra.Projectivization.Action
 import Mathlib.Topology.Compactification.OnePoint.Basic
 
+
 /-!
 # One-point compactification and projectivization
 
@@ -26,9 +29,35 @@ one-point extension, projectivization
 -/
 
 open scoped LinearAlgebra.Projectivization OnePoint
-open Projectivization
+
+open Projectivization Matrix
+
+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 _
+
+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 [Units.smul_def]
+
+end MatrixProdAction
 
 namespace OnePoint
+
+section DivisionRing
+
 variable (K : Type*) [DivisionRing K] [DecidableEq K]
 
 /-- The one-point compactification of a division ring `K` is equivalent to
@@ -68,4 +97,36 @@ 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
   simp [equivProjectivization]
 
+end DivisionRing
+
+section Field
+
+variable {K : Type*} [Field K] [DecidableEq K]
+
+/-- For a field `K`, the group `GL(2, K)` acts on `OnePoint K`, via the canonical identification
+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 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
+  simp [Equiv.smul_def, mulVec_eq_sum, Units.smul_def]
+
+lemma smul_infty_eq_ite (g : GL (Fin 2) K) :
+    g • (∞ : OnePoint K) = if g 1 0 = 0 then ∞ else g 0 0 / g 1 0 := by
+  by_cases h : g 1 0 = 0 <;>
+  simp [h, div_eq_inv_mul, smul_infty_def]
+
+lemma smul_infty_eq_iff (g : GL (Fin 2) K) :
+    g • (∞ : OnePoint K) = ∞ ↔ g 1 0 = 0 := by
+  simp [smul_infty_eq_ite]
+
+lemma smul_some_eq_ite (g : GL (Fin 2) K) (k : K) :
+    g • (k : OnePoint K) =
+      if g 1 0 * k + g 1 1 = 0 then ∞ else (g 0 0 * k + g 0 1) / (g 1 0 * k + g 1 1) := by
+  simp [Equiv.smul_def, mulVec_eq_sum, div_eq_inv_mul, mul_comm, Units.smul_def]
+
+end Field
+
 end OnePoint