Dependencies

Define the category of non-degenerated modules over the Hecke algebra.

A continuous representation is a representation \(\rho : G \to \mathrm{Aut}_R(V)\) whose action map \((g,v) \mapsto \rho (g)v\) is continuous. (In Lean this is defined as a subtype of Representation equipped with the continuity proof.)

We have the action map \(G \times V \to V\) associated to a continuous representation.

Given a representation \(\rho \) and a proof of continuity of the action map, we obtain a continuous representation.

Assuming \(G\) has continuous multiplication, if \(N \trianglelefteq G\) and \(\rho \) is trivial on \(N\), then \(\rho \) descends to a continuous representation of \(G/N\).

If \(M\) is an object of \(\mathrm{TopModuleCat}(R)\) equipped with a continuous action by \(R\)-linear maps, this yields a continuous representation.

A continuous representation restricts to any subgroup \(H \le G\).

The underlying topological \(R\)-module is bundled as an object of \(\mathrm{TopModuleCat}(R)\).

The trivial representation is a continuous representation.

The convolution of \(F\) and \(D\) is defined by

Given \(D\) and \(\varphi \), the function \(x \mapsto D(R_x\varphi )\) is locally constant and compactly supported, and hence defines an element of \(C_c^{\infty }(G)\).

A compactly supported distribution is a distribution whose support is compact.

We write \(C_c^{\infty }(X)\) for locally constant functions with compact support.

Translations of test functions are defined and satisfy the expected identities.

The category \(\mathrm{CRep}_R(G)\) is the category of continuous actions of \(G\) on topological \(R\)-modules, implemented as a category of continuous \(G\)-actions in \(\mathrm{TopModuleCat}(R)\).

For \(V \in \mathrm{CRep}_R(G)\) we extract the underlying action and define the evaluation map \(\mathrm{act}(g,v)\).

A continuous representation (as defined above) can be lifted to an object of \(\mathrm{CRep}_R(G)\).

A representation with a compatible topology and continuous action determines an object of \(\mathrm{CRep}_R(G)\).

A representation with a jointly continuous action determines a continuous action object in \(\mathrm{TopModuleCat}(R)\).

Each group element acts by a continuous endomorphism of the underlying topological module, and these assemble into a monoid homomorphism \(G \to \mathrm{End}(V)\).

Every object in \(\mathrm{CRep}_R(G)\) yields a continuous representation on its underlying type.

There is a forgetful functor \(\mathrm{CRep}_R(G) \to \mathrm{Rep}_R(G)\).

There is a forgetful functor to \(\mathrm{TopModuleCat}(R)\) and an induced map on morphisms.

The delta distribution at \(g\) evaluates test functions at \(g\).

Left and right translation actions are defined by dualizing the actions on test functions.

A distribution on \(X\) restricts to a subspace \(Z\) by evaluating on the extension by zero of test functions on \(Z\).

The support of a distribution \(F\) consists of those points \(x\) such that every neighborhood of \(x\) contains a test function on which \(F\) does not vanish.

A distribution on \(X\) is a \(\mathbb {C}\)-linear functional on \(C_c^{\infty }(X)\).

Given a locally constant function on a subset \(Z \subseteq X\), we extend it to \(X\) by zero outside \(Z\).

Let \(G\) be a topological group. We say that \(G\) has a compact open subgroup basis if \(\mathcal N(1)\) has a basis consisting of compact open subgroups.

The Hecke algebra \(\mathcal{H}(G)\) is the space of compactly supported, locally constant distributions on \(G\), equipped with convolution.

Define idempotented algebra.

The indicator function of a compact clopen subset is a compactly supported locally constant function.

We say a distribution is left, right, or bi-invariant under an open subgroup if it is fixed by the corresponding translation action.

Let \(D\) be a compactly supported distribution on \(G\). The following statements are equivalent:

1. \(D\) is left-invariant under some compact open subgroup of \(G\);

2. \(D\) is right-invariant under some compact open subgroup of \(G\);

3. \(D\) is bi-invariant under some compact open group of \(G\).

A compactly supported distribution satisfying the above condition is said to be locally constant.

We write \(C^{\infty }(X)\) for the space of complex-valued locally constant functions on \(X\).

Define non-degenerated (also called unital) modules over an idempotented algebra.

We define a compactly supported distribution \(e_H\) attached to a compact open subgroup \(H\) as the average of a test function over \(H\) with respect to the normalized Haar measure on \(H\).

