The level-one modular group as a cofinite Fuchsian group

The effective group acting on the upper half-plane at level one is the image of PSL(2, ℤ) in PSL(2, ℝ), not SL(2, ℤ): the latter still contains the central matrix -I, which acts trivially. This file proves that the projective image is a discrete cofinite subgroup of PSL(2, ℝ).

The standard open modular fundamental domain is transported from the PSL(2, ℤ) action to its image in PSL(2, ℝ). Its finite hyperbolic area then proves cofiniteness. This supplies the effective level-one input for quotient and compactification constructions.

The elliptic data of the effective group are transported from PSL(2, ℤ) in the same way: the stabilizers of i and ρ have orders 2 and 3, and every point outside their two orbits has trivial stabilizer. So the free locus of the level-one quotient is the complement of exactly two orbits.

Main results

• TauCeti.ModularGroup.isFundamentalDomain_fdo_psl2zToPSL2RRange: the standard open modular domain is a fundamental domain for the projective image in PSL(2, ℝ).
• TauCeti.ModularGroup.isCofinite_psl2zToPSL2RRange: that image is a cofinite Fuchsian group.
• TauCeti.ModularGroup.card_stabilizer_psl2zToPSL2RRange_I and TauCeti.ModularGroup.card_stabilizer_psl2zToPSL2RRange_ρ: the elliptic orders 2 and 3.
• TauCeti.ModularGroup.quotientMk_psl2zToPSL2RRange_eq_iff_quotientMk_sl_eq: the orbits of the projective image are those of SL(2, ℤ).
• TauCeti.ModularGroup.stabilizer_psl2zToPSL2RRange_eq_bot_iff: a stabilizer is trivial exactly off the orbits of i and ρ.

References

• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §§2.3–2.4.
• Jean-Pierre Serre, A Course in Arithmetic, Graduate Texts in Mathematics 7, Springer, 1973, Chapter VII.

theorem TauCeti.ModularGroup.isFundamentalDomain_fdo_psl2zToPSL2RRange : MeasureTheory.IsFundamentalDomain (↥psl2zToPSL2R.range) ModularGroup.fdo MeasureTheory.volume

The standard open modular domain is a fundamental domain for the image of PSL(2, ℤ) in PSL(2, ℝ). It presents the effective level-one quotient and supplies the finite-area domain used to prove that the projective image is cofinite.

theorem TauCeti.ModularGroup.isCofinite_psl2zToPSL2RRange : psl2zToPSL2R.range.IsCofinite

The image of PSL(2, ℤ) in PSL(2, ℝ) is a cofinite Fuchsian group.

Elliptic points

theorem TauCeti.ModularGroup.card_stabilizer_psl2zToPSL2RRange_eq_card_stabilizer_psl (z : UpperHalfPlane) : Nat.card ↥(MulAction.stabilizer (↥psl2zToPSL2R.range) z) = Nat.card ↥(MulAction.stabilizer (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) z)

The point stabilizers of the effective level-one group are those of PSL(2, ℤ), transported along the injective homomorphism psl2zToPSL2R.

theorem TauCeti.ModularGroup.orbitRel_psl2zToPSL2RRange_iff_orbitRel_sl {z w : UpperHalfPlane} : (MulAction.orbitRel (↥psl2zToPSL2R.range) UpperHalfPlane) z w ↔ (MulAction.orbitRel (Matrix.SpecialLinearGroup (Fin 2) ℤ) UpperHalfPlane) z w

Two points lie in the same orbit of the effective level-one group exactly when they lie in the same orbit of SL(2, ℤ).

theorem TauCeti.ModularGroup.card_stabilizer_psl2zToPSL2RRange_I : Nat.card ↥(MulAction.stabilizer (↥psl2zToPSL2R.range) UpperHalfPlane.I) = 2

The stabilizer of i in the effective level-one group has order 2.

theorem TauCeti.ModularGroup.card_stabilizer_psl2zToPSL2RRange_ρ : Nat.card ↥(MulAction.stabilizer (↥psl2zToPSL2R.range) UpperHalfPlane.ρ) = 3

The stabilizer of ρ in the effective level-one group has order 3.

theorem TauCeti.ModularGroup.quotientMk_psl2zToPSL2RRange_eq_iff_quotientMk_sl_eq {z w : UpperHalfPlane} : ⟦z⟧ = ⟦w⟧ ↔ Quotient.mk'' z = Quotient.mk'' w

Two points have the same orbit under the effective level-one group exactly when they have the same orbit under SL(2, ℤ).

theorem TauCeti.ModularGroup.stabilizer_psl2zToPSL2RRange_eq_bot_iff (z : UpperHalfPlane) : MulAction.stabilizer (↥psl2zToPSL2R.range) z = ⊥ ↔ ⟦z⟧ ≠ ⟦UpperHalfPlane.I⟧ ∧ ⟦z⟧ ≠ ⟦UpperHalfPlane.ρ⟧

The elliptic points of the level-one group. The stabilizer of z in the effective level-one group is trivial exactly when z lies in neither the orbit of i nor that of ρ.