Theorems · Definition · number theory

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.

Defined in

Mathlib.NumberTheory.ModularForms.Cusps

Cited by

3 results in Mathlib

Foundations

Depth 164 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Subgroup.IsArithmetic