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 𝒢

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

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

instance instFactIsCuspInftyRealOfIsArithmetic {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] : Fact (IsCusp OnePoint.infty Γ)

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.

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

The action of 𝒢 on its own cusps.

Equations

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

@[simp]

theorem mem_cuspsSubMulAction {𝒢 : Subgroup (GL (Fin 2) ℝ)} {c : OnePoint ℝ} : c ∈ cuspsSubMulAction 𝒢 ↔ IsCusp c 𝒢

@[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 ↥𝒢 ↥(cuspsSubMulAction 𝒢)

noncomputable def CuspOrbits.map {G H : Subgroup (GL (Fin 2) ℝ)} (hGH : G ≤ H) : CuspOrbits G → CuspOrbits H

The map on cusp orbits induced by an inclusion of groups.

Equations

• CuspOrbits.map hGH = Quotient.map (fun (c : ↥(cuspsSubMulAction G)) => ⟨↑c, ⋯⟩) ⋯

@[simp]

theorem CuspOrbits.map_mk {G H : Subgroup (GL (Fin 2) ℝ)} (hGH : G ≤ H) (c : ↥(cuspsSubMulAction G)) : map hGH ⟦c⟧ = ⟦⟨↑c, ⋯⟩⟧

@[simp]

theorem CuspOrbits.map_map {G H K : Subgroup (GL (Fin 2) ℝ)} (hGH : G ≤ H) (hHK : H ≤ K) (c : CuspOrbits G) : map hHK (map hGH c) = map ⋯ c

theorem CuspOrbits.map_surjective {G H : Subgroup (GL (Fin 2) ℝ)} (hGH : G ≤ H) [G.IsFiniteRelIndex H] : Function.Surjective (map hGH)

Every cusp orbit lifts along an inclusion of finite relative index.

noncomputable def CuspOrbits.conj (G : Subgroup (GL (Fin 2) ℝ)) (g : GL (Fin 2) ℝ) : CuspOrbits G → CuspOrbits (ConjAct.toConjAct g • G)

Conjugation transports cusp orbits along the action on the projective line.

Equations

• CuspOrbits.conj G g = Quotient.map (fun (c : ↥(cuspsSubMulAction G)) => ⟨g • ↑c, ⋯⟩) ⋯

@[simp]

theorem CuspOrbits.conj_mk {G : Subgroup (GL (Fin 2) ℝ)} (g : GL (Fin 2) ℝ) (c : ↥(cuspsSubMulAction G)) : conj G g ⟦c⟧ = ⟦⟨g • ↑c, ⋯⟩⟧

theorem CuspOrbits.conj_bijective (G : Subgroup (GL (Fin 2) ℝ)) (g : GL (Fin 2) ℝ) : Function.Bijective (conj G g)

theorem CuspOrbits.map_conj {G H : Subgroup (GL (Fin 2) ℝ)} (hGH : G ≤ H) (g : GL (Fin 2) ℝ) (c : CuspOrbits G) : map ⋯ (conj G g c) = conj H g (map hGH c)

theorem CuspOrbits.map_adjoinNegOne_bijective (G : Subgroup (GL (Fin 2) ℝ)) : Function.Bijective (map ⋯)

The natural map from cusp orbits for G to those for G.adjoinNegOne is a bijection.

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.

@[reducible, inline]

noncomputable abbrev cuspOrbitInfty {𝒢 : Subgroup (GL (Fin 2) ℝ)} [Fact (IsCusp OnePoint.infty 𝒢)] : CuspOrbits 𝒢

The cusp ∞. (The Fact hypothesis is automatically supplied for arithmetic groups.)

Equations

• cuspOrbitInfty = ⟦⟨OnePoint.infty, ⋯⟩⟧

@[instance_reducible]

noncomputable instance instUniqueCuspOrbitsRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL : Unique (CuspOrbits (Matrix.SpecialLinearGroup.mapGL ℝ).range)

Equations

• instUniqueCuspOrbitsRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL = { default := cuspOrbitInfty, uniq := ⋯ }

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] ∈ 𝒢.

Equations

• 𝒢.strictPeriods = AddSubgroup.comap Matrix.GeneralLinearGroup.upperRightHom.toAddMonoidHom (Subgroup.toAddSubgroup 𝒢)

@[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] ∈ 𝒢.

Equations

• 𝒢.periods = 𝒢.adjoinNegOne.strictPeriods

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.

Equations

• 𝒢.IsRegularAtInfty = (𝒢.strictPeriods = 𝒢.periods)

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

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

