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.

Equations

• IsCusp c 𝒢 = ∃ g ∈ 𝒢, g.IsParabolic ∧ g • c = c

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_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, ℤ).

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

The action of 𝒢 on its own cusps.

Equations

• cusps_subMulAction 𝒢 = { carrier := {c : OnePoint ℝ | IsCusp c 𝒢}, smul_mem' := ⋯ }

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

• CuspOrbits 𝒢 = MulAction.orbitRel.Quotient ↥𝒢 ↥(cusps_subMulAction 𝒢)

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

• cosetToCuspOrbit 𝒢 = Quotient.lift (fun (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) => ⟦⟨(Matrix.SpecialLinearGroup.mapGL ℝ) g⁻¹ • OnePoint.infty, ⋯⟩⟧) ⋯

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