The T_p coset representatives at n = 2

GLn/CosetDecomposition.lean indexes the upper-triangular coset representatives by the bounded entry assignments UpperTriEntries n a, a dependent function on the ordered index pairs {ij : Fin n × Fin n // ij.1 < ij.2}. At n = 2 there is exactly one such pair, (0, 1), so an assignment carries a single coordinate and UpperTriEntries 2 a is just Fin (a 1 / a 0).

This file records that identification, and its specialisation to a = ![1, p], where the coordinate is an offset b ∈ Fin p and upperTriGL runs over the classical !![1, b; 0, p]. It is the adapter between the general-n decomposition and the classical T_p bookkeeping, which sums over b directly: a sum over UpperTriEntries 2 ![1, p] transfers along this equivalence rather than being restated.

Alongside the upper-triangular family this file records the remaining representative, scaleRep p = !![p, 0; 0, 1], so that both families and the two facts every slash argument needs of them — upper-triangularity and positive determinant — sit together.

Nothing here involves a level or a congruence subgroup; the level-N membership statements for these representatives are in GL2/UpperTriangularDelta0.lean.

Main definitions

• HeckeRing.GL2.uniqueIndexPair: (0, 1) is the only ordered index pair at n = 2.
• HeckeRing.GL2.upperTriEntriesEquiv: UpperTriEntries 2 a ≃ Fin (a 1 / a 0), for an arbitrary tuple a.
• HeckeRing.GL2.upperTriEntriesEquivFin: its specialisation UpperTriEntries 2 ![1, p] ≃ Fin p.
• HeckeRing.GL2.scaleRep: the scaling representative !![p, 0; 0, 1], as natDiagGL 2 ![p, 1] — named for TauCeti.scaleGL, its image over ℝ. "Diagonal" alone would not pin it down: upperTriRep p 0 is !![1, 0; 0, p], diagonal with the entries the other way round.

Main results

• HeckeRing.GL2.upperTriEntriesEquiv_apply, upperTriEntriesEquiv_symm_apply_default: the equivalence reads off, and installs, the coordinate at the unique index pair.

• HeckeRing.GL2.upperTriEntriesEquivFin_apply_val and upperTriEntriesEquivFin_symm_apply_default_val: the same for a = ![1, p], as an identity of natural numbers — the two fibres Fin (![1, p] 1 / ![1, p] 0) is Fin (p / 1), which finCongr carries to Fin p along p / 1 = p.

• HeckeRing.GL2.coe_upperTriRep: the entrywise description of the representative: !![1, b; 0, p].

• HeckeRing.GL2.upperTriRep_apply_one_zero: the representatives are upper triangular — the hypothesis mathlib's IsBoundedAtImInfty.slash asks for.

• HeckeRing.GL2.upperTriRep_mul_upperTriRep: the families at indices n and m multiply into the family at index n · m, along finProdFinEquiv.

• HeckeRing.GL2.det_upperTriRep_pos: they have determinant p > 0, which is what lets scalars pass through a slash by them without the σ twist.

• HeckeRing.GL2.scaleRep_def and HeckeRing.GL2.scaleRep_zero: the defining equation and the junk branch, the route into the natDiagGL API.

• HeckeRing.GL2.coe_scaleRep: its entrywise description, for 0 < p.

• HeckeRing.GL2.scaleRep_apply_one_zero and det_scaleRep_pos: it too is upper triangular and has positive determinant — both unconditionally in p, since natDiagGL's junk value is the identity.

Provenance

No code is ported: the equivalence is a fact about this repository's own UpperTriEntries. The "classical T_p bookkeeping" it adapts to is that of the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0), LeanModularForms/HeckeRIngs/GL2/HeckeT_p.lean at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, whose heckeT_p_ut sums over b ∈ Finset.range p and whose T_p_upper p _ b = !![1, b; 0, p] is upperTriGL at n = 2, a = ![1, p]. This file exists so that such a sum transfers onto the existing general-n decomposition instead of restating the index. scaleRep is the same file's T_p_lower (line 52), the diagonal representative [[p, 0], [0, 1]], restated here as natDiagGL 2 ![p, 1] rather than as a fresh matrix literal.

References

• [DS] Diamond–Shurman, A first course in modular forms, Proposition 5.2.1 — the p + 1 left cosets of the double coset of diag(1, p) over Γ₀(N), the decomposition scaleRep completes.

@[instance_reducible]

instance HeckeRing.GL2.uniqueIndexPair : Unique { ij : Fin 2 × Fin 2 // ij.1 < ij.2 }

At n = 2 there is exactly one ordered index pair, (0, 1), so UpperTriEntries is a function on a one-element type.

Equations

• HeckeRing.GL2.uniqueIndexPair = { default := ⟨(0, 1), HeckeRing.GL2.uniqueIndexPair._proof_1⟩, uniq := HeckeRing.GL2.uniqueIndexPair._proof_2 }

@[simp]

theorem HeckeRing.GL2.default_indexPair_val : ↑default = (0, 1)

def HeckeRing.GL2.upperTriEntriesEquiv (a : Fin 2 → ℕ) : GLn.UpperTriEntries 2 a ≃ Fin (a 1 / a 0)

An entry assignment at n = 2 is a single coordinate. UpperTriEntries 2 a is a dependent function on the ordered index pairs, and by uniqueIndexPair there is only the pair (0, 1); the fibre over it is Fin (a 1 / a 0).

The fibre over default reduces to the fibre over (0, 1), namely Fin (a 1 / a 0), because default is the field of uniqueIndexPair. The specialisation to a = ![1, p] is a separate matter: it leaves the bound p / 1, and finCongr (by simp) transports along the propositional equality p / 1 = p.

Equations

• HeckeRing.GL2.upperTriEntriesEquiv a = Equiv.piUnique fun (p : { ij : Fin 2 × Fin 2 // ij.1 < ij.2 }) => Fin (a (↑p).2 / a (↑p).1)

@[simp]

theorem HeckeRing.GL2.upperTriEntriesEquiv_apply {a : Fin 2 → ℕ} (B : GLn.UpperTriEntries 2 a) : (upperTriEntriesEquiv a) B = B default

The equivalence reads off the coordinate at the unique index pair.

@[simp]

theorem HeckeRing.GL2.upperTriEntriesEquiv_symm_apply_default {a : Fin 2 → ℕ} (b : Fin (a 1 / a 0)) : (upperTriEntriesEquiv a).symm b default = b

Its inverse installs a given coordinate at the unique index pair.

def HeckeRing.GL2.upperTriEntriesEquivFin (p : ℕ) : GLn.UpperTriEntries 2 ![1, p] ≃ Fin p

The classical index of the upper-triangular representatives. For a = ![1, p] the entry assignments are just the offsets b ∈ Fin p, so upperTriGL at these entries runs over the familiar !![1, b; 0, p].

Equations

• HeckeRing.GL2.upperTriEntriesEquivFin p = (HeckeRing.GL2.upperTriEntriesEquiv ![1, p]).trans (finCongr ⋯)

@[simp]

theorem HeckeRing.GL2.upperTriEntriesEquivFin_apply_val {p : ℕ} (B : GLn.UpperTriEntries 2 ![1, p]) : ↑((upperTriEntriesEquivFin p) B) = ↑(B default)

At a = ![1, p] the offset read off is the coordinate, as natural numbers: the fibres Fin (![1, p] 1 / ![1, p] 0) is Fin (p / 1), carried to Fin p by finCongr.

@[simp]

theorem HeckeRing.GL2.upperTriEntriesEquivFin_symm_apply_default_val {p : ℕ} (b : Fin p) : ↑((upperTriEntriesEquivFin p).symm b default) = ↑b

At a = ![1, p] the coordinate installed is the offset, as natural numbers.

noncomputable def HeckeRing.GL2.upperTriRep (p : ℕ) (b : Fin p) : GL (Fin 2) ℚ

The b-th upper-triangular representative !![1, b; 0, p], as an element of this repository's general-n family at a = ![1, p].

Equations

• HeckeRing.GL2.upperTriRep p b = HeckeRing.GLn.upperTriGL ((HeckeRing.GL2.upperTriEntriesEquivFin p).symm b)

@[simp]

theorem HeckeRing.GL2.coe_upperTriRep (p : ℕ) (b : Fin p) : ↑(upperTriRep p b) = !![1, ↑↑b; 0, ↑p]

The matrix of upperTriRep p b is !![1, b; 0, p].

@[simp]

theorem HeckeRing.GL2.upperTriRep_one (b : Fin 1) : upperTriRep 1 b = 1

The unique upper-triangular representative at index one is the identity matrix.

@[simp]

theorem HeckeRing.GL2.upperTriRep_apply_one_zero (p : ℕ) (b : Fin p) : ↑(upperTriRep p b) 1 0 = 0

The representatives are upper triangular — the hypothesis mathlib's IsBoundedAtImInfty.slash asks for. At n = 2 this is the (1, 0) entry of upperTriGL_apply_eq_zero_of_lt.

theorem HeckeRing.GL2.upperTriRep_mul_upperTriRep {n m : ℕ} (b' : Fin n) (b : Fin m) : upperTriRep n b' * upperTriRep m b = upperTriRep (n * m) (finProdFinEquiv (b', b))

The upper-triangular representatives compose. The product of the representative at offset b' of index n with the one at offset b of index m is again a representative,

!![1, b'; 0, n] * !![1, b; 0, m] = !![1, b + m·b'; 0, n·m],

at index n · m and at the offset finProdFinEquiv (b', b), which is exactly b + m · b'.

Since finProdFinEquiv is a bijection, the n · m representatives are enumerated once each by the pairs, which is what makes the slash sums over these families multiply.

theorem HeckeRing.GL2.det_upperTriRep_pos (p : ℕ) (b : Fin p) : 0 < (↑(upperTriRep p b)).det

The representatives have positive determinant: det !![1, b; 0, p] = p > 0.

noncomputable def HeckeRing.GL2.scaleRep (p : ℕ) : GL (Fin 2) ℚ

The scaling representative !![p, 0; 0, 1], as natDiagGL 2 ![p, 1]. That entrywise description needs 0 < p, which is why coe_scaleRep carries the hypothesis: at p = 0 the positivity condition fails and natDiagGL returns its junk value 1 (natDiagGL_of_not_pos).

For a prime p ∤ N, over Γ₀(N) and with trivial character, the double coset of diag(1, p) has p + 1 left cosets: the p upper-triangular ones upperTriRep p b and this one. Both qualifiers are load-bearing. With nebentypus χ the last term acquires a factor χ(p), and over Γ₁(N) the untwisted matrix is not a coset representative at all — it is one only up to a Γ₀(N) twist, which is exactly what supplies the χ(p) in the recurrence.

The p + 1 count is specific to prime p; this definition is well formed for every p and claims no coset decomposition in general.

Over ℝ the same matrix is TauCeti.scaleGL p (ModularForms/Degeneracy.lean), where slashing by it is, up to the scalar p ^ (k - 1), the level-raising operator V_p. No declaration yet connects the two, so denom_scaleGL and coe_scaleGL_smul are not reachable from this name; the bridge belongs with the first consumer that needs the analytic facts.

It is diagonal, hence upper triangular, so it satisfies the same (1, 0) = 0 hypothesis that mathlib's IsBoundedAtImInfty.slash asks for, for every p.

Equations

• HeckeRing.GL2.scaleRep p = HeckeRing.GLn.natDiagGL 2 ![p, 1]

theorem HeckeRing.GL2.scaleRep_def (p : ℕ) : scaleRep p = GLn.natDiagGL 2 ![p, 1]

The defining equation. The body is not exported, so this is what routes scaleRep into the natDiagGL API — natDiagGL_det, and the Δ₀(N) membership natDiagGL_mem_Delta0_of_coprime that the coprime branch needs.

@[simp]

theorem HeckeRing.GL2.scaleRep_zero : scaleRep 0 = 1

The junk branch: at p = 0 the positivity condition fails and natDiagGL returns 1.

@[simp]

theorem HeckeRing.GL2.coe_scaleRep (p : ℕ) (hp : 0 < p) : ↑(scaleRep p) = !![↑p, 0; 0, 1]

The matrix of scaleRep p is !![p, 0; 0, 1], for 0 < p.

@[simp]

theorem HeckeRing.GL2.scaleRep_apply_one_zero (p : ℕ) : ↑(scaleRep p) 1 0 = 0

The remaining representative is upper triangular too: its (1, 0) entry vanishes, which is the hypothesis IsBoundedAtImInfty.slash asks for. For every p, p = 0 included.

theorem HeckeRing.GL2.det_scaleRep_pos (p : ℕ) : 0 < (↑(scaleRep p)).det

det (scaleRep p) > 0, for every p — including p = 0, where scaleRep 0 = 1.