# mathlibdocumentation

representation_theory.basic

# Monoid representations #

This file introduces monoid representations and their characters and defines a few ways to construct representations.

## Main definitions #

• representation.representation
• representation.character
• representation.tprod
• representation.lin_hom
• represensation.dual

## Implementation notes #

Representations of a monoid G on a k-module V are implemented as homomorphisms G →* (V →ₗ[k] V).

def representation (k : Type u_1) (G : Type u_2) (V : Type u_3) [monoid G] [ V] :
Type (max u_3 u_2)

A representation of G on the k-module V is an homomorphism G →* (V →ₗ[k] V).

def representation.trivial {k : Type u_1} {G : Type u_2} [monoid G] :
k

The trivial representation of G on the one-dimensional module k.

Equations
@[simp]
theorem representation.trivial_def {k : Type u_1} {G : Type u_2} [monoid G] (g : G) (v : k) :
= v
noncomputable def representation.as_algebra_hom {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) :

A k-linear representation of G on V can be thought of as an algebra map from monoid_algebra k G into the k-linear endomorphisms of V.

Equations
theorem representation.as_algebra_hom_def {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) :
@[simp]
theorem representation.as_algebra_hom_single {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) (g : G) :
(ρ.as_algebra_hom) 1) = ρ g
theorem representation.as_algebra_hom_of {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) (g : G) :
(ρ.as_algebra_hom) ( G) g) = ρ g
noncomputable def representation.as_module {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) :
module G) V

A k-linear representation of G on V can be thought of as a module over monoid_algebra k G.

Equations
def representation.as_group_hom {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρ : V) :
G →* (V →ₗ[k] V)ˣ

When G is a group, a k-linear representation of G on V can be thought of as a group homomorphism from G into the invertible k-linear endomorphisms of V.

Equations
theorem representation.as_group_hom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρ : V) (g : G) :
((ρ.as_group_hom) g) = ρ g
def representation.tprod {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [monoid G] [ V] [ W] (ρV : V) (ρW : W) :
V W)

Given representations of G on V and W, there is a natural representation of G on their tensor product V ⊗[k] W.

Equations
@[simp]
theorem representation.tprod_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [monoid G] [ V] [ W] (ρV : V) (ρW : W) (g : G) :
(ρV.tprod ρW) g = tensor_product.map (ρV g) (ρW g)
def representation.lin_hom {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [group G] [ V] [ W] (ρV : V) (ρW : W) :
(V →ₗ[k] W)

Given representations of G on V and W, there is a natural representation of G on the module V →ₗ[k] W, where G acts by conjugation.

Equations
@[simp]
theorem representation.lin_hom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [group G] [ V] [ W] (ρV : V) (ρW : W) (g : G) (f : V →ₗ[k] W) :
((ρV.lin_hom ρW) g) f = (ρW g).comp (f.comp (ρV g⁻¹))
def representation.dual {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρV : V) :
V)

The dual of a representation ρ of G on a module V, given by (dual ρ) g f = f ∘ₗ (ρ g⁻¹), where f : module.dual k V.

Equations
@[simp]
theorem representation.dual_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [group G] [ V] (ρV : V) (g : G) :
(ρV.dual) g =
theorem representation.dual_tensor_hom_comm {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [group G] [ V] [ W] (ρV : V) (ρW : W) (g : G) :
V W).comp (tensor_product.map ((ρV.dual) g) (ρW g)) = ((ρV.lin_hom ρW) g).comp V W)