# mathlib3documentation

representation_theory.fdRep

# fdRep k G is the category of finite dimensional k-linear representations of G. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

fdRep k G has all finite limits.

## TODO #

• fdRep k G ≌ full_subcategory (finite_dimensional k)
• Upgrade the right rigid structure to a rigid structure (this just needs to be done for fgModule).
• fdRep k G has all finite colimits.
• fdRep k G is abelian.
• fdRep k G ≌ fgModule (monoid_algebra k G).
@[protected, instance]
def fdRep.preadditive (k G : Type u) [field k] [monoid G] :
@[protected, instance]
def fdRep.concrete_category (k G : Type u) [field k] [monoid G] :
@[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]
def fdRep.has_finite_limits (k G : Type u) [field k] [monoid G] :
@[protected, instance]
def fdRep.large_category (k G : Type u) [field k] [monoid G] :
@[protected, instance]
def fdRep.category_theory.linear {k G : Type u} [field k] [monoid G] :
(fdRep k G)
Equations
@[protected, instance]
def fdRep.has_coe_to_sort {k G : Type u} [field k] [monoid G] :
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) :
@[protected, instance]
def fdRep.quiver.hom.finite_dimensional {k G : Type u} [field k] [monoid G] (V W : G) :
(V W)

All hom spaces are finite dimensional.

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, ρ := ρ}
theorem fdRep.forget₂_ρ {k G : Type u} [field k] [monoid G] (V : G) :
@[protected, instance]
theorem fdRep.finrank_hom_simple_simple {k G : Type u} [field k] [monoid G] (V W : G)  :
(V W) = ite (nonempty (V W)) 1 0
def fdRep.forget₂_hom_linear_equiv {k G : Type u} [field k] [monoid G] (X Y : G) :

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

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 : Type u} [field k] [group G] [ V] [ V] (ρV : V) (W : G) :
(fdRep.of ρV.dual 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 : Type u} [field k] [group G] [ V] [ V] (ρV : V) (W : G) :

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 : Type u} [field k] [group G] [ V] [ V] (ρV : V) (W : G) :