Hecke rings: commutativity via an anti-involution

Shimura's commutativity criterion (Proposition 3.8 of Shimura): if the monoid Δ admits an anti-involution ι preserving H and fixing every double coset HgH for g ∈ Δ, then Shimura's multiplicity is symmetric, m(g₁, g₂; d) = m(g₂, g₁; d), so the structure constants of the convolution product are symmetric and the Hecke ring 𝕋 Δ H R is commutative for every commutative semiring R. Following Shimura, the anti-involution is data on the submonoid Δ alone — it need not extend to the ambient group, and Δ contains no inverses in general — while an anti-involution of the ambient group preserving H and Δ restricts to one of the datum via HeckeAntiInvolution.ofAmbient. The classical instance is the transpose on GL₂(ℚ), which fixes the double cosets of M₂(ℤ)-integral matrices by the elementary divisor theorem.

The symmetry of the multiplicity is proved through the one-sided count DoubleCoset.multiplicity_eq_card_filter: the anti-involution induces an injection between the two count sets by transporting the representative decomposition of (σᵢ g₁)⁻¹ d through ι (Shimura's change of variables), and the two opposite injections give equality.

Checking the fixing hypothesis for a concrete datum is the work in any application, so the file also records two reductions that fixing a single double coset survives: it may be tested at any element of that coset, and a central factor the anti-involution fixes may be split off. Both trade a stubborn g for a better-behaved one without leaving the coset.

Ported from the AINTLIB LeanModularForms project (HeckeRIngs/AbstractHeckeRing/Commutativity.lean, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), per the ModularForms roadmap's dependency policy, rebuilt on the one-sided multiplicity count of the vendored Mathlib stack. The two reductions are generalised from Gamma0_AL_scalar_reduce and bar_mem_DC_of_bar_conj_mem in that project's HeckeRIngs/GLn/CongruenceHecke/AtkinLehner.lean, Apache-2.0 at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08: there they are stated for the Atkin-Lehner anti-involution of Γ₀(N), and the conjugation one is proved by hand for an H-conjugate γ₁ g γ₂, but neither argument needs more than bar_mem_doubleCoset and bar_mul.

Main definitions

• HeckeAntiInvolution: an anti-involution of the Hecke datum (Δ, H) — a monoid homomorphism Δ →* Δᵐᵒᵖ, involutive on Δ and preserving H.
• HeckeAntiInvolution.ofAmbient: restriction of an anti-involution of the ambient group.
• HeckeAntiInvolution.onHeckeCoset: the induced action on double cosets.

Main results

• HeckeAntiInvolution.multiplicity_comm: Shimura's multiplicity is symmetric when the anti-involution fixes every double coset.
• HeckeAntiInvolution.bar_mem_doubleCoset_self_of_mem: whether it fixes one double coset can be tested at any element of that coset.
• HeckeAntiInvolution.bar_mem_doubleCoset_self_mul_of_mem_centralizer: fixing survives multiplication by an element the anti-involution fixes which centralizes g and H.
• HeckeCosetModule.mul_comm_of_antiInvolution: the convolution product is commutative.
• HeckeCosetModule.commSemiringOfAntiInvolution: the resulting CommSemiring (𝕋 Δ H R).

structure HeckeAntiInvolution {G : Type u_1} [Group G] (Δ : Submonoid G) (H : Subgroup G) : Type u_1

An anti-involution of the Hecke datum (Δ, H): a monoid homomorphism Δ →* Δᵐᵒᵖ (equivalently, an anti-homomorphism of Δ) that is involutive and preserves membership in H. Following Shimura, the data lives on the submonoid Δ alone; an anti-involution of the ambient group restricts via HeckeAntiInvolution.ofAmbient. Shimura's commutativity criterion applies when it moreover fixes every double coset HgH, g ∈ Δ; see HeckeAntiInvolution.multiplicity_comm.

• toFun : ↥Δ →* (↥Δ)ᵐᵒᵖ

  The underlying homomorphism to the opposite monoid.

• involutive (g : ↥Δ) : MulOpposite.unop (self.toFun (MulOpposite.unop (self.toFun g))) = g

  The induced map on Δ is involutive.

• mem_H (g : ↥Δ) : ↑g ∈ H → ↑(MulOpposite.unop (self.toFun g)) ∈ H

  The induced map preserves membership in H.

theorem HeckeAntiInvolution.ext {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} {ι₁ ι₂ : HeckeAntiInvolution Δ H} (h : ι₁.toFun = ι₂.toFun) : ι₁ = ι₂

theorem HeckeAntiInvolution.ext_iff {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} {ι₁ ι₂ : HeckeAntiInvolution Δ H} : ι₁ = ι₂ ↔ ι₁.toFun = ι₂.toFun

def HeckeAntiInvolution.bar {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) (x : G) (hx : x ∈ Δ) : G

The underlying function of the anti-involution, as a map on elements of G lying in Δ. The membership witness is explicit; it is proof-irrelevant, so rewriting is unaffected by which witness appears.

Equations

• ι.bar x hx = ↑(MulOpposite.unop (ι.toFun ⟨x, hx⟩))

theorem HeckeAntiInvolution.bar_mem_Δ {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) (x : G) (hx : x ∈ Δ) : ι.bar x hx ∈ Δ

The anti-involution maps Δ into itself.

theorem HeckeAntiInvolution.bar_congr {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) {x y : G} (e : x = y) (hx : x ∈ Δ) (hy : y ∈ Δ) : ι.bar x hx = ι.bar y hy

bar does not depend on the membership witness; equal elements have equal images.

@[simp]

theorem HeckeAntiInvolution.bar_bar {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) {x : G} (hx : x ∈ Δ) (hbx : ι.bar x hx ∈ Δ) : ι.bar (ι.bar x hx) hbx = x

The anti-involution is an involution.

theorem HeckeAntiInvolution.bar_mul {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) {x y : G} (hx : x ∈ Δ) (hy : y ∈ Δ) (hxy : x * y ∈ Δ) : ι.bar (x * y) hxy = ι.bar y hy * ι.bar x hx

The anti-involution reverses multiplication. The memberships of the factors are explicit so that rw [ι.bar_mul hx hy] determines the factors.

@[simp]

theorem HeckeAntiInvolution.bar_one {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) (h : 1 ∈ Δ) : ι.bar 1 h = 1

The anti-involution fixes the identity.

theorem HeckeAntiInvolution.bar_mem_H {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) {x : G} (hx : x ∈ Δ) (h : x ∈ H) : ι.bar x hx ∈ H

The anti-involution preserves membership in H.

@[simp]

theorem HeckeAntiInvolution.bar_mem_H_iff {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) {x : G} (hx : x ∈ Δ) : ι.bar x hx ∈ H ↔ x ∈ H

Membership in H is preserved in both directions by the anti-involution.

def HeckeAntiInvolution.ofAmbient {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (f : G →* Gᵐᵒᵖ) (hinv : ∀ (g : G), MulOpposite.unop (f (MulOpposite.unop (f g))) = g) (hH : ∀ g ∈ H, MulOpposite.unop (f g) ∈ H) (hΔ : ∀ g ∈ Δ, MulOpposite.unop (f g) ∈ Δ) : HeckeAntiInvolution Δ H

An anti-involution of the ambient group G preserving H and Δ restricts to an anti-involution of the Hecke datum (Δ, H). The classical instance is the transpose on GL₂(ℚ) restricted to the integral matrices.

Equations

• HeckeAntiInvolution.ofAmbient f hinv hH hΔ = { toFun := { toFun := fun (g : ↥Δ) => MulOpposite.op ⟨MulOpposite.unop (f ↑g), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }, involutive := ⋯, mem_H := ⋯ }

@[simp]

theorem HeckeAntiInvolution.ofAmbient_bar {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (f : G →* Gᵐᵒᵖ) (hinv : ∀ (g : G), MulOpposite.unop (f (MulOpposite.unop (f g))) = g) (hH : ∀ g ∈ H, MulOpposite.unop (f g) ∈ H) (hΔ : ∀ g ∈ Δ, MulOpposite.unop (f g) ∈ Δ) (x : G) (hx : x ∈ Δ) : (ofAmbient f hinv hH hΔ).bar x hx = MulOpposite.unop (f x)

theorem HeckeAntiInvolution.bar_mem_doubleCoset {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) [IsHeckeTriple Δ H H] {a x : G} (ha : a ∈ Δ) (hx : x ∈ Δ) (hmem : x ∈ DoubleCoset.doubleCoset a ↑H ↑H) : ι.bar x hx ∈ DoubleCoset.doubleCoset (ι.bar a ha) ↑H ↑H

The anti-involution maps the double coset of a into the double coset of bar a.

noncomputable def HeckeAntiInvolution.onHeckeCoset {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) (D : HeckeCoset Δ H H) : HeckeCoset Δ H H

The induced action of the anti-involution on the double cosets H\Δ/H.

Equations

• ι.onHeckeCoset D = HeckeCoset.mk H H ⟨ι.bar ↑D.rep ⋯, ⋯⟩

@[simp]

theorem HeckeAntiInvolution.onHeckeCoset_mk {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) [IsHeckeTriple Δ H H] (g : ↥Δ) : ι.onHeckeCoset (HeckeCoset.mk H H g) = HeckeCoset.mk H H ⟨ι.bar ↑g ⋯, ⋯⟩

onHeckeCoset sends the class of g to the class of bar g.

@[simp]

theorem HeckeAntiInvolution.onHeckeCoset_onHeckeCoset {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) [IsHeckeTriple Δ H H] (D : HeckeCoset Δ H H) : ι.onHeckeCoset (ι.onHeckeCoset D) = D

The induced action on double cosets is an involution.

theorem HeckeAntiInvolution.bar_mem_doubleCoset_self {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) [IsHeckeTriple Δ H H] (h_fix : ∀ (D : HeckeCoset Δ H H), ι.onHeckeCoset D = D) (g : ↥Δ) : ι.bar ↑g ⋯ ∈ DoubleCoset.doubleCoset ↑g ↑H ↑H

When the anti-involution fixes every double coset, bar g lies in the double coset of g for every g ∈ Δ.

theorem HeckeAntiInvolution.bar_mem_doubleCoset_self_of_mem {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) [IsHeckeTriple Δ H H] {g x : G} (hg : g ∈ Δ) (hmem : x ∈ DoubleCoset.doubleCoset g ↑H ↑H) (hbar : ι.bar x ⋯ ∈ DoubleCoset.doubleCoset g ↑H ↑H) : ι.bar g hg ∈ DoubleCoset.doubleCoset g ↑H ↑H

Whether bar fixes a double coset can be tested at any of its elements. If some x ∈ HgH has bar x back in HgH, then bar g ∈ HgH as well.

Unlike bar_mem_doubleCoset_self, this asks nothing of the other double cosets: it is the pointwise statement, and it is what lets an argument replace g by a more convenient representative of its coset — an H-conjugate, say, or an integral witness with better entries — and still conclude for g itself.

theorem HeckeAntiInvolution.bar_mem_doubleCoset_self_mul_of_mem_centralizer {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) {s g : G} (hs : s ∈ Δ) (hg : g ∈ Δ) (hs_comm : s ∈ Subgroup.centralizer (insert g ↑H)) (hbar : ι.bar s hs = s) (hfix : ι.bar g hg ∈ DoubleCoset.doubleCoset g ↑H ↑H) : ι.bar (s * g) ⋯ ∈ DoubleCoset.doubleCoset (s * g) ↑H ↑H

A factor that bar fixes and that centralizes g and H can be split off. If bar g ∈ HgH, bar s = s, and s commutes with g and with every element of H, then bar (s * g) ∈ H (s * g) H.

The scalars of a matrix Hecke datum are the standard source of such an s: being central they lie in every centralizer (Subgroup.center_le_centralizer), and splitting one off reduces a determinant to its primitive part without disturbing the double coset.

theorem HeckeAntiInvolution.multiplicity_comm {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (ι : HeckeAntiInvolution Δ H) [IsHeckeTriple Δ H H] (h_fix : ∀ (D : HeckeCoset Δ H H), ι.onHeckeCoset D = D) (g₁ g₂ d : ↥Δ) : DoubleCoset.multiplicity H H H ↑g₁ ↑g₂ ↑d = DoubleCoset.multiplicity H H H ↑g₂ ↑g₁ ↑d

Shimura's multiplicity is symmetric under an anti-involution (Proposition 3.8 of Shimura): when the anti-involution fixes every double coset, m(g₁, g₂; d) = m(g₂, g₁; d).

theorem HeckeCosetModule.structureConstants_comm {G : Type u_1} [Group G] (R : Type u_2) {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] [Semiring R] (ι : HeckeAntiInvolution Δ H) (h_fix : ∀ (D : HeckeCoset Δ H H), ι.onHeckeCoset D = D) (g₁ g₂ : ↥Δ) : structureConstants R H H H g₁ g₂ = structureConstants R H H H g₂ g₁

The structure constants of the Hecke ring are symmetric under an anti-involution fixing every double coset.

theorem HeckeCosetModule.mul_comm_of_antiInvolution {G : Type u_1} [Group G] (R : Type u_2) {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] [CommSemiring R] (ι : HeckeAntiInvolution Δ H) (h_fix : ∀ (D : HeckeCoset Δ H H), ι.onHeckeCoset D = D) (f g : HeckeRing Δ H R) : f * g = g * f

Shimura's commutativity criterion (Proposition 3.8 of Shimura): the Hecke ring over a commutative semiring is commutative when an anti-involution fixes every double coset.

@[instance_reducible]

noncomputable def HeckeCosetModule.commSemiringOfAntiInvolution {G : Type u_1} [Group G] (R : Type u_2) {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] [CommSemiring R] (ι : HeckeAntiInvolution Δ H) (h_fix : ∀ (D : HeckeCoset Δ H H), ι.onHeckeCoset D = D) : CommSemiring (HeckeRing Δ H R)

The Hecke ring over a commutative semiring is a commutative semiring when an anti-involution fixes every double coset (Proposition 3.8 of Shimura). Not an instance: the anti-involution is data supplied per application (for GL₂ it is the transpose).

Equations

• HeckeCosetModule.commSemiringOfAntiInvolution R ι h_fix = { toSemiring := HeckeCosetModule.instSemiringHeckeRing R, mul_comm := ⋯ }