2.2 The category of continuous representations
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)\).
We defined \(\mathrm{CRep}_R(G)\) using a more abstract way, i.e. group actions on the category \(\mathrm{TopModuleCat}(R)\) for Lean implementation considerations.
Therefore, we need to show that this abstract definition coincide with the natural one, i.e. the category of continuous representations of \(G\).
There is a forgetful functor to \(\mathrm{TopModuleCat}(R)\) and an induced map on morphisms.
For \(V \in \mathrm{CRep}_R(G)\) we extract the underlying action and define the evaluation map \(\mathrm{act}(g,v)\).
The action map \(G \times V \to V\) is jointly continuous.
There is a forgetful functor \(\mathrm{CRep}_R(G) \to \mathrm{Rep}_R(G)\).
Every object in \(\mathrm{CRep}_R(G)\) yields a continuous representation on its underlying type.
Joint continuity of the action implies continuity of each slice \(v \mapsto \rho (g)v\).
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)\).
A representation with a jointly continuous action determines a continuous action object in \(\mathrm{TopModuleCat}(R)\).
A representation with a compatible topology and continuous action determines an object of \(\mathrm{CRep}_R(G)\).
A continuous representation (as defined above) can be lifted to an object of \(\mathrm{CRep}_R(G)\).