For \(\varphi : G \to \mathbb {C}\) and \(g \in G\) we define

If the support of a test function is disjoint from the support of \(F\), then \(F\) evaluates to zero on that function.

Let \(G\) be a td group (totally disconnected, locally compact, Hausdorff). Any closed subgroup of \(G\) is also a td group.

The action map of a continuous representation is continuous by construction.

Two continuous representations are identical exactly when their underlying algebraic representations are identical.

(In dependent type theory/kean) All definitional projections and coercions agree with the data used to build the representation.

For a continuous representation \(\rho \):

1. for fixed \(g\), the map \(v \mapsto \rho (g)v\) is continuous;

2. for fixed \(v\), the map \(g \mapsto \rho (g)v\) is continuous;

3. for fixed \(g\) and \(u\), the affine map \(v \mapsto \rho (g)v + u\) is continuous.

Convolution of compactly supported distributions is associative.

The action map \(G \times V \to V\) is jointly continuous.

Joint continuity of the action implies continuity of each slice \(v \mapsto \rho (g)v\).

For \(g \in G\) and test function \(\varphi \):

If \(g \in H\), then \(\delta _g * e_H = e_H * \delta _g\).

Distributions are additive and \(\mathbb {C}\)-linear.

Let \(G\) be a td group. Then every neighborhood of \(1\) contains a compact clopen neighborhood of \(1\).

Let \(G\) be a td group. Every neighborhood of \(1\) contains a compact open subgroup of \(G\).

Let \(G\) be a td group. Inside a compact clopen neighborhood of \(1\), there exists a compact open subgroup.

Let \(G\) be a topological group. If \(K\) is compact and open subset of \(G\), then there exists \(V \in \mathcal N(1)\) such that \(K \cdot V \subseteq K\).

In Lemma 6, \(V\) can be chosen symmetric.

If \(Z\) is closed and compact, the extension by zero has compact support.

If \(Z\) is clopen, the extension by zero is locally constant.

For any \(n \in \mathbb {N}\), the group \(\mathrm{GL}_n(K)\) is a totally disconnected, locally compact, Hausdorff topological group.

Addition, negation, and scalar multiplication agree with the underlying distribution operations.

(In dependent type theory/lean) The Hecke algebra is a subtype of compactly supported distributions with the expected coercions and extensionality.

Convolution makes \(\mathcal{H}(G)\) into a non-unital ring; associativity is inherited from convolution of distributions.

If a topological group \(G\) has a compact open subgroup basis, then \(G\) is locally compact.

For any \(n \in \mathbb {N}\), the space \(M_n(K)\) is totally disconnected, locally compact, and Hausdorff.

The local field \(K\) is T2, locally compact, and totally disconnected.

Let \(G\) be a topological group. Then a neighborhood basis at unit \(1\) transports to a neighborhood basis at any \(x\in G\) by left translation.

Let \(G\) be a topological group. If \(G\) has a compact open subgroup basis, then \(G\) is a nonarchimedean group.

For a compact open subgroup \(H\), the normalized Haar distribution is idempotent:

For a compact open subgroup \(H\), \(e_H\) is left \(H\)-invariant, right \(H\)-invariant, and hence bi-\(H\)-invariant.

The support of a distribution is a closed subspace of \(X\).

A locally compact, Hausdorff, nonarchimedean group is totally disconnected.

If a topological group \(G\) has a compact open subgroup basis, then \(G\) is totally disconnected.

Right and left translations preserve local constancy and compact support.

If \(F\) is compactly supported and bi-\(H\)-invariant, then there exist finitely many elements \(g_i \in G\) and coefficients \(a_i \in \mathbb {C}\) such that

for all test functions \(\varphi \).

The category of non-degenerated modules over the Hecke algebra of \(G\) is equivalent to the category of smooth \(\mathbb {C}\)-representations of \(G\).

The group \(\mathrm{GL}_n(K)\) has a compact open subgroup basis.

Hecke algebra is an idempotented algebra.

Assuming \(G\) is Hausdorff, having a compact open subgroup basis is equivalent to being locally compact and totally disconnected.

If \(G\) is td group (i.e.totally disconnected, locally compact, and Hausdorff topological group), then \(G\) has a compact open subgroup basis.

Assuming \(G\) is Hausdorff, having a compact open subgroup basis is equivalent to being locally compact and nonarchimedean.