The Γ₀(N)-double coset of a diagonal matrix

diag(a₁, a₂) lies in Δ₀(N) as soon as a₁ is coprime to the level — the lower-left entry vanishes, so the only condition beyond integrality and positive determinant is that the upper-left entry be a unit modulo N. That gives the Γ₀(N)-level analogue diagCosetGamma0 of diagCoset, and it sits over the level-one one:

toLevelOneCoset N (diagCosetGamma0 N a hgcd) = diagCoset a

These are the double cosets the level-N Hecke operators are built from — T(a₁, a₂) at level N. The bridge identifies the image of the level-N coset under toLevelOneCoset with diagCoset a; it says nothing about the Hecke-ring operations, and it does not by itself supply the coprime-determinant hypothesis that toLevelOneCoset_injOn needs.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/Props.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), the diagMat_mem_Delta0_of_gcd and T_diag_Gamma0 declarations.

Main definitions

• HeckeRing.GL2.diagCosetGamma0: the Γ₀(N)-double coset of diag(a).

Main results

• HeckeRing.GL2.natDiagGL_mem_Delta0_of_coprime: diag(a) ∈ Δ₀(N) when a₁ is coprime to N.
• HeckeRing.GL2.diagCosetGamma0_toSet: its underlying set.
• HeckeRing.GL2.toLevelOneCoset_diagCosetGamma0: the Γ₀(N)-coset of diag(a) lies over the level-one coset T(a).
• HeckeRing.GL2.diagCosetGamma0_one: the all-ones tuple gives the identity coset.
• HeckeRing.GL2.diagCosetGamma0_of_not_pos: so does any tuple that is not everywhere positive.
• HeckeRing.GL2.doubleCoset_out_diagCosetGamma0_const_eq_iUnion_rightCosets: a scalar double coset is a single right coset.
• HeckeRing.GL2.coprimeDetCoset_diagCosetGamma0_of_coprime: the coset of diag(a) has determinant prime to m when a₀ a₁ is.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.3.

theorem HeckeRing.GL2.natDiagGL_mem_Delta0_of_coprime (N : ℕ) (a : Fin 2 → ℕ) (hgcd : (∀ (i : Fin 2), 0 < a i) → (a 0).Coprime N) : GLn.natDiagGL 2 a ∈ Delta0 N

A diagonal whose upper-left entry is coprime to N lies in Δ₀(N): the lower-left entry is zero, so only the unit condition has content — and when positivity fails natDiagGL is the identity, which is in Δ₀(N) anyway. Coprimality is therefore only needed in the positive branch, and the hypothesis asks for it only there.

noncomputable def HeckeRing.GL2.diagCosetGamma0 (N : ℕ) (a : Fin 2 → ℕ) (hgcd : (∀ (i : Fin 2), 0 < a i) → (a 0).Coprime N) : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The Γ₀(N)-double coset of diag(a) when the upper-left entry is coprime to the level: the level-N analogue of diagCoset.

Coprimality stays in the signature because it is what puts the matrix in Δ₀(N), but only under positivity: without it natDiagGL falls back to the identity, which lies in Δ₀(N) regardless of the level.

Equations

• One or more equations did not get rendered due to their size.

