Cusps

We define the cusps of a subgroup of GL(2, ℝ) as the fixed points of parabolic elements.

theorem OnePoint.exists_mem_SL2 {K : Type u_1} [Field K] [DecidableEq K] (A : Type u_2) [CommRing A] [IsDomain A] [Algebra A K] [IsFractionRing A K] [IsPrincipalIdealRing A] (c : OnePoint K) : ∃ (g : Matrix.SpecialLinearGroup (Fin 2) A), (Matrix.SpecialLinearGroup.mapGL K) g • infty = c

The modular group SL(2, A) acts transitively on OnePoint K, if A is a PID whose fraction field is K. (This includes the case A = ℤ, K = ℚ.)

theorem Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {𝒢 : Subgroup (GL (Fin 2) K)} [𝒢.HasDetPlusMinusOne] {g : GL (Fin 2) K} (hg : g ∈ 𝒢) (hg10 : ↑g 1 0 = 0) : g.IsParabolic ↔ (∃ (x : K), x ≠ 0 ∧ g = Matrix.GeneralLinearGroup.upperRightHom x) ∨ ∃ (x : K), x ≠ 0 ∧ g = -Matrix.GeneralLinearGroup.upperRightHom x

def IsCusp (c : OnePoint ℝ) (𝒢 : Subgroup (GL (Fin 2) ℝ)) : Prop

The cusps of a subgroup of GL(2, ℝ) are the fixed points of parabolic elements of g.

theorem IsCusp.smul {c : OnePoint ℝ} {𝒢 : Subgroup (GL (Fin 2) ℝ)} (hc : IsCusp c 𝒢) (g : GL (Fin 2) ℝ) : IsCusp (g • c) (ConjAct.toConjAct g • 𝒢)

theorem IsCusp.smul_of_mem {c : OnePoint ℝ} {𝒢 : Subgroup (GL (Fin 2) ℝ)} (hc : IsCusp c 𝒢) {g : GL (Fin 2) ℝ} (hg : g ∈ 𝒢) : IsCusp (g • c) 𝒢

