Transports between equal topological representations #
This file supplements Mathlib's category TopRep k G of continuous representations with the
action of the transports eqToHom h along equalities h : X = Y of objects: on underlying
vectors they are casts of the carriers.
Main results #
TopRep.eqToHom_hom_apply: a transport between equal objects casts the carrier.
@[simp]
theorem
TopRep.eqToHom_hom_apply
{k : Type u_1}
{G : Type u_2}
[Ring k]
[TopologicalSpace k]
[Monoid G]
{X Y : TopRep k G}
(h : X = Y)
(x : ↑X)
:
For an equality h : X = Y of topological representations, the transport eqToHom h sends
x : X to its cast along the induced equality X.V = Y.V of carriers.