Abstract Hecke ring + modular forms over a commensurability class

[CBirkbeck]

Abstract Hecke ring + modular forms over a commensurability class

Two foundational slices toward #75 (Shimura, Ch. 3), ported from AINTLIB with mathlib-only imports. Builds on mathlib v4.31.0; sorry-free.

• ForMathlib/AbstractHeckeRing.lean — the abstract Hecke ring: HeckePair (H, Δ) with H ≤ Δ ≤ commensurator H, the double-coset quotient HeckeCoset, and the ring 𝕋 of formal ℤ-linear combinations of double cosets. Definitions only (convolution product is a follow-up).
• CommensurableLimit/ — modular forms of weight k over a commensurability class: the direct limit ModularFormCommensurable Γ₀ k of ModularForm Γ k over det-one subgroups commensurable with Γ₀, the commensurator action commRep, and range_ofLevel_eq_invariants (the level-Γ invariants are exactly ModularForm Γ.carrier k).

Part of #75.

[CBirkbeck]

Note on dcSetoid / dcRel — rationale + a suggested simplification

Why it's written this way here: dcRel and dcSetoid were ported verbatim from AINTLIB's AbstractHeckeRing/Basic.lean, to keep this slice faithful to the source. That matters because the (not-yet-ported) multiplication and ring structure are written against dcRel / HeckeCoset, so keeping the definitions identical avoids defeq / simp-normal-form drift when those land.

The redundancy: mathlib already has this exact relation. In Mathlib/GroupTheory/DoubleCoset.lean:

def setoid (H K : Set G) : Setoid G := Setoid.ker fun x => doubleCoset x H K

i.e. x ≈ y ↔ HxK = HyK — identical to our dcRel. So dcRel/dcSetoid re-implement DoubleCoset.setoid.

Two reasons it isn't simply deletable:

• HeckeCoset P := Quotient (dcSetoid P) needs a Setoid instance.
• It must be a setoid on the commensurating submonoid Δ, not on all of G (the Hecke ring is spanned by HgH for g ∈ Δ only), so mathlib's DoubleCoset.Quotient H H — a quotient of G — isn't a drop-in.

Suggested option: reuse mathlib's setoid, pulled back along Δ ↪ G, dropping dcRel and the trivial iseqv proof:

/-- The setoid on `Δ` identifying elements with the same double coset, obtained by
restricting mathlib's double-coset setoid `DoubleCoset.setoid H H` along `Δ ↪ G`. -/
instance dcSetoid (P : HeckePair G) : Setoid P.Δ :=
  Setoid.comap Subtype.val (DoubleCoset.setoid (P.H : Set G) P.H)

def HeckeCoset (P : HeckePair G) := Quotient (dcSetoid P)

Definitionally the same relation, shorter, and makes "it's the double-coset setoid restricted to Δ" explicit. ✓ Verified to compile against mathlib v4.31.0.

Trade-off: it diverges from the AINTLIB source, so a later port of the multiplication (written against dcRel) may need small adjustments for defeq / simp-normal-form.

Leaving the code as-is for now — flagging for discussion.