The double coset Γ₀(N) · diag(1, p) · Γ₀(N) at a prime

The right-coset decomposition of the Γ₀(N) double coset of diag(1, p), the Γ₀(N) counterpart of Gamma1/CoprimeCosets.lean and Gamma1/UpperTriCosets.lean. At p ∤ N the representatives are the same p + 1 matrices as over Γ₁(N) — !![1, j; 0, p] for j < p and the twisted diagonal σ · diag(p, 1), primeRep σ p — and at p ∣ N the p upper-triangular ones. Injectivity of the representatives and the membership of the twisted one come from the Γ₁(N) files, since Γ₁(N) ≤ Γ₀(N); what is new is the covering step over Γ₀(N), whose elements need not have a ≡ 1 (mod N).

The covering step

For γ = [a, b; c, d] ∈ Γ₀(N): if p ∤ a, the upper-triangular factorisation exists_mem_Gamma0_upperTriRep_mul_of_isUnit at offset 0 writes diag(1, p) · γ as an element of Γ₀(N) times !![1, j; 0, p]; if p ∣ a, then diag(1, p) · γ = [a / p, b; c, p d] · diag(p, 1) with the first factor in Γ₀(N), which is the coset of σ · diag(p, 1) because σ ∈ Γ₀(N).

Main results

• HeckeRing.GL2.doubleCoset_natDiagGL_Gamma0_eq_iUnion_rightCosets_of_prime: at a prime p ∤ N, the union of the p + 1 right cosets named by primeRep σ p.
• HeckeRing.GL2.doubleCoset_natDiagGL_Gamma0_eq_iUnion_rightCosets_of_dvd: at a prime p ∣ N, the union of the p upper-triangular right cosets. Read at the chosen representative of diagCosetGamma0 N ![1, p] through HeckeCoset.toSet_eq_doubleCoset_rep and diagCosetGamma0_toSet, these are the shapes the twisted slash-sum machinery of HeckeSlash/Nebentypus/Independence.lean consumes.
• HeckeRing.GL2.Delta0UpperUnit_upperTriRep, HeckeRing.GL2.Delta0UpperUnit_mapGL_mul_scaleRep: the upper-left unit of either kind of representative is 1, so the twisting character of HeckeSlash/Nebentypus/* is trivial on both.

Provenance

The coset bookkeeping behind heckeRingHomCharSpace_D_p_eq_scalar_charRestrict of the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Unified/NebentypusHeckeRingHom.lean, Chris Birkbeck, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), reorganised around this repository's primeRep and doubleCoset_eq_iUnion_rightCosets_of_forall_exists.

theorem HeckeRing.GL2.exists_mem_Gamma0_natDiagGL_mul_eq_mul_scaleRep_of_dvd {N p : ℕ} (hp : 0 < p) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 N) (hpa : ↑p ∣ ↑γ 0 0) : ∃ δ ∈ CongruenceSubgroup.Gamma0 N, GLn.natDiagGL 2 ![1, p] * (Matrix.SpecialLinearGroup.mapGL ℚ) γ = (Matrix.SpecialLinearGroup.mapGL ℚ) δ * scaleRep p

When p divides the upper-left entry of γ ∈ Γ₀(N), diag(1, p) · γ factors through the scaling representative: diag(1, p) · !![a, b; c, d] = !![a / p, b; c, p d] · diag(p, 1), and the first factor lies in Γ₀(N).

theorem HeckeRing.GL2.exists_mem_Gamma0_natDiagGL_mul_primeRep {N p : ℕ} {σ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hp : Nat.Prime p) (hσ10 : ↑σ 1 0 = ↑N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 N) : ∃ (i : Option (Fin p)), ∃ δ ∈ CongruenceSubgroup.Gamma0 N, GLn.natDiagGL 2 ![1, p] * (Matrix.SpecialLinearGroup.mapGL ℚ) γ = (Matrix.SpecialLinearGroup.mapGL ℚ) δ * primeRep σ p i

Every diag(1, p) · γ with γ ∈ Γ₀(N) lies in a right coset named by primeRep σ p: at p ∤ a the upper-triangular factorisation exists_mem_Gamma0_upperTriRep_mul_of_isUnit at offset 0 lands on !![1, j; 0, p]; at p ∣ a the scaling factorisation lands on σ · diag(p, 1) after absorbing σ⁻¹ ∈ Γ₀(N).

theorem HeckeRing.GL2.doubleCoset_natDiagGL_Gamma0_eq_iUnion_rightCosets_of_prime {N p : ℕ} {σ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hp : Nat.Prime p) (hσ10 : ↑σ 1 0 = ↑N) (hσ11 : ↑σ 1 1 = ↑p) : DoubleCoset.doubleCoset (GLn.natDiagGL 2 ![1, p]) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) = ⋃ (i : Option (Fin p)), MulOpposite.op (primeRep σ p i) • ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The Γ₀(N) double coset of diag(1, p) at a prime p ∤ N is the union of p + 1 right cosets, named by the same representatives primeRep σ p as over Γ₁(N): p ∤ N is carried by the twist σ with bottom row (N, p).

theorem HeckeRing.GL2.doubleCoset_natDiagGL_Gamma0_eq_iUnion_rightCosets_of_dvd {N p : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) : DoubleCoset.doubleCoset (GLn.natDiagGL 2 ![1, p]) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) = ⋃ (j : Fin p), MulOpposite.op (upperTriRep p j) • ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

At a prime dividing the level, the Γ₀(N) double coset of diag(1, p) is the union of the p upper-triangular right cosets: the factorisation exists_mem_Gamma0_upperTriRep_mul_of_mem_Gamma0 never leaves the family.

The upper-left units of the representatives

@[simp]

theorem HeckeRing.GL2.Delta0UpperUnit_upperTriRep {N p : ℕ} (j : Fin p) (hmem : upperTriRep p j ∈ Delta0 N) : (Delta0UpperUnit N) ⟨upperTriRep p j, hmem⟩ = 1

The upper-left unit of an upper-triangular representative is 1.

@[simp]

theorem HeckeRing.GL2.Delta0UpperUnit_mapGL_mul_scaleRep {N p : ℕ} {σ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hp : 0 < p) (hσ10 : ↑σ 1 0 = ↑N) (hσ11 : ↑σ 1 1 = ↑p) (hmem : (Matrix.SpecialLinearGroup.mapGL ℚ) σ * scaleRep p ∈ Delta0 N) : (Delta0UpperUnit N) ⟨(Matrix.SpecialLinearGroup.mapGL ℚ) σ * scaleRep p, hmem⟩ = 1

The upper-left unit of the twisted representative σ · diag(p, 1) is 1: its upper-left entry is σ₀₀ p ≡ 1 (mod N), by the determinant of σ.