The descent matrices at a prime

Miyake's level descent at a prime p runs over the p upper-triangular matrices [1, v; 0, p] together with, when p divides N but p² does not, one further matrix built from an element of Γ₀(N / p) reducing to S = [[0, -1], [1, 0]] modulo p and to the identity modulo N / p. This file supplies that extra matrix, assembles the family of p or p + 1 elements of GL₂(ℝ) the descent runs over, and computes their determinants.

The extra matrix comes from strong approximation at a coprime pair of levels, CongruenceSubgroup.exists_mem_Gamma_map_intCast_zmod_eq: for coprime d and d' the principal congruence subgroup Γ(d') still surjects onto SL₂(ℤ/dℤ). The descent is that statement at d = p and d' = N / p — a coprime pair exactly because p divides N while p² does not — with S as the prescribed reduction modulo p. Approximation returns membership in Γ(N / p), which is stronger than the Γ₀(N / p) the descent asks for, so the second reduction is the identity rather than merely lower-triangular.

Main definitions

• TauCeti.descendMatrixCount: the size of the family, p when p² ∣ N and p + 1 otherwise.
• TauCeti.descendExtraGamma: the extra matrix, with the junk value 1 outside the hypotheses that make the choice.
• TauCeti.descendMatrixRat: the family before the embedding into GL₂(ℝ), indexed by Fin (descendMatrixCount p N).
• TauCeti.descendMatrix: the family itself, the image of descendMatrixRat in GL₂(ℝ) (descendMatrix_eq_map); descendMatrixRat_of_lt/descendMatrixRat_of_le and descendMatrix_of_lt/descendMatrix_of_le describe the members, and descendMatrixRat_det/ descendMatrix_det their determinant.

Main results

• TauCeti.exists_mem_Gamma0_map_intCast_zmod_eq_S: for a prime p with p ∣ N and p² ∤ N, some γ ∈ Γ₀(N / p) reduces to S modulo p and to the identity modulo N / p.
• TauCeti.descendExtraGamma_mem_Gamma0, TauCeti.descendExtraGamma_map_intCast_zmod_eq_S and TauCeti.descendExtraGamma_map_intCast_zmod_div_eq_one: those three properties, read back off the chosen matrix.
• TauCeti.descendExtraGamma_eq_one_of_not: outside the hypotheses that make the choice, the extra matrix is the identity.
• TauCeti.descendMatrixCount_of_sq_dvd and TauCeti.descendMatrixCount_of_not_sq_dvd: the two values of the count.
• TauCeti.descendMatrix_of_lt and TauCeti.descendMatrix_of_le: the two branches of the family, as equations in GL₂(ℝ).
• TauCeti.descendMatrix_det: every member of the family has determinant p.
• TauCeti.descendMatrix_det_pos: that determinant is positive, which is what the slash action needs to pull a scalar through a member of the family.

Scope

The family is defined and its determinants computed. That its members are a set of coset representatives, and that the associated slash sum descends the level, are separate statements about the double coset Γ₀(N) diag(1, p) Γ₀(N); neither is proved here. Until they are, the family is the intended list of representatives rather than a formalized one.

Follows the AINTLIB LeanModularForms project, whose descendExtraGamma, descendCosetCount, descendCosetList and descendCosetList_det are the counterparts of the declarations here — the names differ because nothing here proves these matrices are coset representatives — and specializes its descendExtraGamma_exists (LeanModularForms/StrongMultiplicityOne/DescentCosets.lean, Chris Birkbeck, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), which proves the same existence directly; here it is read off the general coprime-level statement instead.

theorem TauCeti.exists_mem_Gamma0_map_intCast_zmod_eq_S {p N : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) (hpsq : ¬p ^ 2 ∣ N) : ∃ γ ∈ CongruenceSubgroup.Gamma0 (N / p), (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod p))) γ = (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod p))) ModularGroup.S ∧ (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod (N / p)))) γ = 1

