Documentation

TauCeti.NumberTheory.Modular.Orbits

Orbits of the modular group on the upper half-plane #

Every SL(2, ℤ)-orbit of ℍ has a representative in the standard fundamental domain, and translation by one preserves orbits. On the open domain the representative is moreover unique, so the orbit map is injective there. These are the orbit-space inputs of the valence formula: the first says a sum over orbits can be read off representatives, the last says doing so counts each orbit once.

On the closed domain 𝒟 the representative is not unique: z ↦ z + 1 identifies the two vertical edges and z ↦ -1/z folds the unit arc onto itself, fixing i and swapping ρ with ρ + 1. Mathlib's classification ModularGroup.cases_of_mem_fd_smul_mem_fd pins these identifications down, and here it yields the closed-domain complements: the elliptic orbits of i and ρ meet 𝒟 exactly at i and at {ρ, ρ + 1}, and every orbit meets the part of 𝒟 left of the identifications — 𝒟 without the right vertical edge and the part of the unit arc right of i — exactly once.

Main declarations #

References #

source
theorem TauCeti.ModularGroup.exists_rep_mem_fd (q : MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) UpperHalfPlane) :
∃ (p : UpperHalfPlane), Quotient.mk'' p = q ∧ p ∈ ModularGroup.fd

Every SL(2, ℤ)-orbit of ℍ has a representative in the standard fundamental domain.

source
@[simp]
theorem TauCeti.ModularGroup.orbit_mk_int_vadd (n : ℤ) (z : UpperHalfPlane) :
Quotient.mk'' (↑n +ᵥ z) = Quotient.mk'' z

Translation by any integer preserves the SL(2, ℤ)-orbit.

source
theorem TauCeti.ModularGroup.vadd_mem_fd_of_re_eq {r : ℝ} {p : UpperHalfPlane} (hp : p ∈ ModularGroup.fd) (hre : p.re = -r / 2) :
r +ᵥ p ∈ ModularGroup.fd

Translation by r carries a point of 𝒟 on the line re = -r / 2 into 𝒟.

source
theorem TauCeti.ModularGroup.orbit_mk_injOn_fdo :
Set.InjOn (fun (p : UpperHalfPlane) => Quotient.mk'' p) ModularGroup.fdo

Distinct points of the open fundamental domain lie in distinct SL(2, ℤ)-orbits: the orbit map is injective there. This is the Second Fundamental Domain Lemma (ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo) restated as injectivity, which is the form the orbit-indexed valence formula needs. It fails on the closed domain 𝒟, whose boundary is identified with itself by T and S.

The boundary identifications of the closed fundamental domain #

The values of the corner points and of the finitely many group elements that can move a point of 𝒟 inside 𝒟 (classified by ModularGroup.cases_of_mem_fd_smul_mem_fd).

source
theorem TauCeti.ModularGroup.norm_coe_S_smul (p : UpperHalfPlane) :
‖↑(ModularGroup.S • p)‖ = ‖↑p‖⁻¹

The inversion S scales the norm of every point by its reciprocal.

Not @[simp]: the simpNF linter rewrites the stated LHS ‖↑(ModularGroup.S • p)‖ through the unconditional simp lemma ModularGroup.sl_moeb to ‖↑((ModularGroup.S : GL (Fin 2) ℝ) • p)‖ (the GL (Fin 2) ℝ-lifted action), which is not how any call site in this development states the S-action, so tagging would make the lemma unusable via plain rw.

source
theorem TauCeti.ModularGroup.norm_coe_S_smul_of_norm_eq_one {p : UpperHalfPlane} (hp : ‖↑p‖ = 1) :
‖↑(ModularGroup.S • p)‖ = 1

The unit-circle specialization of norm_coe_S_smul: on the unit circle, S keeps the norm at 1.

source
theorem TauCeti.ModularGroup.re_S_smul_of_norm_eq_one {p : UpperHalfPlane} (hp : ‖↑p‖ = 1) :
(ModularGroup.S • p).re = -p.re

The unit-circle specialization of ModularGroup.re_S_smul: on the unit circle, S negates the real part.

source
theorem TauCeti.ModularGroup.S_smul_mem_fd_of_norm_eq_one {p : UpperHalfPlane} (hre : |p.re| ≤ 1 / 2) (hnorm : ‖↑p‖ = 1) :
ModularGroup.S • p ∈ ModularGroup.fd

On the unit circle a point with the fundamental domain's real-part bound is carried into the closed fundamental domain by the inversion: the norm stays at 1, and the real-part bound is symmetric under the sign flip.

source
@[simp]
theorem TauCeti.ModularGroup.orbit_mk_eq_I_iff {p : UpperHalfPlane} (hp : p ∈ ModularGroup.fd) :
Quotient.mk'' p = Quotient.mk'' UpperHalfPlane.I ↔ p = UpperHalfPlane.I

A point of the closed fundamental domain lying in the SL(2, ℤ)-orbit of i is i itself: the boundary identifications of 𝒟 fix i.

source
@[simp]
theorem TauCeti.ModularGroup.orbit_mk_eq_ρ_iff {p : UpperHalfPlane} (hp : p ∈ ModularGroup.fd) :
Quotient.mk'' p = Quotient.mk'' UpperHalfPlane.ρ ↔ p = UpperHalfPlane.ρ ∨ p = 1 +ᵥ UpperHalfPlane.ρ

A point of the closed fundamental domain lying in the SL(2, ℤ)-orbit of ρ is ρ or its translate ρ + 1: the two corners the boundary identifications of 𝒟 exchange.

source
theorem TauCeti.ModularGroup.orbit_mk_I_ne_orbit_mk_ρ :
Quotient.mk'' UpperHalfPlane.I ≠ Quotient.mk'' UpperHalfPlane.ρ

The two elliptic orbits are distinct.

source
theorem TauCeti.ModularGroup.orbit_mk_injOn_fd_left :
Set.InjOn (fun (p : UpperHalfPlane) => Quotient.mk'' p) {p : UpperHalfPlane | p ∈ ModularGroup.fd ∧ p.re < 1 / 2 ∧ (‖↑p‖ = 1 → p.re ≤ 0)}

The orbit map is injective on the part of 𝒟 left of the boundary identifications: the points with re < 1/2 which, if on the unit circle, have re ≤ 0. This drops the right vertical edge, which T identifies with the left one, and the arc right of i, which S folds onto the arc left of i while fixing i.

source
theorem TauCeti.ModularGroup.exists_smul_mem_fd_left (z : UpperHalfPlane) :
∃ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), g • z ∈ ModularGroup.fd ∧ (g • z).re < 1 / 2 ∧ (‖↑(g • z)‖ = 1 → (g • z).re ≤ 0)

Every SL(2, ℤ)-orbit of ℍ meets the part of 𝒟 left of the boundary identifications: the points with re < 1/2 which, if on the unit circle, have re ≤ 0.