Evaluation of the algebraic representation underlying a continuous representation

Forgetting continuity leaves the action on each vector unchanged.

Main results

• ContRepresentation.toRepresentation_apply: evaluation agrees with the continuous action.

References

• Mathlib.RepresentationTheory.Continuous.Basic, for ContRepresentation.toRepresentation.

@[simp]

theorem ContRepresentation.toRepresentation_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Monoid G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (g : G) (v : V) : ((toRepresentation R G V π) g) v = (π g) v

Forgetting continuity of an action preserves its evaluation on vectors.