mathlib3 documentation

representation_theory.basic

Monoid representations #

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

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

@[reducible]
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} {V : Type u_3} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] :

The trivial representation of G on a k-module V.

Equations
@[simp]
theorem representation.trivial_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] (g : G) (v : V) :
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) (r : k) :
theorem representation.as_algebra_hom_single_one {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) :
@[nolint]
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) :
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]
@[protected, instance]
def representation.as_module.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) :
@[protected, instance]
def representation.as_module.inhabited {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) :
Equations
@[protected, instance]
noncomputable def representation.as_module_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_module_equiv {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) :

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} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] (ρ : representation k G V) (r : monoid_algebra k 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} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] (ρ : representation k G 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} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] (ρ : representation k G V) (g : G) (x : V) :
noncomputable def representation.of_module' {k : Type u_1} {G : Type u_2} [comm_semiring k] [monoid G] (M : Type u_3) [add_comm_monoid M] [module k M] [module (monoid_algebra k G) M] [is_scalar_tower k (monoid_algebra k G) 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) [comm_semiring k] [monoid G] (M : Type u_4) [add_comm_monoid M] [module (monoid_algebra k 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).

@[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] [module k V] (ρ : representation k G V) :
Equations
noncomputable def representation.of_mul_action (k : Type u_1) [comm_semiring k] (G : Type u_2) [monoid G] (H : Type u_3) [mul_action G H] :

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

Equations
theorem representation.of_mul_action_single {k : Type u_1} [comm_semiring k] {G : Type u_2} [monoid G] {H : Type u_3} [mul_action G H] (g : G) (x : H) (r : k) :
@[simp]
theorem representation.of_mul_action_apply {k : Type u_1} {G : Type u_2} [comm_semiring k] [group G] {H : Type u_3} [mul_action G H] (g : G) (f : H →₀ k) (h : H) :

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
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)
theorem representation.smul_tprod_one_as_module {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) (r : monoid_algebra k 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} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V] [add_comm_monoid W] [module k W] (ρW : representation k G W) (r : monoid_algebra k 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} [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)

Given $k$-modules $V, W$, there is a homomorphism $φ : V^* ⊗ W → Hom_k(V, W)$ (implemented by linear_algebra.contraction.dual_tensor_hom). Given representations of $G$ on $V$ and $W$,there are representations of $G$ on $V^* ⊗ W$ and on $Hom_k(V, W)$. This lemma says that $φ$ is $G$-linear.