theorem HeckeRing.GL2.diagCosetGamma0_def (N : ℕ) (a : Fin 2 → ℕ) (hgcd : (∀ (i : Fin 2), 0 < a i) → (a 0).Coprime N) : diagCosetGamma0 N a hgcd = HeckeCoset.mk (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ⟨GLn.natDiagGL 2 a, ⋯⟩

Defining equation for the sealed definition diagCosetGamma0.

@[simp]

theorem HeckeRing.GL2.diagCosetGamma0_toSet (N : ℕ) (a : Fin 2 → ℕ) (hgcd : (∀ (i : Fin 2), 0 < a i) → (a 0).Coprime N) : (diagCosetGamma0 N a hgcd).toSet = DoubleCoset.doubleCoset (GLn.natDiagGL 2 a) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The underlying set of diagCosetGamma0 a is the Γ₀(N)-double coset of diag(a).

@[simp]

theorem HeckeRing.GL2.toLevelOneCoset_diagCosetGamma0 (N : ℕ) (a : Fin 2 → ℕ) (hgcd : (∀ (i : Fin 2), 0 < a i) → (a 0).Coprime N) : toLevelOneCoset N (diagCosetGamma0 N a hgcd) = GLn.diagCoset a

The Γ₀(N)-coset of diag(a) lies over the level-one coset T(a): widening both coefficient subgroups from Γ₀(N) to SL₂(ℤ) along toLevelOneCoset gives the double coset of the same representative, hence exactly diagCoset a. (The Γ₀(N)-coset itself is in general strictly smaller than the level-one one.)

@[simp]

theorem HeckeRing.GL2.diagCosetGamma0_one (N : ℕ) (h : (∀ (x : Fin 2), 0 < 1) → Nat.Coprime 1 N) : diagCosetGamma0 N (fun (x : Fin 2) => 1) h = 1

The identity normal form, mirroring diagCoset_one: the all-ones tuple gives the identity double coset, whatever proof of the coprimality condition is supplied.

@[simp]

theorem HeckeRing.GL2.diagCosetGamma0_of_not_pos (N : ℕ) {a : Fin 2 → ℕ} (hgcd : (∀ (i : Fin 2), 0 < a i) → (a 0).Coprime N) (ha : ¬∀ (i : Fin 2), 0 < a i) : diagCosetGamma0 N a hgcd = 1

The junk normal form, mirroring diagCoset_of_not_pos: a tuple that is not everywhere positive gives the identity coset, matching the junk value of natDiagGL. The coprimality condition is vacuous in this branch, so it is irrelevant which proof is supplied.

theorem HeckeRing.GL2.exists_rep_diagCosetGamma0_eq_mul_natDiagGL_mul (N : ℕ) (a : Fin 2 → ℕ) (hgcd : (∀ (i : Fin 2), 0 < a i) → (a 0).Coprime N) : ∃ h₁ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N), ∃ h₂ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N), ↑(diagCosetGamma0 N a hgcd).rep = h₁ * GLn.natDiagGL 2 a * h₂

The representative of the Γ₀(N)-coset of diag(a) differs from diag(a) by a left and a right factor in Γ₀(N).

theorem HeckeRing.GL2.doubleCoset_out_diagCosetGamma0_const_eq_iUnion_rightCosets (N c : ℕ) (hcN : 0 < c → c.Coprime N) : DoubleCoset.doubleCoset ↑(Quotient.out (diagCosetGamma0 N ![c, c] ⋯)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) = ⋃ (x : Unit), MulOpposite.op (GLn.natDiagGL 2 ![c, c]) • ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The scalar Γ₀(N) double coset is the single right coset represented by its natural diagonal matrix. The coprimality hypothesis is only needed on the positive branch, matching the junk-branch convention of diagCosetGamma0: at c = 0 the representative is the identity and the statement is the trivial decomposition of Γ₀(N) itself.

@[simp]

theorem HeckeRing.GL2.degree_diagCosetGamma0_const (N c : ℕ) (hgcd : (∀ (x : Fin 2), 0 < c) → c.Coprime N) : (diagCosetGamma0 N (fun (x : Fin 2) => c) hgcd).degree = 1

The scalar double coset has degree one: diag(c, c) is central, so its Γ₀(N)-double coset is a single right coset. The level-N companion of degree_diagCoset_const; it is what bounds the multiplicity of a product one of whose factors is scalar.

theorem HeckeRing.GL2.coprimeDetCoset_diagCosetGamma0_of_coprime (N : ℕ) {m : ℕ} {a : Fin 2 → ℕ} (ha : ∀ (i : Fin 2), 0 < a i) (hgcd : (∀ (i : Fin 2), 0 < a i) → (a 0).Coprime N) (h : (a 0 * a 1).Coprime m) : CoprimeDetCoset N m (diagCosetGamma0 N a hgcd)

A diagonal double coset has determinant prime to m as soon as a₀ a₁ is: the determinant of diag(a₀, a₁) is a₀ a₁. At m = Q for an exact divisor Q of the level this is the hypothesis CoprimeDetCoset N Q under which the Hecke operator T(a₀, a₁) commutes with the Atkin–Lehner operator W_Q; at m = N it is the one for the Fricke operator.