Hecke Rings: Commutativity via Anti-Involution

Shimura Proposition 3.8: if an arithmetic group pair admits an anti-automorphism ι : G →* Gᵐᵒᵖ that preserves H and Δ and fixes every double coset, then the Hecke ring 𝕋 P ℤ is commutative.

structure HeckeRing.AntiInvolution {G : Type u_1} [Group G] (P : HeckePair G) : Type u_1

An anti-involution of an HeckePair: ι : G →* Gᵐᵒᵖ, involutive and preserving both H and Δ.

• toFun : G →* Gᵐᵒᵖ

  The underlying anti-homomorphism G →* Gᵐᵒᵖ.

• involutive (g : G) : MulOpposite.unop (self.toFun (MulOpposite.unop (self.toFun g))) = g
• map_H (g : G) : g ∈ P.H → MulOpposite.unop (self.toFun g) ∈ P.H
• map_Δ (g : G) : g ∈ P.Δ → MulOpposite.unop (self.toFun g) ∈ P.Δ

def HeckeRing.AntiInvolution.bar {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (g : G) : G

The underlying function of the anti-involution, mapping g to ι(g) viewed in G.

Equations

• ι.bar g = MulOpposite.unop (ι.toFun g)

@[simp]

theorem HeckeRing.AntiInvolution.bar_bar {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (g : G) : ι.bar (ι.bar g) = g

The anti-involution is an involution: bar(bar(g)) = g.

theorem HeckeRing.AntiInvolution.bar_mul {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (a b : G) : ι.bar (a * b) = ι.bar b * ι.bar a

The anti-involution reverses multiplication: bar(ab) = bar(b) * bar(a).

theorem HeckeRing.AntiInvolution.bar_one {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) : ι.bar 1 = 1

The anti-involution fixes the identity.

theorem HeckeRing.AntiInvolution.bar_inv {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (g : G) : ι.bar g⁻¹ = (ι.bar g)⁻¹

The anti-involution commutes with inversion.

theorem HeckeRing.AntiInvolution.bar_injective {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) : Function.Injective ι.bar

The anti-involution is injective.

theorem HeckeRing.AntiInvolution.bar_mem_H {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) {g : G} (hg : g ∈ P.H) : ι.bar g ∈ P.H

The anti-involution preserves membership in H.

theorem HeckeRing.AntiInvolution.bar_mem_Δ {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) {g : G} (hg : g ∈ P.Δ) : ι.bar g ∈ P.Δ

The anti-involution preserves membership in Δ.

theorem HeckeRing.AntiInvolution.bar_doubleCoset_eq {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (g₁ g₂ : G) (h : DoubleCoset.doubleCoset g₁ ↑P.H ↑P.H = DoubleCoset.doubleCoset g₂ ↑P.H ↑P.H) : DoubleCoset.doubleCoset (ι.bar g₁) ↑P.H ↑P.H = DoubleCoset.doubleCoset (ι.bar g₂) ↑P.H ↑P.H

The anti-involution preserves double coset equality.

noncomputable def HeckeRing.AntiInvolution.onHeckeCoset {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (D : HeckeCoset P) : HeckeCoset P

The induced action of the anti-involution on double cosets, defined via Quotient.lift.

Equations

• ι.onHeckeCoset D = Quotient.lift (fun (g : ↥P.Δ) => ⟦⟨ι.bar ↑g, ⋯⟩⟧) ⋯ D

theorem HeckeRing.AntiInvolution.onHeckeCoset_mk {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (g : ↥P.Δ) : ι.onHeckeCoset ⟦g⟧ = ⟦⟨ι.bar ↑g, ⋯⟩⟧

onHeckeCoset ⟦g⟧ equals ⟦bar(g)⟧.

theorem HeckeRing.AntiInvolution.onHeckeCoset_toSet {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (D : HeckeCoset P) : (ι.onHeckeCoset D).toSet = DoubleCoset.doubleCoset (ι.bar ↑D.rep) ↑P.H ↑P.H

The set underlying onHeckeCoset D is the double coset of the barred representative.

theorem HeckeRing.AntiInvolution.onHeckeCoset_involutive {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) : Function.Involutive ι.onHeckeCoset

The action on double cosets is involutive: onHeckeCoset(onHeckeCoset(D)) = D.

theorem HeckeRing.AntiInvolution.heckeMultiplicity_comm_of_onHeckeCoset_eq {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (h_fix : ∀ (D : HeckeCoset P), ι.onHeckeCoset D = D) (D₁ D₂ D : HeckeCoset P) : heckeMultiplicity P D₁.rep D₂.rep D.rep = heckeMultiplicity P D₂.rep D₁.rep D.rep

When the anti-involution fixes all double cosets, the multiplicity is symmetric: heckeMultiplicity(D₁, D₂, D) = heckeMultiplicity(D₂, D₁, D) (Shimura Proposition 3.8).

theorem HeckeRing.AntiInvolution.m_comm_of_onHeckeCoset_eq {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (h_fix : ∀ (D : HeckeCoset P), ι.onHeckeCoset D = D) (D₁ D₂ : HeckeCoset P) : m P D₁.rep D₂.rep = m P D₂.rep D₁.rep

When the anti-involution fixes all double cosets, the multiplication finsupp is symmetric: m(D₁, D₂) = m(D₂, D₁).

theorem HeckeRing.AntiInvolution.mul_comm_of_antiInvolution {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (h_fix : ∀ (D : HeckeCoset P), ι.onHeckeCoset D = D) (f g : 𝕋 P ℤ) : f * g = g * f

Shimura Proposition 3.8: the Hecke ring is commutative when the anti-involution fixes every double coset.

@[reducible]

noncomputable def HeckeRing.instCommRingOfAntiInvolution {G : Type u_1} [Group G] {P : HeckePair G} (ι : AntiInvolution P) (h_fix : ∀ (D : HeckeCoset P), ι.onHeckeCoset D = D) : CommRing (𝕋 P ℤ)

Shimura Proposition 3.8: CommRing (𝕋 P ℤ) from an anti-involution fixing every double coset.

Equations

• HeckeRing.instCommRingOfAntiInvolution ι h_fix = { toRing := HeckeRing.instRing P, mul_comm := ⋯ }