A matrix with prescribed reductions at p and at N / p. For a prime p with p ∣ N but p² ∤ N, there is a γ ∈ Γ₀(N / p) reducing to S = [[0, -1], [1, 0]] modulo p and to the identity modulo N / p.

p² ∤ N is exactly what makes p coprime to N / p; the target modulo p is S, and membership in Γ₀(N / p) comes from the stronger Γ(N / p) that CongruenceSubgroup.exists_mem_Gamma_map_intCast_zmod_eq already delivers.

This is the matrix Miyake's Lemma 4.5.11 takes as its extra coset representative for the level descent when p exactly divides N. Only existence and the two reductions are proved here: the coset system is not formalized, so nothing is claimed about enumerating or completing it.

def TauCeti.descendMatrixCount (p N : ℕ) : ℕ

The size of the descent family at p. Miyake's count: p when p² divides N, and p + 1 when it does not, the extra member being the one descendExtraGamma supplies.

Equations

• TauCeti.descendMatrixCount p N = if p ^ 2 ∣ N then p else p + 1

@[simp]

theorem TauCeti.descendMatrixCount_of_sq_dvd {p N : ℕ} (h : p ^ 2 ∣ N) : descendMatrixCount p N = p

The descent family has p members when p² divides N.

@[simp]

theorem TauCeti.descendMatrixCount_of_not_sq_dvd {p N : ℕ} (h : ¬p ^ 2 ∣ N) : descendMatrixCount p N = p + 1

The descent family has p + 1 members when p² does not divide N.

noncomputable def TauCeti.descendExtraGamma (p N : ℕ) : Matrix.SpecialLinearGroup (Fin 2) ℤ

The extra descent matrix. For a prime p exactly dividing N, an element of Γ₀(N / p) reducing to S modulo p and to the identity modulo N / p; the junk value 1 when those hypotheses fail, so that the definition is total. Its three defining properties are descendExtraGamma_mem_Gamma0, descendExtraGamma_map_intCast_zmod_eq_S and descendExtraGamma_map_intCast_zmod_div_eq_one.

Equations

• TauCeti.descendExtraGamma p N = if h : Nat.Prime p ∧ p ∣ N ∧ ¬p ^ 2 ∣ N then ⋯.choose else 1

theorem TauCeti.descendExtraGamma_mem_Gamma0 {p N : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) (hpsq : ¬p ^ 2 ∣ N) : descendExtraGamma p N ∈ CongruenceSubgroup.Gamma0 (N / p)

The extra descent matrix lies in Γ₀(N / p).

@[simp]

theorem TauCeti.descendExtraGamma_map_intCast_zmod_eq_S {p N : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) (hpsq : ¬p ^ 2 ∣ N) : (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod p))) (descendExtraGamma p N) = (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod p))) ModularGroup.S

The extra descent matrix reduces to S modulo p.

@[simp]

theorem TauCeti.descendExtraGamma_map_intCast_zmod_div_eq_one {p N : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) (hpsq : ¬p ^ 2 ∣ N) : (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod (N / p)))) (descendExtraGamma p N) = 1

The extra descent matrix reduces to the identity modulo N / p.

@[simp]

theorem TauCeti.descendExtraGamma_eq_one_of_not {p N : ℕ} (h : ¬(Nat.Prime p ∧ p ∣ N ∧ ¬p ^ 2 ∣ N)) : descendExtraGamma p N = 1

Outside its guard the extra matrix is the identity. For p not prime, or not dividing N, or with p² dividing N, the choice is not available and descendExtraGamma takes its junk value.

noncomputable def TauCeti.descendMatrixRat (p N : ℕ) [NeZero p] : Fin (descendMatrixCount p N) → GL (Fin 2) ℚ

The descent family at p, over ℚ (Miyake, Lemma 4.5.11): a family in GL₂(ℚ) made of the p upper-triangular matrices upperTriRep p v = [1, v; 0, p] for v < p — this repository's T_p representative family — together with, when p² does not divide N, so that descendMatrixCount is p + 1, the further matrix [1, 0; 0, p] * mapGL ℚ γ_p, where γ_p = descendExtraGamma p N is embedded into GL₂(ℚ) by mapGL ℚ.