theorem isCusp_iff_of_relIndex_ne_zero {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)} (h𝒢 : 𝒢' ≤ 𝒢) (h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0) (c : OnePoint ℝ) : IsCusp c 𝒢' ↔ IsCusp c 𝒢

@[deprecated isCusp_iff_of_relIndex_ne_zero (since := "2025-09-13")]

theorem isCusp_iff_of_relindex_ne_zero {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)} (h𝒢 : 𝒢' ≤ 𝒢) (h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0) (c : OnePoint ℝ) : IsCusp c 𝒢' ↔ IsCusp c 𝒢

Alias of isCusp_iff_of_relIndex_ne_zero.

theorem Subgroup.Commensurable.isCusp_iff {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)} (h𝒢 : 𝒢.Commensurable 𝒢') {c : OnePoint ℝ} : IsCusp c 𝒢 ↔ IsCusp c 𝒢'

@[deprecated Subgroup.Commensurable.isCusp_iff (since := "2025-09-17")]

theorem Commensurable.isCusp_iff {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)} (h𝒢 : 𝒢.Commensurable 𝒢') {c : OnePoint ℝ} : IsCusp c 𝒢 ↔ IsCusp c 𝒢'

Alias of Subgroup.Commensurable.isCusp_iff.

theorem IsCusp.mono {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {c : OnePoint ℝ} (hGH : 𝒢 ≤ ℋ) (hc : IsCusp c 𝒢) : IsCusp c ℋ

theorem IsCusp.of_isFiniteRelIndex {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {c : OnePoint ℝ} [𝒢.IsFiniteRelIndex ℋ] (hc : IsCusp c ℋ) : IsCusp c 𝒢

theorem IsCusp.of_isFiniteRelIndex_conj {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {c : OnePoint ℝ} [𝒢.IsFiniteRelIndex ℋ] (hc : IsCusp c ℋ) {h : GL (Fin 2) ℝ} (hh : h ∈ ℋ) : IsCusp c (ConjAct.toConjAct h • 𝒢)

Variant version of IsCusp.of_isFiniteRelIndex.

theorem isCusp_SL2Z_iff {c : OnePoint ℝ} : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range ↔ c ∈ Set.range (OnePoint.map Rat.cast)

The cusps of SL(2, ℤ) are precisely the elements of ℙ¹(ℚ).

theorem isCusp_SL2Z_iff' {c : OnePoint ℝ} : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range ↔ ∃ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), c = (Matrix.SpecialLinearGroup.mapGL ℝ) g • OnePoint.infty

The cusps of SL(2, ℤ) are precisely the SL(2, ℤ) orbit of ∞.

theorem Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] {c : OnePoint ℝ} : IsCusp c 𝒢 ↔ IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range

The cusps of any arithmetic subgroup are the same as those of SL(2, ℤ).

Cusp orbits

We consider the orbits for the action of 𝒢 on its own cusps. The main result is that if [𝒢.IsArithmetic] holds, then this set is finite.

def cusps_subMulAction (𝒢 : Subgroup (GL (Fin 2) ℝ)) : SubMulAction (↥𝒢) (OnePoint ℝ)

The action of 𝒢 on its own cusps.

@[reducible, inline]

abbrev CuspOrbits (𝒢 : Subgroup (GL (Fin 2) ℝ)) : Type

The type of cusp orbits of 𝒢, i.e. orbits for the action of 𝒢 on its own cusps.

noncomputable def cosetToCuspOrbit (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] : Matrix.SpecialLinearGroup (Fin 2) ℤ ⧸ Subgroup.comap (Matrix.SpecialLinearGroup.mapGL ℝ) 𝒢 → CuspOrbits 𝒢

Surjection from SL(2, ℤ) / (𝒢 ⊓ SL(2, ℤ)) to cusp orbits of 𝒢. Mostly useful for showing that CuspOrbits 𝒢 is finite for arithmetic subgroups.

@[simp]

theorem cosetToCuspOrbit_apply_mk {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : cosetToCuspOrbit 𝒢 ⟦g⟧ = ⟦⟨(Matrix.SpecialLinearGroup.mapGL ℝ) g⁻¹ • OnePoint.infty, ⋯⟩⟧

theorem surjective_cosetToCuspOrbit (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] : Function.Surjective (cosetToCuspOrbit 𝒢)

instance instFiniteCuspOrbitsOfIsArithmetic (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] : Finite (CuspOrbits 𝒢)

An arithmetic subgroup has finitely many cusp orbits.

Width of a cusp

We define the strict width of 𝒢 at ∞ to be the smallest h > 0 such that [1, h; 0, 1] ∈ 𝒢, or 0 if no such h exists; and the width of 𝒢 to be the strict width of the subgroup generated by 𝒢 and -1, or equivalently the smallest h > 0 such that ±[1, h; 0, 1] ∈ 𝒢 (again, if it exists). We show both widths exist when 𝒢 is discrete and has det ± 1.

def Subgroup.strictPeriods {R : Type u_1} [Ring R] (𝒢 : Subgroup (GL (Fin 2) R)) : AddSubgroup R

For a subgroup 𝒢 of GL(2, R), this is the additive group of x : R such that [1, x; 0, 1] ∈ 𝒢.

@[simp]

theorem Subgroup.mem_strictPeriods_iff {R : Type u_1} [Ring R] {𝒢 : Subgroup (GL (Fin 2) R)} {x : R} : x ∈ 𝒢.strictPeriods ↔ Matrix.GeneralLinearGroup.upperRightHom x ∈ 𝒢

noncomputable def Subgroup.periods {R : Type u_1} [Ring R] (𝒢 : Subgroup (GL (Fin 2) R)) : AddSubgroup R

For a subgroup 𝒢 of GL(2, R), this is the additive group of x : R such that ±[1, x; 0, 1] ∈ 𝒢.

theorem Subgroup.strictPeriods_le_periods {R : Type u_1} [Ring R] (𝒢 : Subgroup (GL (Fin 2) R)) : 𝒢.strictPeriods ≤ 𝒢.periods

def Subgroup.IsRegularAtInfty {R : Type u_1} [Ring R] (𝒢 : Subgroup (GL (Fin 2) R)) : Prop

A subgroup is regular at ∞ if its periods and strict periods coincide.

theorem Subgroup.IsRegularAtInfty.eq {R : Type u_1} [Ring R] (𝒢 : Subgroup (GL (Fin 2) R)) (h : 𝒢.IsRegularAtInfty) : 𝒢.strictPeriods = 𝒢.periods

theorem Subgroup.relIndex_strictPeriods {R : Type u_1} [Ring R] (𝒢 : Subgroup (GL (Fin 2) R)) : 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

theorem Subgroup.commensurable_strictPeriods_periods {R : Type u_1} [Ring R] (𝒢 : Subgroup (GL (Fin 2) R)) : 𝒢.strictPeriods.Commensurable 𝒢.periods

theorem Subgroup.strictPeriods_eq_periods_of_neg_one_mem {R : Type u_1} [Ring R] {𝒢 : Subgroup (GL (Fin 2) R)} (h𝒢 : -1 ∈ 𝒢) : 𝒢.strictPeriods = 𝒢.periods

theorem Subgroup.isRegularAtInfty_of_neg_one_mem {R : Type u_1} [Ring R] {𝒢 : Subgroup (GL (Fin 2) R)} (h𝒢 : -1 ∈ 𝒢) : 𝒢.IsRegularAtInfty

instance Subgroup.instDiscreteTopStrictPeriods {R : Type u_1} [Ring R] {𝒢 : Subgroup (GL (Fin 2) R)} [TopologicalSpace R] [IsTopologicalRing R] [hG : DiscreteTopology ↥𝒢] : DiscreteTopology ↥𝒢.strictPeriods

If 𝒢 is discrete, so is its strict period subgroup.

instance Subgroup.instDiscreteTopPeriods {R : Type u_1} [Ring R] {𝒢 : Subgroup (GL (Fin 2) R)} [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] [hG : DiscreteTopology ↥𝒢] : DiscreteTopology ↥𝒢.periods

If 𝒢 is discrete, so is its period subgroup.

theorem Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : ModularGroup.T ∈ Γ) : (map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1

@[simp]

theorem Subgroup.strictPeriods_SL2Z : (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods = AddSubgroup.zmultiples 1

noncomputable def Subgroup.strictWidthInfty (𝒢 : Subgroup (GL (Fin 2) ℝ)) : ℝ

The strict width of the cusp ∞, i.e. the x such that 𝒢.strictPeriods = zmultiples x, or 0 if no such x exists.

theorem Subgroup.strictWidthInfty_nonneg (𝒢 : Subgroup (GL (Fin 2) ℝ)) : 0 ≤ 𝒢.strictWidthInfty

noncomputable def Subgroup.widthInfty (𝒢 : Subgroup (GL (Fin 2) ℝ)) : ℝ

The width of the cusp ∞, i.e. the x such that 𝒢.periods = zmultiples x, or 0 if no such x exists.

theorem Subgroup.widthInfty_nonneg (𝒢 : Subgroup (GL (Fin 2) ℝ)) : 0 ≤ 𝒢.widthInfty

theorem Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.strictPeriods] : 𝒢.strictPeriods = AddSubgroup.zmultiples 𝒢.strictWidthInfty

theorem Subgroup.strictWidthInfty_eq_one_of_T_mem {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hΓ : ModularGroup.T ∈ Γ) : (map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).strictWidthInfty = 1

theorem Subgroup.strictWidthInfty_SL2Z : (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictWidthInfty = 1

theorem Subgroup.strictWidthInfty_mem_strictPeriods (𝒢 : Subgroup (GL (Fin 2) ℝ)) : 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods

theorem Subgroup.periods_eq_zmultiples_widthInfty {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.periods] : 𝒢.periods = AddSubgroup.zmultiples 𝒢.widthInfty

theorem Subgroup.widthInfty_mem_periods (𝒢 : Subgroup (GL (Fin 2) ℝ)) : 𝒢.widthInfty ∈ 𝒢.periods

theorem Subgroup.two_mul_withInfty_mem_strictPeriods (𝒢 : Subgroup (GL (Fin 2) ℝ)) : 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

theorem Subgroup.strictWidthInfty_pos_iff {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.strictPeriods] [𝒢.HasDetPlusMinusOne] : 0 < 𝒢.strictWidthInfty ↔ IsCusp OnePoint.infty 𝒢

theorem Subgroup.strictWidthInfty_pos (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] : 0 < 𝒢.strictWidthInfty

theorem Subgroup.isCusp_of_mem_strictPeriods {𝒢 : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (h𝒢 : h ∈ 𝒢.strictPeriods) : IsCusp OnePoint.infty 𝒢

theorem Subgroup.widthInfty_pos_iff {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.periods] [𝒢.HasDetPlusMinusOne] : 0 < 𝒢.widthInfty ↔ IsCusp OnePoint.infty 𝒢

theorem Subgroup.isRegularAtInfty_iff {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.periods] : 𝒢.IsRegularAtInfty ↔ 𝒢.widthInfty ∈ 𝒢.strictPeriods

theorem Subgroup.widthInfty_pos (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] : 0 < 𝒢.widthInfty

@[simp]

theorem CongruenceSubgroup.strictPeriods_Gamma0 (N : ℕ) : (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma0 N)).strictPeriods = AddSubgroup.zmultiples 1

@[simp]

theorem CongruenceSubgroup.strictPeriods_Gamma1 (N : ℕ) : (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma1 N)).strictPeriods = AddSubgroup.zmultiples 1

@[simp]

theorem CongruenceSubgroup.strictWidthInfty_Gamma0 (N : ℕ) : (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma0 N)).strictWidthInfty = 1

@[simp]

theorem CongruenceSubgroup.strictWidthInfty_Gamma1 (N : ℕ) : (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma1 N)).strictWidthInfty = 1

@[simp]

theorem CongruenceSubgroup.strictPeriods_Gamma (N : ℕ) : (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma N)).strictPeriods = AddSubgroup.zmultiples ↑N

@[simp]

theorem CongruenceSubgroup.strictWidthInfty_Gamma (N : ℕ) [NeZero N] : (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma N)).strictWidthInfty = ↑N