mathlib documentation

representation_theory.basic

Monoid representations #

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

Main definitions #

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) [comm_semiring k] [monoid G] [add_comm_monoid V] [module k 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} [comm_semiring k] [monoid G] :

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} [comm_semiring k] [monoid G] (g : G) (v : k) :
noncomputable def representation.as_algebra_hom {k : Type u_1} {G : Type u_2} {V : Type u_3} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] (ρ : representation k G 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} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] (ρ : representation k G V) :
@[simp]
theorem representation.as_algebra_hom_single {k : Type u_1} {G : Type u_2} {V : Type u_3} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] (ρ : representation k G V) (g : G) :
theorem representation.as_algebra_hom_of {k : Type u_1} {G : Type u_2} {V : Type u_3} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] (ρ : representation k G V) (g : G) :
noncomputable def representation.as_module {k : Type u_1} {G : Type u_2} {V : Type u_3} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] (ρ : representation k 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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρ : representation k G 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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρ : representation k G 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} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] [add_comm_monoid W] [module k W] (ρV : representation k G V) (ρW : representation k G 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} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] [add_comm_monoid W] [module k W] (ρV : representation k G V) (ρW : representation k G 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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] [add_comm_monoid W] [module k W] (ρV : representation k G V) (ρW : representation k G 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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] [add_comm_monoid W] [module k W] (ρV : representation k G V) (ρW : representation k G 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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρV : representation k G 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} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] (ρV : representation k G V) (g : G) :
theorem representation.dual_tensor_hom_comm {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [comm_semiring k] [group G] [add_comm_monoid V] [module k V] [add_comm_monoid W] [module k W] (ρV : representation k G V) (ρW : representation k G W) (g : G) :
(dual_tensor_hom k V W).comp (tensor_product.map ((ρV.dual) g) (ρW g)) = ((ρV.lin_hom ρW) g).comp (dual_tensor_hom k V W)