fdRep k G
is the category of finite dimensional k
-linear representations of G
. #
If 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 finite_dimensional k V
instances.
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 fdRep k G
is a rigid monoidal category.
TODO #
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
fdRep.has_coe_to_sort
{k G : Type u}
[field k]
[monoid G] :
has_coe_to_sort (fdRep k G) (Type u)
Equations
@[protected, instance]
Equations
- V.add_comm_group = id ((category_theory.forget₂ (fdRep k G) (FinVect k)).obj V).obj.is_add_comm_group
@[protected, instance]
The underlying linear_equiv
of an isomorphism of representations.
Equations
- fdRep.iso_to_linear_equiv i = FinVect.iso_to_linear_equiv ((Action.forget (FinVect k) (Mon.of G)).map_iso i)
@[simp]
theorem
fdRep.of_ρ
{k G : Type u}
[field k]
[monoid G]
{V : Type u}
[add_comm_group V]
[module k V]
[finite_dimensional k V]
(ρ : representation k G V) :
def
fdRep.of
{k G : Type u}
[field k]
[monoid G]
{V : Type u}
[add_comm_group V]
[module k V]
[finite_dimensional k V]
(ρ : representation k G V) :
fdRep k G
Lift an unbundled representation to fdRep
.
@[protected, instance]
def
fdRep.Rep.category_theory.has_forget₂
{k G : Type u}
[field k]
[monoid G] :
category_theory.has_forget₂ (fdRep k G) (Rep k G)
Equations
- fdRep.Rep.category_theory.has_forget₂ = {forget₂ := (category_theory.forget₂ (FinVect k) (Module k)).map_Action (Mon.of G), forget_comp := _}
@[protected, instance]
noncomputable
def
fdRep.dual_tensor_iso_lin_hom_aux
{k G V W : Type u}
[field k]
[group G]
[add_comm_group V]
[module k V]
[add_comm_group W]
[module k W]
[finite_dimensional k V]
[finite_dimensional k W]
(ρV : representation k G V)
(ρW : representation k G W) :
Auxiliary definition for fdRep.dual_tensor_iso_lin_hom
.
Equations
noncomputable
def
fdRep.dual_tensor_iso_lin_hom
{k G V W : Type u}
[field k]
[group G]
[add_comm_group V]
[module k V]
[add_comm_group W]
[module k W]
[finite_dimensional k V]
[finite_dimensional k W]
(ρV : representation k G V)
(ρW : representation k G W) :
When V
and W
are finite dimensional representations of a group G
, the isomorphism
dual_tensor_hom_equiv k V W
of vector spaces induces an isomorphism of representations.
Equations
- fdRep.dual_tensor_iso_lin_hom ρV ρW = Action.mk_iso (fdRep.dual_tensor_iso_lin_hom_aux ρV ρW) _
@[simp]
theorem
fdRep.dual_tensor_iso_lin_hom_hom_hom
{k G V W : Type u}
[field k]
[group G]
[add_comm_group V]
[module k V]
[add_comm_group W]
[module k W]
[finite_dimensional k V]
[finite_dimensional k W]
(ρV : representation k G V)
(ρW : representation k G W) :
(fdRep.dual_tensor_iso_lin_hom ρV ρW).hom.hom = dual_tensor_hom k V W