[Merged by Bors] - feat(GeneralLinearGroup/FinTwo): the addChar sending x to [1,x;0,1]

Mathlib/Algebra/Group/AddChar.lean

@@ -93,6 +93,8 @@ instance instFunLike : FunLike (AddChar A M) A M where
   coe := AddChar.toFun
   coe_injective' φ ψ h := by cases φ; cases ψ; congr
 
+initialize_simps_projections AddChar (toFun → apply) -- needs to come after FunLike instance
+
 @[ext] lemma ext (f g : AddChar A M) (h : ∀ x : A, f x = g x) : f = g :=
   DFunLike.ext f g h
 

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean

@@ -3,6 +3,7 @@ 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.Algebra.Group.AddChar
 import Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
 
@@ -21,10 +22,10 @@ variable {R : Type*} [CommRing R] [Nontrivial R] (m : Matrix (Fin 2) (Fin 2) R)
 /-- A `2 × 2` matrix is *parabolic* if it is non-scalar and its discriminant is 0. -/
 def IsParabolic : Prop := m ∉ Set.range (scalar _) ∧ m.disc = 0
 
-section conjugation
-
 variable {m}
 
+section conjugation
+
 @[simp] lemma disc_conj : (g.val * m * g.val⁻¹).disc = m.disc := by
   simp only [disc_fin_two, ← Matrix.coe_units_inv, trace_units_conj, det_units_conj]
 
@@ -41,6 +42,23 @@ variable {m}
 
 end conjugation
 
+lemma isParabolic_iff_of_upperTriangular [IsReduced R] (hm : m 1 0 = 0) :
+    m.IsParabolic ↔ m 0 0 = m 1 1 ∧ m 0 1 ≠ 0 := by
+  rw [IsParabolic]
+  have aux : m.disc = 0 ↔ m 0 0 = m 1 1 := by
+    suffices m.disc = (m 0 0 - m 1 1) ^ 2 by
+      rw [this, IsReduced.pow_eq_zero_iff two_ne_zero, sub_eq_zero]
+    grind [disc_fin_two, trace_fin_two, det_fin_two]
+  have (h : m 0 0 = m 1 1) : m ∈ Set.range (scalar _) ↔ m 0 1 = 0 := by
+    constructor
+    · rintro ⟨a, rfl⟩
+      simp
+    · intro h'
+      use m 1 1
+      ext i j
+      fin_cases i <;> fin_cases j <;> simp [h, h', hm]
+  tauto
+
 end CommRing
 
 section Field
@@ -118,6 +136,23 @@ end LinearOrderedRing
 
 namespace GeneralLinearGroup
 
+section Ring
+
+variable {R : Type*} [Ring R]
+
+/-- The map sending `x` to `[1, x; 0, 1]` (bundled as an `AddChar`). -/
+@[simps apply]
+def upperRightHom : AddChar R (GL (Fin 2) R) where
+  toFun x := ⟨!![1, x; 0, 1], !![1, -x; 0, 1], by simp [one_fin_two], by simp [one_fin_two]⟩
+  map_zero_eq_one' := by simp [Units.ext_iff, one_fin_two]
+  map_add_eq_mul' a b := by simp [Units.ext_iff, add_comm]
+
+lemma injective_upperRightHom : Function.Injective (upperRightHom (R := R)) := by
+  refine (injective_iff_map_eq_zero (upperRightHom (R := R)).toAddMonoidHom).mpr ?_
+  simp [Units.ext_iff, one_fin_two]
+
+end Ring
+
 variable {R K : Type*} [CommRing R] [Field K]
 
 /-- Synonym of `Matrix.IsParabolic`, for dot-notation. -/
@@ -189,6 +224,32 @@ lemma IsParabolic.pow {g : GL (Fin 2) K} (hg : IsParabolic g) [CharZero K]
     rw [← hg] at hmsq
     rw [Units.val_pow_eq_pow_val, hmsq, det_zero ⟨0⟩]
 
+lemma isParabolic_iff_of_upperTriangular {g : GL (Fin 2) K} (hg : g 1 0 = 0) :
+    g.IsParabolic ↔ g 0 0 = g 1 1 ∧ g 0 1 ≠ 0 :=
+  Matrix.isParabolic_iff_of_upperTriangular hg
+
+/-- Specialized version of `isParabolic_iff_of_upperTriangular` intended for use with
+discrete subgroups of `GL(2, ℝ)`. -/
+lemma isParabolic_iff_of_upperTriangular_of_det [LinearOrder K] [IsStrictOrderedRing K]
+    {g : GL (Fin 2) K} (h_det : g.det = 1 ∨ g.det = -1) (hg10 : g 1 0 = 0) :
+    g.IsParabolic ↔ (∃ x ≠ 0, g = upperRightHom x) ∨ (∃ x ≠ 0, g = -upperRightHom x) := by
+  rw [isParabolic_iff_of_upperTriangular hg10]
+  constructor
+  · rintro ⟨hg00, hg01⟩
+    have : g 1 1 ^ 2 = 1 := by
+      have : g.det = g 1 1 ^ 2 := by rw [val_det_apply, det_fin_two, hg10, hg00]; ring
+      simp only [Units.ext_iff, Units.val_one, Units.val_neg, this] at h_det
+      exact h_det.resolve_right (neg_one_lt_zero.trans_le <| sq_nonneg _).ne'
+    apply (sq_eq_one_iff.mp this).imp <;> intro hg11 <;> simp only [Units.ext_iff]
+    · refine ⟨g 0 1, hg01, ?_⟩
+      rw [g.val.eta_fin_two]
+      simp_all
+    · refine ⟨-g 0 1, neg_eq_zero.not.mpr hg01, ?_⟩
+      rw [g.val.eta_fin_two]
+      simp_all
+  · rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩) <;>
+    simpa using hx
+
 end GeneralLinearGroup
 
 end Matrix

