The diagonal elements of the Γ₀(N) Hecke ring

Gamma0/Diagonal/Coset.lean builds the double coset Γ₀(N)·diag(a)·Γ₀(N) as a HeckeCoset. This file turns it into an element of the Hecke ring 𝕋 (Δ₀(N)) (Γ₀(N)) — the level-N analogue of diagElem — with the coprimality guard applied once so that the vanishing case is stated in a single place rather than at each generator.

Coset.lean holds the coset layer and this file the ring-element layer, so the two of Coset.lean's three consumers that want only cosets (Gamma1/UpperTriCosets.lean and UpperTriangularDelta0.lean) stop there. Keeping the element here rather than in PrimePower.lean means a consumer wanting only the general diagonal element does not import the prime-power recurrence.

Main definitions

• HeckeRing.GL2.diagElemGamma0: the class of Γ₀(N)·diag(a)·Γ₀(N) in the Hecke ring, or 0 when the head entry shares a factor with the level or some entry is not positive.

Main results

• HeckeRing.GL2.diagElemGamma0_of_pos_of_coprime, _of_not_coprime, _of_not_pos: the three branches of the definition.
• HeckeRing.GL2.diagElemGamma0_one, _one_one: the identity normal forms, at the constant tuple and at the vector literal ![1, 1].

References

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

noncomputable def HeckeRing.GL2.diagElemGamma0 (N : ℕ) (a : Fin 2 → ℕ) : HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ℤ

The level-N diagonal element of the Hecke ring, 0 unless the head entry a 0 is coprime to the level.

Inside the coprime branch the value still depends on the tuple, and the three cases are worth keeping straight:

• ¬ Nat.Coprime (a 0) N — the element is 0 (diagElemGamma0_of_not_coprime);
• some entry not positive — the element is 0 (diagElemGamma0_of_not_pos);
• every entry positive and the head coprime to the level — the class of Γ₀(N)·diag(a)·Γ₀(N), the intended case.

The coprimality guard is what Δ₀(N)-membership needs, and putting it here rather than at each generator means the vanishing case is stated once. Positivity is guarded alongside it so that both degenerate branches take the single junk value 0, matching heckeTDiag at level one (GL2/Basic.lean), whose guard is likewise a positivity-and-condition conjunction. This is the level-N analogue of diagElem.

Equations

• HeckeRing.GL2.diagElemGamma0 N a = if h : (∀ (i : Fin 2), 0 < a i) ∧ (a 0).Coprime N then HeckeCosetModule.single ℤ (HeckeRing.GL2.diagCosetGamma0 N a ⋯) 1 else 0

theorem HeckeRing.GL2.diagElemGamma0_of_pos_of_coprime (N : ℕ) {a : Fin 2 → ℕ} (hpos : ∀ (i : Fin 2), 0 < a i) (h : (a 0).Coprime N) : diagElemGamma0 N a = HeckeCosetModule.single ℤ (diagCosetGamma0 N a ⋯) 1

Defining equation in the nondegenerate branch: the element is the class of the double coset. Both guards are needed — positivity as well as coprimality — since either failing sends the element to 0.

@[simp]

theorem HeckeRing.GL2.diagElemGamma0_of_not_coprime (N : ℕ) {a : Fin 2 → ℕ} (h : ¬(a 0).Coprime N) : diagElemGamma0 N a = 0

The diagonal element vanishes when the head entry shares a factor with the level.

@[simp]

theorem HeckeRing.GL2.diagElemGamma0_of_not_pos (N : ℕ) {a : Fin 2 → ℕ} (ha : ¬∀ (i : Fin 2), 0 < a i) : diagElemGamma0 N a = 0

The diagonal element vanishes when some entry fails to be positive. The underlying natDiagGL would degenerate to the identity matrix there, so the value is a junk convention rather than a membership fact; 0 is the same convention heckeTDiag uses at level one.

@[simp]

theorem HeckeRing.GL2.diagElemGamma0_one (N : ℕ) : (diagElemGamma0 N fun (x : Fin 2) => 1) = 1

The identity normal form at the all-ones tuple, mirroring diagCosetGamma0_one: diag(1, 1) is the identity matrix, so its class is the ring identity. This is the case both generators in Diagonal/PrimePower.lean reduce to at argument 1.

@[simp]

theorem HeckeRing.GL2.diagElemGamma0_one_one (N : ℕ) : diagElemGamma0 N ![1, 1] = 1

The identity at the vector literal ![1, 1]: the same fact as diagElemGamma0_one, at the tuple spelling rather than the constant function. The two are equal but not syntactically so, and ![1, 1] is the spelling the generators of Diagonal/PrimePower.lean reduce to.