The level-descent matrices are permuted by Γ₀(N / p)

Newforms/Descent/Cosets.lean defines the family descendMatrix p N that Miyake's level descent at a prime p runs over, and leaves open both that the family is a set of coset representatives and that the associated slash sum descends the level. This file proves neither of those; it supplies a prerequisite for both: for p ∣ N, right multiplication by an element of Γ₀(N / p) permutes the family, up to left multiplication by an element of Γ₀(N), and the Γ₀(N) witness has the lower-right entry of γ modulo N / p. The two cases p² ∣ N and p ∥ N have different index maps and are proved separately.

The permutation is named rather than left existential, because that is what the descent consumes: a slash by γ ∈ Γ₀(N / p) sends the summand at v to the summand at the image of v, and the sum is unchanged only because that map is a bijection of the index set.

The case p² ∣ N

The hypothesis enters twice. It collapses descendMatrixCount p N to p, so every index is that of an upper-triangular member; and it gives p ∣ N / p, which places γ in Γ₀(p), and that is what makes the offset map HeckeRing.GL2.upperTriShift a bijection (descendShift).

The case p ∥ N: the index line

With p + 1 members the natural index set is the projective line over ZMod p: the upper-triangular member [1, j; 0, p] sits at the affine point j, the extra member [1, 0; 0, p] γ_p (for γ_p = descendExtraGamma p N) at ∞ (descendIndexEquiv). On that line the descent's index map j ↦ (b + j d) / (a + j c) is the Möbius action of moebiusGL (LinearAlgebra/Matrix/GeneralLinearGroup/MoebiusZMod.lean) at γ reduced modulo p, so it is a bijection for free (descendIndexShift_bijective): the affine index with a + j c ≡ 0 — which exists exactly when p ∤ c — goes to ∞, and ∞ comes back to d / c.

The case p ∥ N: the factorisation

Every case is the general upper-triangular factorisation HeckeRing.GL2.exists_mem_Gamma0_upperTriRep_mul_of_isUnit, applied to γ twisted by γ_p: to γ itself at an affine index with a + j c a unit, to γ γ_p⁻¹ at the degenerate affine index, to γ_p γ at ∞ when p ∤ c, and to γ_p γ γ_p⁻¹ at ∞ when p ∣ c. Since γ_p ≡ S = [0, -1; 1, 0] (mod p) the twists have computable residues, which is what makes the denominators units and pins the target indices; since γ_p ≡ 1 (mod N / p) every witness has the lower-right entry of γ modulo N / p, which is what transporting a nebentypus needs.

Main definitions

• TauCeti.descendShift: at p² ∣ N, HeckeRing.GL2.upperTriShift carried to Fin (descendMatrixCount p N) along descendMatrixCount p N = p.
• TauCeti.descendIndexEquiv: at p ∥ N, Fin (descendMatrixCount p N) ≃ OnePoint (ZMod p).
• TauCeti.descendIndexGL: moebiusGL of γ modulo p, the element whose action is the descent's index map at p ∥ N.
• TauCeti.descendIndexShift: that action read back on the index set.

Main results

• TauCeti.cast_descendShift, TauCeti.descendShift_bijective: at p² ∣ N the index map is upperTriShift transported, and a bijection.
• TauCeti.exists_mem_Gamma0_descendMatrix_mul: at p² ∣ N, descendMatrix p N v * γ = α * descendMatrix p N (descendShift … v) for some α ∈ Γ₀(N) whose lower-right entry is γ 1 1 - γ 1 0 * shift v.
• TauCeti.descendIndexShift_bijective: at p ∥ N the index map is a bijection.
• TauCeti.exists_mem_Gamma0_descendMatrix_mul_of_not_sq_dvd: at p ∥ N, descendMatrix p N v * γ = α * descendMatrix p N (descendIndexShift … v) for some α ∈ Γ₀(N) with α 1 1 ≡ γ 1 1 (mod N / p); assembled from four private cases, one per value of the index map.
• TauCeti.descendIndexShift_val_of_isUnit, TauCeti.descendIndexShift_val_of_eq_zero, TauCeti.descendIndexShift_val_of_le_of_ne_zero and TauCeti.descendIndexShift_val_of_le_of_eq_zero: the value of the index map in each case.

Scope

A statement uniform in the two cases is not made. The completeness of the family as a coset system, the invariance of the slash sum and the behaviour at cusps are separate statements and none of them is claimed here.

