Canonical Representatives for Non-Elliptic Orbits

Every non-elliptic orbit with nonzero order of vanishing has a representative in the canonical finsets used by valence_formula_orbit_sum_s₀.

Main Results

• exists_repCanon_of_nonEllOrbit — For any non-elliptic orbit q with ordOrbit f q ≠ 0, there exists p ∈ repCanon f hf with orb p = q.

noncomputable def repStrict {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : Finset UpperHalfPlane

Strict interior representatives: points in s₀ with ‖p‖ > 1, |re| < 1/2, not elliptic.

Equations

• repStrict f hf = {p ∈ s₀ f hf | p ≠ ellipticPointI' ∧ p ≠ ellipticPointRho' ∧ p ≠ ellipticPointRhoPlusOne' ∧ ‖↑p‖ > 1 ∧ |(↑p).re| < 1 / 2}

noncomputable def repLeftVert {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : Finset UpperHalfPlane

Left vertical edge representatives: points in s₀ with re = -1/2, ‖p‖ > 1.

Equations

• repLeftVert f hf = sLeftVert (s₀ f hf)

noncomputable def repLeftArc {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : Finset UpperHalfPlane

Left arc representatives: points in s₀ with ‖p‖ = 1, re < 0, not ρ.

Equations

• repLeftArc f hf = {p ∈ s₀ f hf | p ≠ ellipticPointRho' ∧ ‖↑p‖ = 1 ∧ (↑p).re < 0}

noncomputable def repCanon {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : Finset UpperHalfPlane

The canonical representative finset: union of strict interior, left vertical, and left arc.

Equations

• repCanon f hf = repStrict f hf ∪ repLeftVert f hf ∪ repLeftArc f hf

theorem repStrict_mem_s₀ {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {p : UpperHalfPlane} (hp : p ∈ repStrict f hf) : p ∈ s₀ f hf

theorem repLeftVert_mem_s₀ {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {p : UpperHalfPlane} (hp : p ∈ repLeftVert f hf) : p ∈ s₀ f hf

theorem repLeftArc_mem_s₀ {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {p : UpperHalfPlane} (hp : p ∈ repLeftArc f hf) : p ∈ s₀ f hf

theorem repCanon_mem_s₀ {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {p : UpperHalfPlane} (hp : p ∈ repCanon f hf) : p ∈ s₀ f hf

theorem repCanon_mem_fd {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {p : UpperHalfPlane} (hp : p ∈ repCanon f hf) : p ∈ ModularGroup.fd

theorem orb_vAdd_neg_one_eq (p : UpperHalfPlane) : orb (-1 +ᵥ p) = orb p

T⁻¹-translation preserves orbits: orb((-1)+ᵥp) = orb(p).

theorem orb_S_smul_eq (p : UpperHalfPlane) : orb (ModularGroup.S • p) = orb p

S-action preserves orbits: orb(S • p) = orb(p).

theorem exists_repCanon_of_nonEllOrbit {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (q : NonEllOrbit) : ordOrbit f ↑q ≠ 0 → ∃ p ∈ repCanon f hf, orb p = ↑q

Every non-elliptic orbit with nonzero order has a representative in repCanon.