The regularity factor at infinity: the index of the strict periods in the periods. It is 1 if 𝒢 is regular at ∞ and 2 otherwise.

Equations

• 𝒢.regularityFactorInfty = 𝒢.strictPeriods.relIndex 𝒢.periods

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

@[simp]

theorem Subgroup.regularityFactorInfty_eq_one_of_isRegularAtInfty {R : Type u_1} [Ring R] (𝒢 : Subgroup (GL (Fin 2) R)) (h : 𝒢.IsRegularAtInfty) : 𝒢.regularityFactorInfty = 1

@[simp]

theorem Subgroup.regularityFactorInfty_eq_two_of_not_isRegularAtInfty {R : Type u_1} [Ring R] (𝒢 : Subgroup (GL (Fin 2) R)) (h : ¬𝒢.IsRegularAtInfty) : 𝒢.regularityFactorInfty = 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.

Equations

• 𝒢.strictWidthInfty = if h : DiscreteTopology ↥𝒢.strictPeriods then |⋯.choose| else 0

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.

Equations

• 𝒢.widthInfty = 𝒢.adjoinNegOne.strictWidthInfty

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_of_strictPeriods_eq_zmultiples {𝒢 : Subgroup (GL (Fin 2) ℝ)} {x : ℝ} (hper : 𝒢.strictPeriods = AddSubgroup.zmultiples x) (hnonneg : 0 ≤ x) : 𝒢.strictWidthInfty = x

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

@[simp]

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

@[simp]

theorem Subgroup.widthInfty_SL2Z : (Matrix.SpecialLinearGroup.mapGL ℝ).range.widthInfty = 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_widthInfty_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.strictWidthInfty_eq_regularityFactorInfty_mul_widthInfty (𝒢 : Subgroup (GL (Fin 2) ℝ)) : 𝒢.strictWidthInfty = ↑𝒢.regularityFactorInfty * 𝒢.widthInfty

The strict width is the width multiplied by the regularity factor.

theorem Subgroup.strictWidthInfty_of_isRegularAtInfty (𝒢 : Subgroup (GL (Fin 2) ℝ)) (h𝒢 : 𝒢.IsRegularAtInfty) : 𝒢.strictWidthInfty = 𝒢.widthInfty

theorem Subgroup.strictWidthInfty_of_not_isRegularAtInfty (𝒢 : Subgroup (GL (Fin 2) ℝ)) (h𝒢 : ¬𝒢.IsRegularAtInfty) : 𝒢.strictWidthInfty = 2 * 𝒢.widthInfty

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

theorem Subgroup.mem_strictPeriods_conj_of_upperTriangular {G : Subgroup (GL (Fin 2) ℝ)} {g : GL (Fin 2) ℝ} (hg : ↑g 1 0 = 0) {x : ℝ} : x ∈ (ConjAct.toConjAct g⁻¹ • G).strictPeriods ↔ ↑g 0 0 / ↑g 1 1 * x ∈ G.strictPeriods

Translation parameters under an upper triangular change of cusp coordinate.

theorem Subgroup.strictWidthInfty_conj_of_upperTriangular (G : Subgroup (GL (Fin 2) ℝ)) [DiscreteTopology ↥G.strictPeriods] {g : GL (Fin 2) ℝ} (hg : ↑g 1 0 = 0) : (ConjAct.toConjAct g⁻¹ • G).strictWidthInfty = G.strictWidthInfty / |↑g 0 0 / ↑g 1 1|

Strict cusp widths scale inversely under an upper triangular change of coordinate.

theorem Subgroup.widthInfty_conj_of_upperTriangular (G : Subgroup (GL (Fin 2) ℝ)) [DiscreteTopology ↥G.periods] {g : GL (Fin 2) ℝ} (hg : ↑g 1 0 = 0) : (ConjAct.toConjAct g⁻¹ • G).widthInfty = G.widthInfty / |↑g 0 0 / ↑g 1 1|

Cusp widths scale inversely under an upper triangular change of coordinate.

theorem Subgroup.eq_upperRightHom_or_neg_of_upperTriangular {G : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥G] [G.HasDetOne] (hw : 0 < G.widthInfty) {g : GL (Fin 2) ℝ} (hgG : g ∈ G) (hg : ↑g 1 0 = 0) : g = Matrix.GeneralLinearGroup.upperRightHom (↑g 0 1) ∨ g = -Matrix.GeneralLinearGroup.upperRightHom (-↑g 0 1)

In a discrete determinant-one group with a cusp at infinity, every element fixing infinity is a signed translation.

@[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 : ℕ) : (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma N)).strictWidthInfty = ↑N