# Documentation

Mathlib.RepresentationTheory.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 FiniteDimensional 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 k-linear monoidal category, and rigid when G is a group.

FdRep k G has all finite limits.

## TODO #

• FdRep k G ≌ FullSubcategory (FiniteDimensional k)
• Upgrade the right rigid structure to a rigid structure (this just needs to be done for FGModuleCat).
• FdRep k G has all finite colimits.
• FdRep k G is abelian.
• FdRep k G ≌ FGModuleCat (MonoidAlgebra k G).
@[inline, reducible]
abbrev FdRep (k : Type u) (G : Type u) [] [] :
Type (u + 1)

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

Instances For
instance FdRep.instLargeCategoryFdRep {k : Type u} {G : Type u} [] [] :
instance FdRep.instCoeSortFdRepType {k : Type u} {G : Type u} [] [] :
CoeSort (FdRep k G) (Type u)

All hom spaces are finite dimensional.

def FdRep.ρ {k : Type u} {G : Type u} [] [] (V : FdRep k G) :
G →*

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

Instances For
def FdRep.isoToLinearEquiv {k : Type u} {G : Type u} [] [] {V : FdRep k G} {W : FdRep k G} (i : V W) :

The underlying LinearEquiv of an isomorphism of representations.

Instances For
theorem FdRep.Iso.conj_ρ {k : Type u} {G : Type u} [] [] {V : FdRep k G} {W : FdRep k G} (i : V W) (g : G) :
↑() g = ↑() (↑() g)
@[simp]
theorem FdRep.of_ρ {k : Type u} {G : Type u} [] [] {V : Type u} [] [Module k V] [] (ρ : ) :
().ρ = ρ
def FdRep.of {k : Type u} {G : Type u} [] [] {V : Type u} [] [Module k V] [] (ρ : ) :
FdRep k G

Lift an unbundled representation to FdRep.

Instances For
theorem FdRep.forget₂_ρ {k : Type u} {G : Type u} [] [] (V : FdRep k G) :
Rep.ρ ((CategoryTheory.forget₂ (FdRep k G) (Rep k G)).obj V) =
theorem FdRep.finrank_hom_simple_simple {k : Type u} {G : Type u} [] [] [] (V : FdRep k G) (W : FdRep k G) :
FiniteDimensional.finrank k (V W) = if Nonempty (V W) then 1 else 0
def FdRep.forget₂HomLinearEquiv {k : Type u} {G : Type u} [] [] (X : FdRep k G) (Y : FdRep k G) :
((CategoryTheory.forget₂ (FdRep k G) (Rep k G)).obj X (CategoryTheory.forget₂ (FdRep k G) (Rep k G)).obj Y) ≃ₗ[k] X Y

The forgetful functor to Rep k G preserves hom-sets and their vector space structure.

Instances For
noncomputable def FdRep.dualTensorIsoLinHomAux {k : Type u} {G : Type u} {V : Type u} [] [] [] [Module k V] [] (ρV : ) (W : FdRep k G) :
(FdRep.of ()).V

Auxiliary definition for FdRep.dualTensorIsoLinHom.

Instances For
noncomputable def FdRep.dualTensorIsoLinHom {k : Type u} {G : Type u} {V : Type u} [] [] [] [Module k V] [] (ρV : ) (W : FdRep k G) :

When V and W are finite dimensional representations of a group G, the isomorphism dualTensorHomEquiv k V W of vector spaces induces an isomorphism of representations.

Instances For
@[simp]
theorem FdRep.dualTensorIsoLinHom_hom_hom {k : Type u} {G : Type u} {V : Type u} [] [] [] [Module k V] [] (ρV : ) (W : FdRep k G) :
().hom.hom = dualTensorHom k V ()