Comparing the Γ₀(N) and level-one double cosets

Shimura, Propositions 3.30 and 3.31. Since Γ₀(N) ≤ SL₂(ℤ) and Δ₀(N) ≤ Δ, sending Γ₀(N) α Γ₀(N) to SL₂(ℤ) α SL₂(ℤ) is well defined on double cosets:

noncomputable def toLevelOneCoset :
    HeckeCoset (Delta0 N) ((Gamma0 N).map (mapGL ℚ))
      ((Gamma0 N).map (mapGL ℚ)) →
      HeckeCoset (posDetInt 2) (SLnZ 2) (SLnZ 2)

and it is injective on the cosets whose determinant is coprime to the level (toLevelOneCoset_injOn). Injectivity is the content: two Γ₀(N)-double cosets with the same level-one double coset are recovered from it by intersecting with Δ₀(N), which is exactly doubleCoset_SLnZ_inter_Delta0_eq_doubleCoset_Gamma0_map.

This is the injectivity step towards a later good-prime comparison of R(Γ₀(N), Δ₀(N)) with the level-one Hecke ring. Neither surjectivity nor compatibility with the Hecke-ring operations is proved here: this file compares the two coset types only.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/Props.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), the cosetMap and shimura_prop_3_31 section. The bespoke Delta0_inclusion there is Submonoid.inclusion here, and AINTLIB's HeckePair bundle is Mathlib's HeckeCoset.

Main definitions

• HeckeRing.GL2.CoprimeDetCoset: coprimality of the determinant to a modulus, on a Γ₀(N)-double coset — at the level N the same condition as CoprimeDet — well defined because the coefficients have determinant one, so the determinant is constant on a coset.
• HeckeRing.GL2.toLevelOneCoset: the map Γ₀(N) α Γ₀(N) ↦ SL₂(ℤ) α SL₂(ℤ), the Γ₀ specialisation of HeckeCoset.map.

Main results

• HeckeRing.GL2.toLevelOneCoset_mk, HeckeRing.GL2.coprimeDetCoset_mk, HeckeRing.GL2.coprimeDetCoset_self_mk: the computation rules on a representative.
• HeckeRing.GL2.toLevelOneCoset_injOn: Shimura, Proposition 3.31 — toLevelOneCoset is injective on the set of coprime-determinant double cosets.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Propositions 3.30 and 3.31.

noncomputable def HeckeRing.GL2.toLevelOneCoset (N : ℕ) : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) → HeckeCoset (GLn.posDetInt 2) (GLn.SLnZ 2) (GLn.SLnZ 2)

Shimura, Proposition 3.30. Passing from a Γ₀(N)-double coset to the level-one double coset of the same element, as the HeckeCoset.map of the three inclusions Δ₀(N) ≤ Δ, Γ₀(N) ≤ SL₂(ℤ) (twice).

Equations

• HeckeRing.GL2.toLevelOneCoset N = HeckeCoset.map ⋯ ⋯ ⋯

@[simp]

theorem HeckeRing.GL2.toLevelOneCoset_mk (N : ℕ) (g : ↥(Delta0 N)) : toLevelOneCoset N (HeckeCoset.mk (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) g) = HeckeCoset.mk (GLn.SLnZ 2) (GLn.SLnZ 2) ((Submonoid.inclusion ⋯) g)

The computation rule for toLevelOneCoset: it keeps the representative and forgets the level.

def HeckeRing.GL2.CoprimeDetCoset (N M : ℕ) : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) → Prop

Coprimality of the determinant to a modulus M, as a predicate on Γ₀(N)-double cosets. At M = N it is CoprimeDet on a representative.

Equations

• HeckeRing.GL2.CoprimeDetCoset N M = Quotient.lift (fun (g : ↥(HeckeRing.GL2.Delta0 N)) => ∀ (A : Matrix (Fin 2) (Fin 2) ℤ), ↑↑g = A.map Int.cast → A.det.gcd ↑M = 1) ⋯

@[simp]

theorem HeckeRing.GL2.coprimeDetCoset_mk (N M : ℕ) (g : ↥(Delta0 N)) : CoprimeDetCoset N M (HeckeCoset.mk (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) g) ↔ ∀ (A : Matrix (Fin 2) (Fin 2) ℤ), ↑↑g = A.map Int.cast → A.det.gcd ↑M = 1

CoprimeDetCoset reads the determinant of any integral witness of a representative.

@[simp]

theorem HeckeRing.GL2.coprimeDetCoset_self_mk (N : ℕ) (g : ↥(Delta0 N)) : CoprimeDetCoset N N (HeckeCoset.mk (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) g) ↔ CoprimeDet N g

At the level itself, CoprimeDetCoset is CoprimeDet on any representative.

This has high simp priority so it fires before the general coprimeDetCoset_mk.

theorem HeckeRing.GL2.toLevelOneCoset_injOn (N : ℕ) : Set.InjOn (toLevelOneCoset N) {D : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) | CoprimeDetCoset N N D}

Shimura, Proposition 3.31. toLevelOneCoset is injective on the double cosets whose determinant is coprime to N: the level-one double coset determines the Γ₀(N) one, because intersecting it with Δ₀(N) returns the latter.