V : FdRep k G, there is a coercion that allows you to treat
V as a type,
and this type comes equipped with
Module k V and
FiniteDimensional k V instances.
V.ρ gives the homomorphism
G →* (V →ₗ[k] V).
We verify that
FdRep k G is a
k-linear monoidal category, and rigid when
G is a group.
FdRep k G has all finite limits.
All hom spaces are finite dimensional.
The forgetful functor to
Rep k G preserves hom-sets and their vector space structure.
Auxiliary definition for
W are finite dimensional representations of a group
G, the isomorphism
dualTensorHomEquiv k V W of vector spaces induces an isomorphism of representations.