3.3 The Hecke algebra
The Hecke algebra \(\mathcal{H}(G)\) is the space of compactly supported, locally constant distributions on \(G\), equipped with convolution.
(In dependent type theory/lean) The Hecke algebra is a subtype of compactly supported distributions with the expected coercions and extensionality.
Proof
Addition, negation, and scalar multiplication agree with the underlying distribution operations.
Proof
Convolution makes \(\mathcal{H}(G)\) into a non-unital ring; associativity is inherited from convolution of distributions.
Proof