Abstract Hecke ring: full construction (HeckePair, double-coset quotient, 𝕋, convolution ring)

[CBirkbeck]

Abstract Hecke ring — full construction

Adds the complete construction of the abstract Hecke ring (à la Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Ch. 3) to LeanBridge/ForMathlib/AbstractHeckeRing/. This supersedes the definition-only draft #76 and addresses the first item of #75.

For an arithmetic pair (H, Δ) with H ≤ Δ ≤ commensurator(H):

• HeckeRing.HeckePair, the double-coset quotient HeckeRing.HeckeCoset, and the Hecke ring HeckeRing.𝕋 (Basic);
• the convolution product and its associativity (Multiplication, Associativity), assembled into the Ring structure (Ring);
• the Hecke module over left cosets (Module), commutativity from an anti-involution (Commutativity), the degree map (Degree), and stabilizer/conjugation lemmas (StabConjugation).

8 files, ~3100 lines, no sorry/axiom. Ported from the AINTLIB project (projects/LeanModularForms/.../HeckeRIngs/AbstractHeckeRing), imports rewritten to LeanBridge.ForMathlib.*; imports are mathlib-only.

Verification

• ✅ lake build LeanBridge.ForMathlib.AbstractHeckeRing — builds clean against the pinned mathlib v4.31.0 (1830 jobs, exit 0). No drift from the v4.31.0-rc2 it was developed on.
• ✅ /cleanup (file-level): already mathlib-clean — copyright + module docstrings throughout, no in-body dividers, no set_option, zero λ/$/push_neg, no sorry/deprecations. The one fix applied was wrapping 36 over-long lines to ≤100 cols (line breaks only — no semantic/name/proof changes); build stayed green. Per-declaration golf was intentionally skipped to keep the port faithful to the AINTLIB source.

/mathlib-quality:mathlibable assessment — YES (add to mathlib)

• Standard form (Phase 3): the construction matches the classical Shimura R(Γ,Δ) / "Hecke algebra of a pair" exactly (free module on H\Δ/H, convolution product, (H,Δ) a Hecke pair) — Wikipedia, nLab.
• Not in mathlib (Phase 5): mathlib has Mathlib.GroupTheory.DoubleCoset and Mathlib.GroupTheory.Commensurable but no Hecke algebra/ring/operator.
• Not composable (Phase 6): the convolution product + ring axioms are genuine new content, not a short composition of mathlib primitives.
• Generality: the (H, Δ)-Hecke-pair form is maximally general (more general than the "commensurated subgroup" form); 𝕋 P Z is already over an arbitrary [CommRing Z]. Recommended refinement before a mathlib PR: generalise the ring structure from Z = ℤ to an arbitrary commutative ring R (the module is already general; only Mul/Ring are ℤ-pinned). MODERATE re-proof — a /generalise follow-up.
• Defeq/diamond (Phase 4.5): LOW — 𝕋 is a sealed def over Finsupp, which correctly prevents the convolution Mul from colliding with Finsupp's pointwise Mul.
• Suggested mathlib home: Mathlib/GroupTheory/HeckeRing/ (or Mathlib/RepresentationTheory/).

Part of #75.