Mathlib/NumberTheory/ModularForms/Cusps.lean

@@ -16,7 +16,7 @@ import Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
 We define the cusps of a subgroup of `GL(2, ℝ)` as the fixed points of parabolic elements.
 -/
 
-open Matrix SpecialLinearGroup Filter Polynomial OnePoint
+open Matrix SpecialLinearGroup GeneralLinearGroup Filter Polynomial OnePoint
 
 open scoped MatrixGroups LinearAlgebra.Projectivization
 
@@ -37,6 +37,17 @@ lemma exists_mem_SL2 (A : Type*) [CommRing A] [IsDomain A] [Algebra A K] [IsFrac
 
 end OnePoint
 
+namespace Subgroup.HasDetPlusMinusOne
+
+variable {K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K]
+  {𝒢 : Subgroup (GL (Fin 2) K)} [𝒢.HasDetPlusMinusOne]
+
+lemma isParabolic_iff_of_upperTriangular {g} (hg : g ∈ 𝒢) (hg10 : g 1 0 = 0) :
+    g.IsParabolic ↔ (∃ x ≠ 0, g = upperRightHom x) ∨ (∃ x ≠ 0, g = -upperRightHom x) :=
+  isParabolic_iff_of_upperTriangular_of_det (HasDetPlusMinusOne.det_eq hg) hg10
+
+end Subgroup.HasDetPlusMinusOne
+
 section IsCusp
 
 /-- The *cusps* of a subgroup of `GL(2, ℝ)` are the fixed points of parabolic elements of `g`. -/

Mathlib/Topology/Instances/Matrix.lean

@@ -8,7 +8,7 @@ import Mathlib.Topology.Algebra.Group.Pointwise
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Algebra.Star
 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
-import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
+import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
 import Mathlib.LinearAlgebra.Matrix.Trace
 
 /-!
@@ -461,6 +461,14 @@ namespace Matrix.GeneralLinearGroup
   simp_rw [Units.continuous_iff, ← map_inv]
   constructor <;> fun_prop
 
+lemma continuous_upperRightHom {R : Type*} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] :
+    Continuous (upperRightHom (R := R)) := by
+  simp only [continuous_induced_rng, Function.comp_def, upperRightHom_apply,
+    Units.embedProduct_apply, Units.inv_mk, continuous_prodMk, MulOpposite.unop_op]
+  constructor <;>
+  · refine continuous_matrix fun i j ↦ ?_
+    fin_cases i <;> fin_cases j <;> simp [continuous_const, continuous_neg, continuous_id']
+
 end Matrix.GeneralLinearGroup
 
 namespace Matrix.SpecialLinearGroup