Compactness of the level-one modular compactification

The modular group has one cusp orbit, represented by infinity. Its standard closed fundamental domain has a compact truncation at each height. These two facts turn the general compactness criterion for Fuchsian compactifications into compactness of the level-one carrier.

Mathlib's ModularGroup.isCompact_truncatedFundamentalDomain supplies the geometric compact set, and isCusp_SL2Z_iff' supplies the classification of modular cusps.

Main results

• TauCeti.ModularGroup.cuspOrbitInfty and instUniqueCuspOrbit: the unique modular cusp orbit.
• TauCeti.ModularGroup.compactSpace_compactifiedQuotient: compactness of the level-one compactified quotient.

References

• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, §2.4.

theorem TauCeti.ModularGroup.cuspPoint_mem_orbit_infty {c : OnePoint ℝ} (hc : psl2zToPSL2R.range.IsCuspPoint c) : c ∈ MulAction.orbit (↥psl2zToPSL2R.range) OnePoint.infty

Every cusp of the effective level-one modular group is equivalent to infinity.

theorem TauCeti.ModularGroup.isCuspPoint_infty : psl2zToPSL2R.range.IsCuspPoint OnePoint.infty

Infinity is a cusp point of the effective level-one modular group.

noncomputable def TauCeti.ModularGroup.cuspOrbitInfty : psl2zToPSL2R.range.CuspOrbit

The unique cusp orbit of the effective level-one modular group, represented by infinity.

Equations

• TauCeti.ModularGroup.cuspOrbitInfty = Subgroup.cuspOrbitMk ⟨OnePoint.infty, TauCeti.ModularGroup.cuspOrbitInfty._proof_4✝⟩

@[simp]

theorem TauCeti.ModularGroup.cuspOrbitInfty_val : ↑cuspOrbitInfty = Quotient.mk'' OnePoint.infty

@[instance_reducible]

noncomputable instance TauCeti.ModularGroup.instUniqueCuspOrbit : Unique psl2zToPSL2R.range.CuspOrbit

The effective level-one modular group has exactly one cusp orbit.

Equations

• TauCeti.ModularGroup.instUniqueCuspOrbit = { default := TauCeti.ModularGroup.cuspOrbitInfty, uniq := ⋯ }

@[simp]

theorem TauCeti.ModularGroup.cuspDatumInfty_cuspOrbit : cuspDatumInfty.cuspOrbit = cuspOrbitInfty

instance TauCeti.ModularGroup.compactSpace_compactifiedQuotient : CompactSpace psl2zToPSL2R.range.CompactifiedQuotient

The level-one modular orbit space becomes compact after its unique cusp orbit is adjoined. The compact sets used here are Mathlib's truncated closed modular fundamental domains.