Documentation

TauCeti.Analysis.Complex.Fuchsian.Cusp.Tower

Cusp ramification indices in a tower of Fuchsian groups #

The ratio of compatible normalized cusp widths is a canonical positive natural number. For three nested groups this index multiplies, giving the exponent of the composite cusp map. The index is also the relative index of the two cusp stabilizers, so it does not depend on the chosen scaling.

The normalization of cusp widths follows Diamond and Shurman, A First Course in Modular Forms, §2.4.

source
theorem TauCeti.Subgroup.CuspDatum.width_factor_unique {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Δ.CuspDatum) (E : Γ.CuspDatum) {m n : ℕ} (hm : D.width = ↑m * E.width) (hn : D.width = ↑n * E.width) :
m = n

The integral ratio between two positive normalized cusp widths is unique.

source
theorem TauCeti.Subgroup.CuspDatum.width_factor_tower {Δ Γ Θ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Δ.CuspDatum) (E : Γ.CuspDatum) (F : Θ.CuspDatum) {m n : ℕ} (hm : D.width = ↑m * E.width) (hn : E.width = ↑n * F.width) :
D.width = ↑(m * n) * F.width

The exponent of the cusp width ratio multiplies in a subgroup tower.

source
noncomputable def TauCeti.Subgroup.CuspDatum.widthIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hc : D.cusp = E.cusp) (hσ : D.scaling = E.scaling) :
ℕ

The positive integer by which the cusp width grows under a subgroup inclusion, for normalized cusp data with the same representative and scaling.

Equations
Instances For
    source
    theorem TauCeti.Subgroup.CuspDatum.widthIndex_pos {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hc : D.cusp = E.cusp) (hσ : D.scaling = E.scaling) :
    0 < widthIndex h D E hc hσ

    The cusp width ratio is positive.

    source
    theorem TauCeti.Subgroup.CuspDatum.width_eq_widthIndex_mul {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hc : D.cusp = E.cusp) (hσ : D.scaling = E.scaling) :
    D.width = ↑(widthIndex h D E hc hσ) * E.width

    The smaller group's width is the cusp index times the larger group's width.

    source
    theorem TauCeti.Subgroup.CuspDatum.widthIndex_eq_relIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hc : D.cusp = E.cusp) (hσ : D.scaling = E.scaling) :
    widthIndex h D E hc hσ = (Δ.subgroupOf Γ).relIndex (MulAction.stabilizer (↥Γ) E.cusp)

    The cusp width index is the index of the cusp stabilizers. For compatible normalized cusp data, the factor by which the width grows under Δ ≤ Γ is the relative index of Δ in the stabilizer of the cusp in Γ, that is, [stabilizer Γ c : stabilizer Δ c]. The generator for Δ is the n-th power of the generator for Γ, and the infinite cyclic stabilizer for Γ contains its subgroup of n-th powers with index n.

    source
    @[simp]
    theorem TauCeti.Subgroup.CuspDatum.widthIndex_self {Δ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Δ.CuspDatum) :
    widthIndex ⋯ D D ⋯ ⋯ = 1

    The cusp index of the identity inclusion is one.

    source
    theorem TauCeti.Subgroup.CuspDatum.widthIndex_tower {Δ Γ Θ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (k : Γ ≤ Θ) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (F : Θ.CuspDatum) (hcDE : D.cusp = E.cusp) (hcEF : E.cusp = F.cusp) (hσDE : D.scaling = E.scaling) (hσEF : E.scaling = F.scaling) :
    widthIndex ⋯ D F ⋯ ⋯ = widthIndex h D E hcDE hσDE * widthIndex k E F hcEF hσEF

    The cusp ramification index multiplies in a tower of subgroup inclusions.