Rep k G
is the category of k
-linear representations of G
. #
If V : Rep k G
, there is a coercion that allows you to treat V
as a type,
and this type comes equipped with a module k V
instance.
Also V.ρ
gives the homomorphism G →* (V →ₗ[k] V)
.
Conversely, given a homomorphism ρ : G →* (V →ₗ[k] V)
,
you can construct the bundled representation as Rep.of ρ
.
We verify that Rep k G
is a k
-linear abelian symmetric monoidal category with all (co)limits.
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable
def
Rep.abelian
(k G : Type u)
[ring k]
[monoid G] :
category_theory.abelian (Rep k G)
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
Rep.category_theory.linear
(k G : Type u)
[comm_ring k]
[monoid G] :
category_theory.linear k (Rep k G)
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- V.add_comm_monoid = id (add_comm_group.to_add_comm_monoid ↥((category_theory.forget₂ (Rep k G) (Module k)).obj V))