# 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).

@[reducible]
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) (r : k) :
(ρ.as_algebra_hom) r) = r ρ g
theorem representation.as_algebra_hom_single_one {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
@[nolint]
def representation.as_module {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) :
Type u_3

If ρ : representation k G V, then ρ.as_module is a type synonym for V, which we equip with an instance module (monoid_algebra k G) ρ.as_module.

You should use as_module_equiv : ρ.as_module ≃+ V to translate terms.

Equations
Instances for representation.as_module
@[protected, instance]
def representation.as_module.add_comm_monoid {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) :
@[protected, instance]
def representation.as_module.module {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) :
@[protected, instance]
def representation.as_module.inhabited {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) :
Equations
@[protected, instance]
noncomputable def representation.as_module_module {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 a module over monoid_algebra k G.

Equations
def representation.as_module_equiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) :

The additive equivalence from the module (monoid_algebra k G) to the original vector space of the representative.

This is just the identity, but it is helpful for typechecking and keeping track of instances.

Equations
@[simp]
theorem representation.as_module_equiv_map_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) (r : G) (x : ρ.as_module) :
@[simp]
theorem representation.as_module_equiv_symm_map_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) (r : k) (x : V) :
@[simp]
theorem representation.as_module_equiv_symm_map_rho {k : Type u_1} {G : Type u_2} {V : Type u_3} [monoid G] [ V] (ρ : V) (g : G) (x : V) :
noncomputable def representation.of_module' {k : Type u_1} {G : Type u_2} [monoid G] (M : Type u_3) [ M] [module G) M] [ G) M] :
M

Build a representation k G M from a [module (monoid_algebra k G) M].

This version is not always what we want, as it relies on an existing [module k M] instance, along with a [is_scalar_tower k (monoid_algebra k G) M] instance.

We remedy this below in of_module (with the tradeoff that the representation is defined only on a type synonym of the original module.)

Equations
noncomputable def representation.of_module (k : Type u_1) (G : Type u_2) [monoid G] (M : Type u_4) [module G) M] :
G) M)

Build a representation from a [module (monoid_algebra k G) M].

Note that the representation is built on restrict_scalars k (monoid_algebra k G) M, rather than on M itself.

Equations

## of_module and as_module are inverses. #

This requires a little care in both directions: this is a categorical equivalence, not an isomorphism.

See Rep.equivalence_Module_monoid_algebra for the full statement.

Starting with ρ : representation k G V, converting to a module and back again we have a representation k G (restrict_scalars k (monoid_algebra k G) ρ.as_module). To compare these, we use the composition of restrict_scalars_add_equiv and ρ.as_module_equiv.

Similarly, starting with module (monoid_algebra k G) M, after we convert to a representation and back to a module, we have module (monoid_algebra k G) (restrict_scalars k (monoid_algebra k G) M).

@[simp]
theorem representation.of_module_as_algebra_hom_apply_apply (k : Type u_1) (G : Type u_2) [monoid G] (M : Type u_4) [module G) M] (r : G) (m : G) M) :
( M).as_algebra_hom) r) m = G) M).symm) (r M) m)
@[simp]
theorem representation.of_module_as_module_act (k : Type u_1) (G : Type u_2) {V : Type u_3} [monoid G] [ V] (ρ : V) (g : G) (x : G) ρ.as_module) :
( g) x = G) ρ.as_module).symm) ((ρ.as_module_equiv.symm) ((ρ g) ((ρ.as_module_equiv) ( ρ.as_module) x))))
theorem representation.smul_of_module_as_module (k : Type u_1) (G : Type u_2) [monoid G] (M : Type u_4) [module G) M] (r : G) (m : M).as_module) :
M) ( M).as_module_equiv) (r m)) = r M) ( M).as_module_equiv) m)
@[protected, instance]
def representation.as_module.add_comm_group {k : Type u_1} {G : Type u_2} {V : Type u_3} [comm_ring k] [monoid G] [I : add_comm_group V] [ V] (ρ : V) :
Equations
noncomputable def representation.of_mul_action (k : Type u_1) (G : Type u_2) [monoid G] (H : Type u_3) [ H] :
(H →₀ k)

A G-action on H induces a representation G →* End(k[H]) in the natural way.

Equations
theorem representation.of_mul_action_def {k : Type u_1} {G : Type u_2} [monoid G] {H : Type u_3} [ H] (g : G) :
H) g =
@[simp]
theorem representation.of_mul_action_apply {k : Type u_1} {G : Type u_2} [group G] {H : Type u_3} [ H] (g : G) (f : H →₀ k) (h : H) :
(( H) g) f) h = f (g⁻¹ h)
theorem representation.of_mul_action_self_smul_eq_mul {k : Type u_1} {G : Type u_2} [group G] (x : G) (y : G).as_module) :
x y = x * y
@[simp]
theorem representation.of_mul_action_self_as_module_equiv_apply {k : Type u_1} {G : Type u_2} [group G] (ᾰ : G).as_module) :
noncomputable def representation.of_mul_action_self_as_module_equiv {k : Type u_1} {G : Type u_2} [group G] :

If we equip k[G] with the k-linear G-representation induced by the left regular action of G on itself, the resulting object is isomorphic as a k[G]-module to k[G] with its natural k[G]-module structure.

Equations
@[simp]
theorem representation.of_mul_action_self_as_module_equiv_symm_apply {k : Type u_1} {G : Type u_2} [group G] (ᾰ : G →₀ k) :
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)
theorem representation.smul_tprod_one_as_module {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [monoid G] [ V] [ W] (ρV : V) (r : G) (x : V) (y : W) :
r x ⊗ₜ[k] y = (r x) ⊗ₜ[k] y
theorem representation.smul_one_tprod_as_module {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [monoid G] [ V] [ W] (ρW : W) (r : G) (x : V) (y : W) :
r x ⊗ₜ[k] y = x ⊗ₜ[k] (r y)
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)