Documentation

TauCeti.NumberTheory.HeckeRing.GL2.Gamma0.Diagonal.Composite

The composite diagonal element of the Γ₀(N) Hecke ring #

Diagonal/PrimePower.lean builds the generator T_p and the family T_{p^r} that the Diamond–Shurman recurrence produces, and closes by naming its own gap: "the composite element assembled over a prime factorisation is [not] proved here". This file assembles it.

heckeTCompositeGamma0 N n multiplies the blocks heckeTGeneratorRecGamma0 N p (v_p n) over the primes of n, least prime first. The assembly is TauCeti.Nat.primePowerProd rather than n.factorization.prod: a Finsupp.prod needs a CommMonoid instance, and the Hecke ring 𝕋 (Δ₀(N)) (Γ₀(N)) ℤ carries only a Ring one — its commutativity is a theorem about the Atkin–Lehner anti-involution, not a structure field. The ordered product asks only for One and Mul — its bracketing is fixed, so neither associativity nor a unit law enters — and so is available now.

The block map is heckeTGeneratorRecGamma0 N applied directly, with no primality guard. That is exactly what Diagonal/PrimePower.lean bought by dropping Nat.Prime p from the recurrence: the family is total in p, so it is a block map, and the composite needs no dite over primality and no junk branch to reason around. The primality of n.minFac still does all the mathematical work — it is what heckeTCompositeGamma0_prime_pow runs on — but it enters as a hypothesis of the lemmas rather than as a guard inside the definition.

What this file adds to the per-prime theory #

The per-prime product formula is heckeTGeneratorRecGamma0_mul, in Diagonal/PrimePower.lean, a statement about the recurrence family with no assembly in it. This file assembles it over a factorisation, in two forms: multiplicativity at coprime arguments, and the full divisor table at arbitrary nonzero ones. Both rest on the commutativity of the Γ₀(N) Hecke ring, which comes from the Atkin–Lehner anti-involution.

Main definitions #

Main results #

References #

source
noncomputable def HeckeRing.GL2.heckeTCompositeGamma0 (N : ℕ) [NeZero N] (n : ℕ) :
HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ℤ

The composite element of the Γ₀(N) Hecke ring attached to n: the product of the prime-power blocks heckeTGeneratorRecGamma0 N p (n.factorization p) over the primes p ∣ n, taken least prime first. At a prime p this is the generator T_p, at a prime power p ^ v the v-th term of the Diamond–Shurman recurrence, and at 1 — as at the junk input 0 — the identity.

The ordering is an artefact of the weakened typeclass, not of the mathematics: once the Hecke ring is known to be commutative the factors commute and the product is n.factorization.prod (heckeTGeneratorRecGamma0 N) by TauCeti.Nat.primePowerProd_eq_factorization_prod.

