Documentation

TauCeti.NumberTheory.ModularForms.Cusps.Basic

The integer cusp width of a finite-index subgroup #

The image of T = [1, 1; 0, 1] in GL(2, โ„) and its powers are the upper-triangular shift matrices; a subgroup ๐’ข of finite relative index in ๐’ฎโ„’ contains some positive power of T, and Subgroup.integerCuspWidth ๐’ข is the least such exponent. The cosets of the first Subgroup.integerCuspWidth ๐’ข powers of T are pairwise distinct in ๐’ฎโ„’ โงธ ๐’ข โŠ“ ๐’ฎโ„’, and the integer cusp width is a positive integer multiple of the strict width at โˆž.

Main declarations #

References #

source
@[simp]
theorem TauCeti.ModularGroup.mapGL_T_zpow_eq_upperRightHom {S : Type u_1} [CommRing S] (n : โ„ค) :
(Matrix.SpecialLinearGroup.mapGL S) (ModularGroup.T ^ n) = Matrix.GeneralLinearGroup.upperRightHom โ†‘n

The image of T ^ n : SL(2, โ„ค) in GL(2, S) for any commutative ring S is the upper-triangular matrix [1, n; 0, 1].

source
@[simp]
theorem TauCeti.ModularGroup.mapGL_T_pow_eq_upperRightHom {S : Type u_1} [CommRing S] (n : โ„•) :
(Matrix.SpecialLinearGroup.mapGL S) (ModularGroup.T ^ n) = Matrix.GeneralLinearGroup.upperRightHom โ†‘n

The image of T ^ n : SL(2, โ„ค) in GL(2, S), for a natural exponent.

source
theorem TauCeti.Matrix.SpecialLinearGroup.coe_GL_eq_mapGL (g : Matrix.SpecialLinearGroup (Fin 2) โ„ค) :
Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom โ„)) g) = (Matrix.SpecialLinearGroup.mapGL โ„) g

The coercion of SL(2, โ„ค) into GL(2, โ„) agrees with mapGL โ„.

source
theorem TauCeti.Matrix.GeneralLinearGroup.upperRightHom_smul (x : โ„) (ฯ„ : UpperHalfPlane) :
Matrix.GeneralLinearGroup.upperRightHom x โ€ข ฯ„ = x +แตฅ ฯ„

The Mรถbius action of upperRightHom x = [1, x; 0, 1] on โ„ is the shift x +แตฅ ยท.

source
theorem TauCeti.ModularForm.slash_upperRightHom_apply (k : โ„ค) (x : โ„) (g : UpperHalfPlane โ†’ โ„‚) (ฯ„ : UpperHalfPlane) :
SlashAction.map k (Matrix.GeneralLinearGroup.upperRightHom x) g ฯ„ = g (x +แตฅ ฯ„)

Slashing a function g : โ„ โ†’ โ„‚ by the shift matrix [1, x; 0, 1] is the shift ฯ„ โ†ฆ g (x +แตฅ ฯ„).

source
theorem TauCeti.ModularForm.slash_T_zpow_apply (k j : โ„ค) (g : UpperHalfPlane โ†’ โ„‚) (ฯ„ : UpperHalfPlane) :
SlashAction.map k (ModularGroup.T ^ j) g ฯ„ = g (โ†‘j +แตฅ ฯ„)

Acting on a function g : โ„ โ†’ โ„‚ by T ^ j via the weight k slash action is the shift ฯ„ โ†ฆ g ((j : โ„) +แตฅ ฯ„).

source
@[simp]
theorem TauCeti.Subgroup.mk_T_pow_eq_iff {๐’ข : Subgroup (GL (Fin 2) โ„)} {n : โ„•} :
โŸฆ(Matrix.SpecialLinearGroup.mapGL โ„).rangeRestrict ModularGroup.T ^ nโŸง = โŸฆ1โŸง โ†” โ†‘n โˆˆ ๐’ข.strictPeriods

The coset of a power of T is the base coset exactly when the exponent is a strict period of ๐’ข: the bridge between the coset space and the strict periods, stated without reference to the group action.

source
theorem TauCeti.Subgroup.exists_pos_nat_mem_strictPeriods (๐’ข : Subgroup (GL (Fin 2) โ„)) [๐’ข.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL โ„).range] :
โˆƒ (n : โ„•), 0 < n โˆง โ†‘n โˆˆ ๐’ข.strictPeriods

A subgroup of GL(2, โ„) of finite relative index in ๐’ฎโ„’ always has a positive natural number in its strict periods: some positive power of T lands in the subgroup.

source
noncomputable def TauCeti.Subgroup.integerCuspWidth (๐’ข : Subgroup (GL (Fin 2) โ„)) :
โ„•