Corresponds to descendCosetList_action_upper_tri_clean (the p² ∣ N case) and to descendCosetList_action_upper_tri_extra, descendCosetList_action_extra and descendCosetList_action (the p² ∤ N branch, including its Gamma0MapUnits compatibility) of the AINTLIB LeanModularForms project (LeanModularForms/StrongMultiplicityOne/DescentCosets.lean, Chris Birkbeck, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms). The source handles the pole by a direct matrix computation and proves bijectivity of the index map by an injectivity argument on Fin (p + 1); here both come from the projective line.

def TauCeti.descendShift (p N : ℕ) [NeZero p] (hpsq : p ^ 2 ∣ N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (v : Fin (descendMatrixCount p N)) : Fin (descendMatrixCount p N)

The offset map on the descent index set. HeckeRing.GL2.upperTriShift carried across descendMatrixCount p N = p, which holds because p² ∣ N. This is the map the descent's slash sum reindexes along.

Equations

• TauCeti.descendShift p N hpsq γ v = (finCongr ⋯).symm (HeckeRing.GL2.upperTriShift p γ ((finCongr ⋯) v))

@[simp]

theorem TauCeti.cast_descendShift {p N : ℕ} [NeZero p] (hpsq : p ^ 2 ∣ N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (v : Fin (descendMatrixCount p N)) : Fin.cast ⋯ (descendShift p N hpsq γ v) = HeckeRing.GL2.upperTriShift p γ (Fin.cast ⋯ v)

The defining property of descendShift: transported to Fin p, it is HeckeRing.GL2.upperTriShift. Read the map off this rather than off the definition, whose finCongr plumbing carries a proof argument. Stated with Fin.cast because that, not finCongr, is the simp normal form.

@[simp]

theorem TauCeti.descendShift_val {p N : ℕ} [NeZero p] (hpsq : p ^ 2 ∣ N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (v : Fin (descendMatrixCount p N)) : ↑(descendShift p N hpsq γ v) = ↑(HeckeRing.GL2.upperTriShift p γ (Fin.cast ⋯ v))

The same, on underlying naturals, which is the form the descendMatrix branches read.

theorem TauCeti.descendShift_bijective {p N : ℕ} [NeZero p] (hpsq : p ^ 2 ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγp : γ ∈ CongruenceSubgroup.Gamma0 p) : Function.Bijective (descendShift p N hpsq γ)

The offset map is a bijection of the descent index set. The hypothesis is γ ∈ Γ₀(p), which is all bijectivity needs. The descent acts by γ ∈ Γ₀(N / p), and p² ∣ N puts that group inside Γ₀(p): a descent caller turns p² ∣ N into p ∣ N / p with Nat.dvd_div_of_mul_dvd and feeds that to Gamma0_le_Gamma0_of_dvd. Reindexing the descent's slash sum along this map is what the bijection is for.

theorem TauCeti.exists_mem_Gamma0_descendMatrix_mul (p N : ℕ) [NeZero p] (hpsq : p ^ 2 ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 (N / p)) (v : Fin (descendMatrixCount p N)) : ∃ α ∈ CongruenceSubgroup.Gamma0 N, ↑α 1 1 = ↑γ 1 1 - ↑γ 1 0 * ↑↑(descendShift p N hpsq γ v) ∧ descendMatrix p N v * (Matrix.SpecialLinearGroup.mapGL ℝ) γ = (Matrix.SpecialLinearGroup.mapGL ℝ) α * descendMatrix p N (descendShift p N hpsq γ v)

The descent family is permuted by Γ₀(N / p) when p² ∣ N. For γ ∈ Γ₀(N / p), the product descendMatrix p N v * γ is an element of Γ₀(N) times the member of the family at descendShift p N hpsq γ v — and that map is a bijection, by descendShift_bijective.

The target index is named rather than existentially quantified, because reindexing the descent's slash sum needs the permutation itself, not merely that some member of the family appears.

The lower-right entry of α is given as an equation, as exists_mem_Gamma0_upperTriRep_mul gives it, rather than as a congruence: the modulus at which it is useful varies with the caller. Transporting a nebentypus through the descent reads off from it that α and γ agree modulo N / p, since N / p ∣ γ 1 0.

When p exactly divides N

theorem TauCeti.neZero_of_fact_prime {p : ℕ} [Fact (Nat.Prime p)] : NeZero p

A prime is nonzero. Primality is what the projective line over ZMod p needs, and it supplies the NeZero p that the descent family and the offset map need throughout this file.

def TauCeti.descendIndexEquiv (p N : ℕ) [NeZero p] (hpsq : ¬p ^ 2 ∣ N) : Fin (descendMatrixCount p N) ≃ OnePoint (ZMod p)

When p² does not divide N, the descent's index set is the projective line over ZMod p. descendMatrixCount p N is p + 1 then, and Fin (p + 1) ≃ Option (Fin p) ≃ Option (ZMod p), which is OnePoint (ZMod p): the upper-triangular members are the affine points and the extra representative is ∞.

Equations

• TauCeti.descendIndexEquiv p N hpsq = (finCongr ⋯).trans (finSuccEquivLast.trans (ZMod.finEquiv p).optionCongr)

@[simp]

theorem TauCeti.descendIndexEquiv_apply_of_lt {p N : ℕ} [NeZero p] (hpsq : ¬p ^ 2 ∣ N) {v : Fin (descendMatrixCount p N)} (hv : ↑v < p) : (descendIndexEquiv p N hpsq) v = ↑↑↑v

An index below p is the affine point it names.

@[simp]

theorem TauCeti.descendIndexEquiv_apply_of_le {p N : ℕ} [NeZero p] (hpsq : ¬p ^ 2 ∣ N) {v : Fin (descendMatrixCount p N)} (hv : p ≤ ↑v) : (descendIndexEquiv p N hpsq) v = OnePoint.infty

The index p is the point at infinity.

@[simp]

theorem TauCeti.descendIndexEquiv_symm_coe_val {p N : ℕ} [NeZero p] (hpsq : ¬p ^ 2 ∣ N) (k : ZMod p) : ↑((descendIndexEquiv p N hpsq).symm ↑k) = k.val

The index of an affine point is its representative below p.

@[simp]

theorem TauCeti.descendIndexEquiv_symm_infty_val {p N : ℕ} [NeZero p] (hpsq : ¬p ^ 2 ∣ N) : ↑((descendIndexEquiv p N hpsq).symm OnePoint.infty) = p

The index of the point at infinity is p.

noncomputable def TauCeti.descendIndexGL (p : ℕ) [Fact (Nat.Prime p)] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : GL (Fin 2) (ZMod p)

The Möbius element of the descent at γ: moebiusGL of γ reduced modulo p, whose action on the projective line is the descent's index map j ↦ (b + j d) / (a + j c).

Equations

• TauCeti.descendIndexGL p γ = TauCeti.moebiusGL ((↑γ).map ⇑(Int.castRingHom (ZMod p))) ⋯

theorem TauCeti.descendIndexGL_smul_coe {p : ℕ} [Fact (Nat.Prime p)] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (k : ZMod p) : descendIndexGL p γ • ↑k = if ↑(↑γ 1 0) * k + ↑(↑γ 0 0) = 0 then OnePoint.infty else ↑((↑(↑γ 1 1) * k + ↑(↑γ 0 1)) / (↑(↑γ 1 0) * k + ↑(↑γ 0 0)))

The value of the descent's Möbius element at an affine point, in the entries of γ.

theorem TauCeti.descendIndexGL_smul_infty {p : ℕ} [Fact (Nat.Prime p)] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : descendIndexGL p γ • OnePoint.infty = if ↑(↑γ 1 0) = 0 then OnePoint.infty else ↑(↑(↑γ 1 1) / ↑(↑γ 1 0))

The value of the descent's Möbius element at the point at infinity.

@[simp]

theorem TauCeti.descendIndexGL_smul_coe_of_isUnit {p : ℕ} [Fact (Nat.Prime p)] {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} {j : Fin p} (hA : ↑(↑γ 0 0) + ↑↑j * ↑(↑γ 1 0) ≠ 0) : descendIndexGL p γ • ↑↑↑j = ↑↑↑(HeckeRing.GL2.upperTriShift p γ j)

An affine index with a + j c a unit goes to the offset map's value.

@[simp]

theorem TauCeti.descendIndexGL_smul_coe_of_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} {j : Fin p} (h : ↑(↑γ 0 0 + ↑↑j * ↑γ 1 0) = 0) : descendIndexGL p γ • ↑↑↑j = OnePoint.infty

The degenerate affine index goes to infinity. When a + j c ≡ 0, the offset map has no affine target — which is why the index set is the projective line, not Fin p.

@[simp]

theorem TauCeti.descendIndexGL_smul_infty_of_ne_zero {p : ℕ} [Fact (Nat.Prime p)] {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hc : ↑(↑γ 1 0) ≠ 0) : descendIndexGL p γ • OnePoint.infty = ↑(↑(↑γ 1 1) / ↑(↑γ 1 0))

Infinity comes back to d / c when p ∤ c.

@[simp]

theorem TauCeti.descendIndexGL_smul_infty_of_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hc : ↑(↑γ 1 0) = 0) : descendIndexGL p γ • OnePoint.infty = OnePoint.infty

Infinity is fixed when p ∣ c.

noncomputable def TauCeti.descendIndexShift (p N : ℕ) [Fact (Nat.Prime p)] (hpsq : ¬p ^ 2 ∣ N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (v : Fin (descendMatrixCount p N)) : Fin (descendMatrixCount p N)

The index map when p² does not divide N: the Möbius action of descendIndexGL p γ on the projective line, read through descendIndexEquiv. It is a bijection (descendIndexShift_bijective), and the descent's factorisation sends the member of the family at v to the member at descendIndexShift p N hpsq γ v.

Equations

• TauCeti.descendIndexShift p N hpsq γ v = (TauCeti.descendIndexEquiv p N hpsq).symm (TauCeti.descendIndexGL p γ • (TauCeti.descendIndexEquiv p N hpsq) v)

theorem TauCeti.descendIndexShift_bijective {p N : ℕ} [Fact (Nat.Prime p)] (hpsq : ¬p ^ 2 ∣ N) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Function.Bijective (descendIndexShift p N hpsq γ)

The index map is a bijection, because a group action is.

@[simp]

theorem TauCeti.descendIndexShift_val_of_isUnit {p N : ℕ} [Fact (Nat.Prime p)] (hpsq : ¬p ^ 2 ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} {v : Fin (descendMatrixCount p N)} (hv : ↑v < p) (hA : ↑(↑γ 0 0) + ↑↑v * ↑(↑γ 1 0) ≠ 0) : ↑(descendIndexShift p N hpsq γ v) = ↑(HeckeRing.GL2.upperTriShift p γ ⟨↑v, hv⟩)

The value of the index map at an affine index whose denominator is a unit: the offset map's value.

@[simp]

theorem TauCeti.descendIndexShift_val_of_eq_zero {p N : ℕ} [Fact (Nat.Prime p)] (hpsq : ¬p ^ 2 ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} {v : Fin (descendMatrixCount p N)} (hv : ↑v < p) (h0 : ↑(↑γ 0 0 + ↑↑v * ↑γ 1 0) = 0) : ↑(descendIndexShift p N hpsq γ v) = p

The value of the index map at the degenerate affine index: the extra index p.

@[simp]

theorem TauCeti.descendIndexShift_val_of_le_of_eq_zero {p N : ℕ} [Fact (Nat.Prime p)] (hpsq : ¬p ^ 2 ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} {v : Fin (descendMatrixCount p N)} (hv : p ≤ ↑v) (hc : ↑(↑γ 1 0) = 0) : ↑(descendIndexShift p N hpsq γ v) = p

The value of the index map at the extra index when p ∣ c: the extra index itself.

The residues of the extra matrix and of its twists

The four cases of the factorisation

@[simp]

theorem TauCeti.descendIndexShift_val_of_le_of_ne_zero {p N : ℕ} [Fact (Nat.Prime p)] (hpN : p ∣ N) (hpsq : ¬p ^ 2 ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} {v : Fin (descendMatrixCount p N)} (hv : p ≤ ↑v) (hc : ↑(↑γ 1 0) ≠ 0) : ↑(descendIndexShift p N hpsq γ v) = ↑(HeckeRing.GL2.upperTriShift p (descendExtraGamma p N * γ) ⟨0, ⋯⟩)

The value of the index map at the extra index when p ∤ c: the offset map of the twist γ_p γ at 0, that is d / c.

theorem TauCeti.exists_mem_Gamma0_descendMatrix_mul_of_not_sq_dvd {p N : ℕ} [Fact (Nat.Prime p)] (hpN : p ∣ N) (hpsq : ¬p ^ 2 ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 (N / p)) (v : Fin (descendMatrixCount p N)) : ∃ α ∈ CongruenceSubgroup.Gamma0 N, ↑(↑α 1 1) = ↑(↑γ 1 1) ∧ descendMatrix p N v * (Matrix.SpecialLinearGroup.mapGL ℝ) γ = (Matrix.SpecialLinearGroup.mapGL ℝ) α * descendMatrix p N (descendIndexShift p N hpsq γ v)

The descent family is permuted by Γ₀(N / p) when p exactly divides N. For γ ∈ Γ₀(N / p), the product descendMatrix p N v * γ is an element of Γ₀(N) times the member of the family at descendIndexShift p N hpsq γ v, a bijection of the index set by descendIndexShift_bijective; and the Γ₀(N) witness has the lower-right entry of γ modulo N / p.