# mathlibdocumentation

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 #

• fdRep k G has all finite (co)limits.
• fdRep k G is abelian.
• fdRep k G ≌ FinVect (monoid_algebra k G) (this will require generalising FinVect first).
• Upgrade the right rigid structure to a rigid structure.
@[protected, instance]
def fdRep.concrete_category (k G : Type u) [field k] [monoid G] :
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]
def fdRep.large_category (k G : Type u) [field k] [monoid G] :
@[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 : G) :
Equations
@[protected, instance]
def fdRep.module {k G : Type u} [field k] [monoid G] (V : G) :
V
Equations
@[protected, instance]
def fdRep.finite_dimensional {k G : Type u} [field k] [monoid G] (V : G) :
def fdRep.ρ {k G : Type u} [field k] [monoid G] (V : 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 : 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 : G} (i : V W) (g : G) :
(W.ρ) g = ((V.ρ) g)
@[simp]
theorem fdRep.of_ρ {k G : Type u} [field k] [monoid G] {V : Type u} [ V] [ V] (ρ : V) :
(fdRep.of ρ).ρ = ρ
def fdRep.of {k G : Type u} [field k] [monoid G] {V : Type u} [ V] [ V] (ρ : V) :
G

Lift an unbundled representation to fdRep.

Equations
• = {V := V _inst_5, ρ := ρ}
@[protected, instance]
def fdRep.Rep.category_theory.has_forget₂ {k G : Type u} [field k] [monoid G] :
(Rep k G)
Equations
@[protected, instance]
noncomputable def fdRep.category_theory.right_rigid_category {k G : Type u} [field k] [group G] :
Equations
noncomputable def fdRep.dual_tensor_iso_lin_hom_aux {k G V W : Type u} [field k] [group G] [ V] [ W] [ V] [ W] (ρV : V) (ρW : 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] [ V] [ W] [ V] [ W] (ρV : V) (ρW : 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]
theorem fdRep.dual_tensor_iso_lin_hom_hom_hom {k G V W : Type u} [field k] [group G] [ V] [ W] [ V] [ W] (ρV : V) (ρW : W) :
.hom.hom = W