Hecke Algebra

This file defines the Hecke algebra as the space of locally constant, compactly supported distributions on a totally disconnected locally compact group.

def HeckeAlgebra (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : Type u_1

The Hecke algebra of G is the set of locally constant, compactly supported distributions. This is defined as a subtype of CptSupportDistribution_td G.

Equations

• HeckeAlgebra G = { F : CptSupportDistribution_td G // F.IsLocallyConstant }

instance HeckeAlgebra.instFunLikeCptSupportLocConst_tdComplex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : FunLike (HeckeAlgebra G) (CptSupportLocConst_td G) ℂ

Equations

• HeckeAlgebra.instFunLikeCptSupportLocConst_tdComplex = { coe := fun (F : HeckeAlgebra G) => ⇑↑F, coe_injective' := ⋯ }

def HeckeAlgebra.toDistribution {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : HeckeAlgebra G) : CptSupportDistribution_td G

The underlying compactly supported distribution.

Equations

• F.toDistribution = ↑F

@[simp]

theorem HeckeAlgebra.coe_toDistribution {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : HeckeAlgebra G) : ⇑F.toDistribution = ⇑F

Coercion to function.

theorem HeckeAlgebra.ext {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F F' : HeckeAlgebra G} (h : ∀ (φ : CptSupportLocConst_td G), F φ = F' φ) : F = F'

Extensionality for HeckeAlgebra.

theorem HeckeAlgebra.ext_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {F F' : HeckeAlgebra G} : F = F' ↔ ∀ (φ : CptSupportLocConst_td G), F φ = F' φ

Algebraic Structure

theorem HeckeAlgebra.zero_isLocallyConstant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : CptSupportDistribution_td.IsLocallyConstant 0

The zero distribution is locally constant (trivially, for any H).

instance HeckeAlgebra.instZero {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : Zero (HeckeAlgebra G)

Zero element of the Hecke algebra.

Equations

• HeckeAlgebra.instZero = { zero := ⟨0, ⋯⟩ }

@[simp]

theorem HeckeAlgebra.coe_zero {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : ⇑0 = 0

noncomputable def HeckeAlgebra.addDist {G : Type u_1} [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F F' : CptSupportDistribution_td G) : CptSupportDistribution_td G

Addition of compactly supported distributions.

Equations

• HeckeAlgebra.addDist F F' = { toDistribution_td := { toFun := fun (φ : CptSupportLocConst_td G) => F φ + F' φ, map_add' := ⋯, map_smul' := ⋯ }, hasCompactSupport' := ⋯ }

theorem HeckeAlgebra.addDist_isLocallyConstant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F F' : CptSupportDistribution_td G) (hF : F.IsLocallyConstant) (hF' : F'.IsLocallyConstant) : (addDist F F').IsLocallyConstant

Sum of locally constant distributions is locally constant.

noncomputable instance HeckeAlgebra.instAdd {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : Add (HeckeAlgebra G)

Addition of elements in the Hecke algebra.

Equations

• HeckeAlgebra.instAdd = { add := fun (F F' : HeckeAlgebra G) => ⟨HeckeAlgebra.addDist ↑F ↑F', ⋯⟩ }

@[simp]

theorem HeckeAlgebra.coe_add {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F F' : HeckeAlgebra G) : ⇑(F + F') = fun (φ : CptSupportLocConst_td G) => F φ + F' φ

noncomputable def HeckeAlgebra.negDist {G : Type u_1} [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) : CptSupportDistribution_td G

Negation of a compactly supported distribution.

Equations

• HeckeAlgebra.negDist F = { toDistribution_td := { toFun := fun (φ : CptSupportLocConst_td G) => -F φ, map_add' := ⋯, map_smul' := ⋯ }, hasCompactSupport' := ⋯ }

theorem HeckeAlgebra.negDist_isLocallyConstant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : CptSupportDistribution_td G) (hF : F.IsLocallyConstant) : (negDist F).IsLocallyConstant

Negation preserves local constancy.

noncomputable instance HeckeAlgebra.instNeg {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : Neg (HeckeAlgebra G)

Negation in the Hecke algebra.

Equations

• HeckeAlgebra.instNeg = { neg := fun (F : HeckeAlgebra G) => ⟨HeckeAlgebra.negDist ↑F, ⋯⟩ }

@[simp]

theorem HeckeAlgebra.coe_neg {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F : HeckeAlgebra G) : ⇑(-F) = fun (φ : CptSupportLocConst_td G) => -F φ

noncomputable def HeckeAlgebra.smulDist {G : Type u_1} [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (c : ℂ) (F : CptSupportDistribution_td G) : CptSupportDistribution_td G

Scalar multiplication of a compactly supported distribution by ℂ.

Equations

• HeckeAlgebra.smulDist c F = { toDistribution_td := { toFun := fun (φ : CptSupportLocConst_td G) => c * F φ, map_add' := ⋯, map_smul' := ⋯ }, hasCompactSupport' := ⋯ }

theorem HeckeAlgebra.smulDist_isLocallyConstant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (c : ℂ) (F : CptSupportDistribution_td G) (hF : F.IsLocallyConstant) : (smulDist c F).IsLocallyConstant

Scalar multiplication preserves local constancy.

noncomputable instance HeckeAlgebra.instSMulComplex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : SMul ℂ (HeckeAlgebra G)

Scalar multiplication in the Hecke algebra.

Equations

• HeckeAlgebra.instSMulComplex = { smul := fun (c : ℂ) (F : HeckeAlgebra G) => ⟨HeckeAlgebra.smulDist c ↑F, ⋯⟩ }

@[simp]

theorem HeckeAlgebra.coe_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (c : ℂ) (F : HeckeAlgebra G) : ⇑(c • F) = fun (φ : CptSupportLocConst_td G) => c * F φ

theorem HeckeAlgebra.conv_isLocallyConstant {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F F' : CptSupportDistribution_td G) (hF : F.IsLocallyConstant) (hF' : F'.IsLocallyConstant) : (F.conv F').IsLocallyConstant

Convolution preserves local constancy.

noncomputable instance HeckeAlgebra.instMul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : Mul (HeckeAlgebra G)

Convolution product in the Hecke algebra.

Equations

• HeckeAlgebra.instMul = { mul := fun (F F' : HeckeAlgebra G) => ⟨(↑F).conv ↑F', ⋯⟩ }

@[simp]

theorem HeckeAlgebra.coe_mul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (F F' : HeckeAlgebra G) (φ : CptSupportLocConst_td G) : (F * F') φ = F ((↑F').convolveTestFun' φ)

noncomputable instance HeckeAlgebra.instAddCommGroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : AddCommGroup (HeckeAlgebra G)

The Hecke algebra is an additive commutative group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance HeckeAlgebra.instModuleComplex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : Module ℂ (HeckeAlgebra G)

The Hecke algebra is a ℂ-module.

Equations

• HeckeAlgebra.instModuleComplex = { toSMul := HeckeAlgebra.instSMulComplex, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

theorem HeckeAlgebra.mul_assoc' {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] (a b c : HeckeAlgebra G) : a * b * c = a * (b * c)

Convolution is associative in the Hecke algebra.

noncomputable instance HeckeAlgebra.instNonUnitalRing {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : NonUnitalRing (HeckeAlgebra G)

The Hecke algebra is a (non-unital) ring.

Equations

• One or more equations did not get rendered due to their size.