Equations
Instances For
    source
    theorem HeckeRing.GL2.heckeTCompositeGamma0_def (N : ℕ) [NeZero N] (n : ℕ) :
    heckeTCompositeGamma0 N n = TauCeti.Nat.primePowerProd (heckeTGeneratorRecGamma0 N) n

    The defining equation of the composite: it is the ordered product of the recurrence family over the factorisation. The body is sealed, so without this the TauCeti.Nat.primePowerProd API — in particular the multiplicativity that arrives with commutativity — is unreachable for it.

    source
    @[simp]
    theorem HeckeRing.GL2.heckeTCompositeGamma0_zero (N : ℕ) [NeZero N] :
    heckeTCompositeGamma0 N 0 = 1

    The junk input: 0 has no factorisation, and the empty product is the identity.

    source
    @[simp]
    theorem HeckeRing.GL2.heckeTCompositeGamma0_one (N : ℕ) [NeZero N] :
    heckeTCompositeGamma0 N 1 = 1

    T₁ = 1: the empty product over the empty factorisation.

    source
    theorem HeckeRing.GL2.heckeTCompositeGamma0_of_one_lt (N : ℕ) [NeZero N] {n : ℕ} (hn : 1 < n) :
    heckeTCompositeGamma0 N n = heckeTGeneratorRecGamma0 N n.minFac (n.factorization n.minFac) * heckeTCompositeGamma0 N (n / n.minFac ^ n.factorization n.minFac)

    The peeling step: for 1 < n the composite splits off the block at the least prime factor of n, carrying its whole multiplicity.

    source
    @[simp]
    theorem HeckeRing.GL2.heckeTCompositeGamma0_prime_pow (N : ℕ) [NeZero N] {p : ℕ} (hp : Nat.Prime p) (v : ℕ) :
    heckeTCompositeGamma0 N (p ^ v) = heckeTGeneratorRecGamma0 N p v

    On a prime power the composite is the recurrence family: T_{p^v} assembled is T_{p^v} generated.

    No positivity is asked of v, unlike the general TauCeti.Nat.primePowerProd_prime_pow: at v = 0 both sides are the identity, the left by heckeTCompositeGamma0_one and the right by heckeTGeneratorRecGamma0_zero. That the two junk conventions agree is what lets every consumer below drop the hypothesis.

    source
    @[simp]
    theorem HeckeRing.GL2.heckeTCompositeGamma0_prime (N : ℕ) [NeZero N] {p : ℕ} (hp : Nat.Prime p) :
    heckeTCompositeGamma0 N p = heckeTGeneratorGamma0 N p

    At a prime the composite is the generator: T_p assembled is T_p. This is TauCeti.Nat.primePowerProd_prime read through the definition. Marked @[simp] alongside heckeTCompositeGamma0_prime_pow, which cannot fire here: a bare prime is not syntactically a power, so without this lemma a prime input does not reduce to the generator.

    source
    theorem HeckeRing.GL2.heckeTCompositeGamma0_prime_pow_of_not_coprime (N : ℕ) [NeZero N] {p : ℕ} (hp : Nat.Prime p) (hpN : ¬p.Coprime N) (v : ℕ) :
    heckeTCompositeGamma0 N (p ^ v) = heckeTGeneratorGamma0 N p ^ v

    When p shares a factor with the level the scalar term of the recurrence vanishes and the composite degenerates to a power of the generator: T_{p^v} = T_p^v. This is the bad-prime half of the classical statement, and it is unconditional in v.

    source
    theorem HeckeRing.GL2.heckeTCompositeGamma0_mul_of_coprime (N : ℕ) [NeZero N] {m n : ℕ} (hmn : m.Coprime n) :
    heckeTCompositeGamma0 N (m * n) = heckeTCompositeGamma0 N m * heckeTCompositeGamma0 N n

    Coprime multiplicativity: T_{mn} = T_m · T_n when m and n share no prime factor.

    The classical multiplicative relation among the Γ₀(N) Hecke operators, at the level of the Hecke ring. Together with heckeTCompositeGamma0_prime_pow, which identifies the composite on a prime power with the Diamond–Shurman recurrence family, it determines T_n for every positive n from the prime-power data: split n into its prime powers here, then evaluate each factor there. The junk input 0 has no factorisation to split and is fixed separately by heckeTCompositeGamma0_zero. No hypothesis relates m or n to the level — the bad primes are already absorbed into the blocks.

    The composite scalar, and the global multiplication table #

    source
    theorem HeckeRing.GL2.heckeTCompositeGamma0_mul_eq_sum_divisors_gcd (N : ℕ) [NeZero N] {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
    heckeTCompositeGamma0 N m * heckeTCompositeGamma0 N n = ∑ d ∈ (m.gcd n).divisors, ↑d • (heckeTScalarGamma0 N d * heckeTCompositeGamma0 N (m * n / d ^ 2))

    Shimura, Theorem 3.24(3) at level Γ₀(N), in full — the global multiplication table:

    T_m · T_n = ∑_{d ∣ gcd m n} d • (S_d · T_{mn/d²}).

    This is the composite counterpart of heckeTGeneratorRecGamma0_mul, which is the same identity one prime at a time. At coprime m and n it specialises to heckeTCompositeGamma0_mul_of_coprime: the gcd is 1, the sum collapses to its d = 1 term, and S₁ = 1 leaves T_m · T_n.

    Both arguments must be nonzero. heckeTCompositeGamma0 sends 0 to the empty product 1 and gcd 0 0 = 0 has no divisors, so at m = n = 0 the left side is 1 and the right an empty sum.

    Together with heckeTCompositeGamma0_prime_pow this determines every product of two composite elements from the prime-power data. Divisors sharing a factor with the level contribute nothing, by heckeTScalarGamma0_of_not_coprime, so the sum over all divisors of gcd m n is the right index even though only the good ones carry weight.

    Subrings containing the prime generators #

    source
    theorem HeckeRing.GL2.heckeTCompositeGamma0_mem_of_forall_prime_dvd (N : ℕ) [NeZero N] {S : Subring (HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ℤ)} {n : ℕ} (hT : ∀ (p : ℕ), Nat.Prime p → p ∣ n → heckeTGeneratorGamma0 N p ∈ S) (hs : ∀ (p : ℕ), Nat.Prime p → p ∣ n → heckeTScalarGamma0 N p ∈ S) :
    heckeTCompositeGamma0 N n ∈ S

    A subring containing the prime data of n contains T_n. If a subring S of the Γ₀(N) Hecke ring contains the generator T_p and the scalar coset T(p, p) at every prime p ∣ n, it contains heckeTCompositeGamma0 N n: each prime-power block is a polynomial in the two by the Diamond–Shurman recurrence, and T_n is the product of its blocks.

    The elements away from m lie in the subring generated by the cosets of determinant #

    prime to m

    source
    theorem HeckeRing.GL2.heckeTCompositeGamma0_mem_closure_coprimeDetCoset (N : ℕ) [NeZero N] {m n : ℕ} (hn : n.Coprime m) :
    heckeTCompositeGamma0 N n ∈ Subring.closure {x : HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ℤ | ∃ (D : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))), CoprimeDetCoset N m D ∧ x = HeckeCosetModule.single ℤ D 1}

    The Hecke elements away from m lie in the subring generated by the double cosets of determinant prime to m. For n coprime to m, T_n is a polynomial with integer coefficients in the classes of double cosets Γ₀(N) α Γ₀(N) with det α prime to m.

    An operator commuting with the action of every such class therefore commutes with every T_n with n prime to m; at m = N this is how the Fricke operator is shown to commute with the good Hecke operators, and at m = Q for an exact divisor Q of N how the Atkin–Lehner operator W_Q is shown to commute with the T_n for n prime to Q.

    source
    theorem HeckeRing.GL2.commute_map_heckeTCompositeGamma0_of_forall_coprimeDetCoset (N : ℕ) [NeZero N] {A : Type u_1} [Ring A] (φ : HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ℤ →+* A) {a : A} {m n : ℕ} (hn : n.Coprime m) (ha : ∀ (D : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))), CoprimeDetCoset N m D → Commute a (φ (HeckeCosetModule.single ℤ D 1))) :
    Commute a (φ (heckeTCompositeGamma0 N n))

    Commuting with the cosets of determinant prime to m is commuting with the T_n away from m. Under a ring homomorphism φ out of the Γ₀(N) Hecke ring, an element commuting with the image of every double coset of determinant prime to m commutes with the image of T_n for every n prime to m. This is how the Fricke operator (m = N) and the Atkin–Lehner operators (m = Q) are shown to commute with the Hecke operators away from m.