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

source
@[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).

source
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] :
representation k G V

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

Equations
source
@[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) :
⇑(⇑(representation.trivial k) g) v = v
source
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) :
monoid_algebra k G →ₐ[k] module.End k 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
source
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) :
ρ.as_algebra_hom = ⇑(monoid_algebra.lift k G (V →ₗ[k] V)) ρ
source
@[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) :
⇑(ρ.as_algebra_hom) (finsupp.single g r) = r • ⇑ρ g
source
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) :
⇑(ρ.as_algebra_hom) (finsupp.single g 1) = ⇑ρ g
source
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) :
⇑(ρ.as_algebra_hom) (⇑(monoid_algebra.of k G) g) = ⇑ρ g
source
@[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
source
@[protected, instance]
def representation.as_module.add_comm_monoid {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) :
add_comm_monoid ρ.as_module
source
@[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) :
module (module.End k V) ρ.as_module
source
@[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) :
inhabited ρ.as_module
Equations
source
@[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) :
module (monoid_algebra k G) ρ.as_module

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

Equations
source
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) :
ρ.as_module ≃+ 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
source
@[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) :
⇑(ρ.as_module_equiv) (r • x) = ⇑(⇑(ρ.as_algebra_hom) r) (⇑(ρ.as_module_equiv) x)
source
@[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) :
⇑(ρ.as_module_equiv.symm) (r • x) = ⇑(algebra_map k (monoid_algebra k G)) r • ⇑(ρ.as_module_equiv.symm) x
source
@[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) :
⇑(ρ.as_module_equiv.symm) (⇑(⇑ρ g) x) = ⇑(monoid_algebra.of k G) g • ⇑(ρ.as_module_equiv.symm) x
source
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] :
representation 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
source
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] :
representation k G (restrict_scalars k (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).

source
@[simp]
theorem representation.of_module_as_algebra_hom_apply_apply (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] (r : monoid_algebra k G) (m : restrict_scalars k (monoid_algebra k G) M) :
⇑(⇑((representation.of_module k G M).as_algebra_hom) r) m = ⇑((restrict_scalars.add_equiv k (monoid_algebra k G) M).symm) (r • ⇑(restrict_scalars.add_equiv k (monoid_algebra k G) M) m)
source
@[simp]
theorem representation.of_module_as_module_act (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 : restrict_scalars k (monoid_algebra k G) ρ.as_module) :
⇑(⇑(representation.of_module k G ρ.as_module) g) x = ⇑((restrict_scalars.add_equiv k (monoid_algebra k G) ρ.as_module).symm) (⇑(ρ.as_module_equiv.symm) (⇑(⇑ρ g) (⇑(ρ.as_module_equiv) (⇑(restrict_scalars.add_equiv k (monoid_algebra k G) ρ.as_module) x))))
source
theorem representation.smul_of_module_as_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] (r : monoid_algebra k G) (m : (representation.of_module k G M).as_module) :
⇑(restrict_scalars.add_equiv k (monoid_algebra k G) M) (⇑((representation.of_module k G M).as_module_equiv) (r • m)) = r • ⇑(restrict_scalars.add_equiv k (monoid_algebra k G) M) (⇑((representation.of_module k G M).as_module_equiv) m)
source
@[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) :
add_comm_group ρ.as_module
Equations
source
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] :
representation k G (H →₀ k)

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

Equations
source
theorem representation.of_mul_action_def {k : Type u_1} [comm_semiring k] {G : Type u_2} [monoid G] {H : Type u_3} [mul_action G H] (g : G) :
⇑(representation.of_mul_action k G H) g = finsupp.lmap_domain k k (has_smul.smul g)
source
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) :
⇑(⇑(representation.of_mul_action k G H) g) (finsupp.single x r) = finsupp.single (g • x) r
source
@[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) :
⇑(⇑(⇑(representation.of_mul_action k G H) g) f) h = ⇑f (g⁻¹ • h)
source
theorem representation.of_mul_action_self_smul_eq_mul {k : Type u_1} {G : Type u_2} [comm_semiring k] [group G] (x : monoid_algebra k G) (y : (representation.of_mul_action k G G).as_module) :
x • y = x * y
source
@[simp]
theorem representation.of_mul_action_self_as_module_equiv_apply {k : Type u_1} {G : Type u_2} [comm_semiring k] [group G] (ᾰ : (representation.of_mul_action k G G).as_module) :
⇑representation.of_mul_action_self_as_module_equiv ᾰ = (representation.of_mul_action k G G).as_module_equiv.to_fun ᾰ
source
noncomputable def representation.of_mul_action_self_as_module_equiv {k : Type u_1} {G : Type u_2} [comm_semiring k] [group G] :
(representation.of_mul_action k G G).as_module ≃ₗ[monoid_algebra k G] monoid_algebra k 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
source
@[simp]
theorem representation.of_mul_action_self_as_module_equiv_symm_apply {k : Type u_1} {G : Type u_2} [comm_semiring k] [group G] (ᾰ : G →₀ k) :
⇑(representation.of_mul_action_self_as_module_equiv.symm) ᾰ = (representation.of_mul_action k G G).as_module_equiv.inv_fun ᾰ
source
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
source
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
source
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) :
representation k G (tensor_product k 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
source
@[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)
source
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
source
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)
source
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) :
representation k G (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
source
@[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⁻¹))
source
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) :
representation k G (module.dual k 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
source
@[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) :
⇑(ρV.dual) g = ⇑module.dual.transpose (⇑ρV g⁻¹)
source
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.