Neither p ∣ N nor primality of p is required: the construction uses only p ≠ 0, to name the zero index of Fin p. Those two hypotheses are what make the family the descent family at a prime — without p ∣ N the matrix descendExtraGamma p N is 1 and the extra member degenerates to [1, 0; 0, p], which the first branch already lists at v = 0 — so they belong on the later results that establish descent, not on the family itself.

Equations

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

noncomputable def TauCeti.descendMatrix (p N : ℕ) [NeZero p] : Fin (descendMatrixCount p N) → GL (Fin 2) ℝ

The descent family, the image of descendMatrixRat p N in GL₂(ℝ), where the slash action of a modular form lives.

Equations

• TauCeti.descendMatrix p N v = (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (TauCeti.descendMatrixRat p N v)

theorem TauCeti.descendMatrix_eq_map (p N : ℕ) [NeZero p] (v : Fin (descendMatrixCount p N)) : descendMatrix p N v = (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (descendMatrixRat p N v)

The descent family is the image of the rational descent family.

@[simp]

theorem TauCeti.descendMatrixRat_of_lt {p N : ℕ} [NeZero p] {v : Fin (descendMatrixCount p N)} (h : ↑v < p) : descendMatrixRat p N v = HeckeRing.GL2.upperTriRep p ⟨↑v, h⟩

The members of the rational descent family below index p are the upper-triangular matrices [1, v; 0, p].

@[simp]

theorem TauCeti.descendMatrixRat_of_le {p N : ℕ} [NeZero p] {v : Fin (descendMatrixCount p N)} (h : p ≤ ↑v) : descendMatrixRat p N v = HeckeRing.GL2.upperTriRep p ⟨0, ⋯⟩ * (Matrix.SpecialLinearGroup.mapGL ℚ) (descendExtraGamma p N)

The member of the rational descent family at index p, present exactly when p² does not divide N, is [1, 0; 0, p] times the extra matrix.

@[simp]

theorem TauCeti.descendMatrix_of_lt {p N : ℕ} [NeZero p] {v : Fin (descendMatrixCount p N)} (h : ↑v < p) : descendMatrix p N v = (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (HeckeRing.GL2.upperTriRep p ⟨↑v, h⟩)

The members of the descent family below index p are the upper-triangular matrices [1, v; 0, p].

@[simp]

theorem TauCeti.descendMatrix_of_le {p N : ℕ} [NeZero p] {v : Fin (descendMatrixCount p N)} (h : p ≤ ↑v) : descendMatrix p N v = (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (HeckeRing.GL2.upperTriRep p ⟨0, ⋯⟩) * (Matrix.SpecialLinearGroup.mapGL ℝ) (descendExtraGamma p N)

The member of the descent family at index p, present exactly when p² does not divide N, is [1, 0; 0, p] times the extra matrix.

@[simp]

theorem TauCeti.descendMatrixRat_det (p N : ℕ) [NeZero p] (v : Fin (descendMatrixCount p N)) : (↑(descendMatrixRat p N v)).det = ↑p

Every member of the rational descent family has determinant p. Every element of the double coset Γ₀(N) diag(1, p) Γ₀(N) that the descent sum runs over has determinant p, so this is a necessary condition for lying in it, not a characterisation of it; that these matrices lie in the double coset is not proved here.

@[simp]

theorem TauCeti.descendMatrix_det (p N : ℕ) [NeZero p] (v : Fin (descendMatrixCount p N)) : (↑(descendMatrix p N v)).det = ↑p

Every member of the descent family has determinant p: the image under algebraMap ℚ ℝ of descendMatrixRat_det.

theorem TauCeti.descendMatrix_det_pos (p N : ℕ) [NeZero p] (v : Fin (descendMatrixCount p N)) : 0 < (↑(descendMatrix p N v)).det

Every member of the descent family has positive determinant, namely p.