The MulAction.period of the coset of T acting on the base coset of ๐’ฎโ„’ โงธ ๐’ข โŠ“ ๐’ฎโ„’. When some positive power of T lies in ๐’ข โ€” in particular whenever ๐’ข has finite relative index in ๐’ฎโ„’, see Subgroup.integerCuspWidth_pos โ€” this is the smallest positive integer n such that the upper-triangular matrix [1, n; 0, 1] lies in ๐’ข; otherwise it is 0.

Equations
Instances For
    source
    theorem TauCeti.Subgroup.integerCuspWidth_pos {๐’ข : Subgroup (GL (Fin 2) โ„)} [๐’ข.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL โ„).range] :
    0 < integerCuspWidth ๐’ข

    The integer cusp width is positive.

    source
    theorem TauCeti.Subgroup.integerCuspWidth_mem_strictPeriods {๐’ข : Subgroup (GL (Fin 2) โ„)} :
    โ†‘(integerCuspWidth ๐’ข) โˆˆ ๐’ข.strictPeriods

    The integer cusp width is a strict period.

    source
    theorem TauCeti.Subgroup.isCusp_infty_of_finiteRelIndex {๐’ข : Subgroup (GL (Fin 2) โ„)} [๐’ข.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL โ„).range] :
    IsCusp OnePoint.infty ๐’ข

    โˆž is a cusp of a subgroup of finite relative index in ๐’ฎโ„’: its integer cusp width is a positive strict period, which is exactly the criterion.

    This is the group-theoretic half of every "a form for ๐’ข is bounded at โˆž" argument; the form-theoretic half is one application of ModularFormClass.bdd_at_cusps on top of it.

    source
    theorem TauCeti.Subgroup.integerCuspWidth_le {๐’ข : Subgroup (GL (Fin 2) โ„)} {n : โ„•} (hpos : 0 < n) (hmem : โ†‘n โˆˆ ๐’ข.strictPeriods) :
    integerCuspWidth ๐’ข โ‰ค n

    The integer cusp width is minimal among positive integer strict periods.

    source
    theorem TauCeti.Subgroup.T_pow_integerCuspWidth_mem {๐’ข : Subgroup (GL (Fin 2) โ„)} :
    Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom โ„)) ModularGroup.T) ^ integerCuspWidth ๐’ข โˆˆ ๐’ข

    The integerCuspWidth ๐’ข-th power of T lies in ๐’ข.

    source
    theorem TauCeti.Subgroup.natCast_mem_strictPeriods_iff {๐’ข : Subgroup (GL (Fin 2) โ„)} {n : โ„•} :
    โ†‘n โˆˆ ๐’ข.strictPeriods โ†” integerCuspWidth ๐’ข โˆฃ n

    The natural numbers among the strict periods are exactly the multiples of the integer cusp width.

    source
    @[simp]
    theorem TauCeti.Subgroup.T_pow_mem_iff {๐’ข : Subgroup (GL (Fin 2) โ„)} {n : โ„•} :
    Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom โ„)) ModularGroup.T) ^ n โˆˆ ๐’ข โ†” integerCuspWidth ๐’ข โˆฃ n

    The powers of T lying in ๐’ข are exactly those with exponent divisible by the integer cusp width.

    source
    theorem TauCeti.Subgroup.quotient_T_pow_integerCuspWidth_injective {๐’ข : Subgroup (GL (Fin 2) โ„)} :
    Function.Injective fun (j : Fin (integerCuspWidth ๐’ข)) => โŸฆ(Matrix.SpecialLinearGroup.mapGL โ„).rangeRestrict (ModularGroup.T ^ โ†‘j)โŸง

    The cosets T ^ j โ€ข (๐’ข โŠ“ ๐’ฎโ„’) for j < integerCuspWidth ๐’ข are pairwise distinct in ๐’ฎโ„’ โงธ ๐’ข.subgroupOf ๐’ฎโ„’.

    source
    theorem TauCeti.Subgroup.exists_pos_nat_integerCuspWidth_eq_mul_strictWidthInfty {๐’ข : Subgroup (GL (Fin 2) โ„)} [๐’ข.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL โ„).range] [DiscreteTopology โ†ฅ๐’ข.strictPeriods] :
    โˆƒ (m : โ„•), 0 < m โˆง โ†‘(integerCuspWidth ๐’ข) = โ†‘m * ๐’ข.strictWidthInfty

    The integer cusp width is a positive integer multiple of the strict width at โˆž.

    The strict period 1 of ฮ“โ‚(N) #

    source
    theorem TauCeti.one_mem_strictPeriods_Gamma1_map (N : โ„•) :
    1 โˆˆ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL โ„) (CongruenceSubgroup.Gamma1 N)).strictPeriods

    1 is a strict period of ฮ“โ‚(N), viewed in GL (Fin 2) โ„.

    This is the side condition the period-1 q-expansion API asks for at every congruence level โ€” ModularForm.qExpansion_smul, qExpansion_levelRaise_coeff and isCusp_of_mem_strictPeriods all take it as a hypothesis โ€” so it is named here rather than reproved at each use site.