mathlib documentation

representation_theory.fdRep

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]
@[reducible]
def fdRep (k G : Type u) [field k] [monoid G] :
Type (u+1)

The category of finite dimensional k-linear representations of a monoid G.

@[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]
def fdRep.add_comm_group {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
Equations
@[protected, instance]
def fdRep.module {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
Equations
@[protected, instance]
def fdRep.finite_dimensional {k G : Type u} [field k] [monoid G] (V : fdRep k G) :
def fdRep.ρ {k G : Type u} [field k] [monoid G] (V : fdRep k G) :

The monoid homomorphism corresponding to the action of G onto V : fdRep k G.

Equations
def fdRep.iso_to_linear_equiv {k G : Type u} [field k] [monoid G] {V W : fdRep k G} (i : V W) :

The underlying linear_equiv of an isomorphism of representations.

Equations
theorem fdRep.iso.conj_ρ {k G : Type u} [field k] [monoid G] {V W : fdRep k G} (i : V W) (g : G) :
@[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) :
(fdRep.of ρ).ρ = ρ
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.

Equations
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) :
(fdRep.of ρV.dual fdRep.of ρW).V (fdRep.of (ρV.lin_hom ρW)).V

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
@[simp]