Documentation

TauCeti.NumberTheory.ModularForms.Cusps.ModularGroup

Modular-group action on rational cusps #

The standard generators S and T, and their product T * S, act on rational cusps by Möbius transformations. These evaluations describe the edges in the Manin-symbol relations.

source
theorem TauCeti.exists_smul_zero_smul_infty {a b : OnePoint ℚ} (h : a ≠ b) :
∃ (g : GL (Fin 2) ℚ), 0 < (↑g).det ∧ g • ↑0 = a ∧ g • OnePoint.infty = b

Any two distinct rational cusps are the images of 0 and ∞ under a rational matrix of positive determinant.

source
@[simp]
theorem TauCeti.mapGL_S_smul_infty :
(Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.S • OnePoint.infty = ↑0

S sends ∞ to 0 under the Möbius action.

source
@[simp]
theorem TauCeti.mapGL_S_smul_zero :
(Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.S • ↑0 = OnePoint.infty

S sends 0 to ∞ under the Möbius action.

source
@[simp]
theorem TauCeti.mapGL_T_smul_infty :
(Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T • OnePoint.infty = OnePoint.infty

T fixes ∞ under the Möbius action.

source
@[simp]
theorem TauCeti.mapGL_T_smul_coe (k : ℚ) :
(Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T • ↑k = ↑(k + 1)

T translates an affine cusp by one.

source
@[simp]
theorem TauCeti.mapGL_T_mul_S_smul_infty :
((Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T * (Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.S) • OnePoint.infty = ↑1

T * S sends ∞ to 1.

source
@[simp]
theorem TauCeti.mapGL_T_mul_S_smul_zero :
((Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T * (Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.S) • ↑0 = OnePoint.infty

T * S sends 0 to ∞.

source
@[simp]
theorem TauCeti.mapGL_T_mul_S_smul_one :
((Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T * (Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.S) • ↑1 = ↑0

T * S sends 1 to 0.

source
@[simp]
theorem TauCeti.mapGL_T_mul_S_sq_smul_infty :
((Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T * (Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.S) ^ 2 • OnePoint.infty = ↑0

(T * S)² sends ∞ to 0.

source
@[simp]
theorem TauCeti.mapGL_T_mul_S_sq_smul_zero :
((Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T * (Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.S) ^ 2 • ↑0 = ↑1

(T * S)² sends 0 to 1.