2.1 Continuous representations
Let \(R\) be a commutative topological ring, \(G\) a group equipped with a topology, and \(V\) a topological \(R\)-module with continuous addition and scalar multiplication.
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.)
Given a representation \(\rho \) and a proof of continuity of the action map, we obtain a continuous representation.
(In dependent type theory/kean) All definitional projections and coercions agree with the data used to build the representation.
We have the action map \(G \times V \to V\) associated to a continuous representation.
The action map of a continuous representation is continuous by construction.
The underlying topological \(R\)-module is bundled as an object of \(\mathrm{TopModuleCat}(R)\).
If \(M\) is an object of \(\mathrm{TopModuleCat}(R)\) equipped with a continuous action by \(R\)-linear maps, this yields a continuous representation.
For a continuous representation \(\rho \):
for fixed \(g\), the map \(v \mapsto \rho (g)v\) is continuous;
for fixed \(v\), the map \(g \mapsto \rho (g)v\) is continuous;
for fixed \(g\) and \(u\), the affine map \(v \mapsto \rho (g)v + u\) is continuous.
Two continuous representations are identical exactly when their underlying algebraic representations are identical.
The trivial representation is a continuous representation.
A continuous representation restricts to any subgroup \(H \le G\).
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\).