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 = ℚ.)

source

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

source

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.

Equations

Instances For

source

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

IsCusp (g • c) (ConjAct.toConjAct g • 𝒢)

source

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

IsCusp (g • c) 𝒢

source

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

IsCusp c 𝒢' ↔ IsCusp c 𝒢

source

@[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.

source

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

IsCusp c 𝒢 ↔ IsCusp c 𝒢'

source

@[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.

source

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

IsCusp c ℋ

source

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

IsCusp c 𝒢

source

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.

source

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 ℙ¹(ℚ).

source

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 ∞.

source

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.

source

def cusps_subMulAction (𝒢 : Subgroup (GL (Fin 2) ℝ)) :

SubMulAction (↥𝒢) (OnePoint ℝ)

The action of 𝒢 on its own cusps.

Equations

Instances For

source

@[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.

Equations

Instances For

source

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.

Equations

Instances For

source

@[simp]

theorem cosetToCuspOrbit_apply_mk {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

cosetToCuspOrbit 𝒢 ⟦g⟧ = ⟦⟨(Matrix.SpecialLinearGroup.mapGL ℝ) g⁻¹ • OnePoint.infty, ⋯⟩⟧

source

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

Function.Surjective (cosetToCuspOrbit 𝒢)

source

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.