# 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.linHom
• Representation.dual

## Implementation notes #

Representations of a monoid G on a k-module V are implemented as homomorphisms G →* (V →ₗ[k] V). We use the abbreviation Representation for this hom space.

The theorem asAlgebraHom_def constructs a module over the group k-algebra of G (implemented as MonoidAlgebra k G) corresponding to a representation. If ρ : Representation k G V, this module can be accessed via ρ.asModule. Conversely, given a MonoidAlgebra k G-module M M.ofModule is the associociated representation seen as a homomorphism.

@[inline, reducible]
abbrev Representation (k : Type u_1) (G : Type u_2) (V : Type u_3) [] [] [] [Module k V] :
Type (max u_2 u_3)

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

Equations
Instances For
def Representation.trivial (k : Type u_1) {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] :

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

Equations
Instances For
theorem Representation.trivial_def (k : Type u_1) {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (g : G) (v : V) :
() v = v
class Representation.IsTrivial {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :

A predicate for representations that fix every element.

• out : ∀ (g : G) (x : V), (ρ g) x = x
Instances
instance Representation.instIsTrivialTrivial {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] :
Equations
• =
@[simp]
theorem Representation.apply_eq_self {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (g : G) (x : V) [h : ] :
(ρ g) x = x
noncomputable def Representation.asAlgebraHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :

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

Equations
Instances For
theorem Representation.asAlgebraHom_def {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :
= (MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ
@[simp]
theorem Representation.asAlgebraHom_single {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (g : G) (r : k) :
= r ρ g
theorem Representation.asAlgebraHom_single_one {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (g : G) :
= ρ g
theorem Representation.asAlgebraHom_of {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (g : G) :
(() g) = ρ g
def Representation.asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] :
Type u_3

If ρ : Representation k G V, then ρ.asModule is a type synonym for V, which we equip with an instance Module (MonoidAlgebra k G) ρ.asModule.

You should use asModuleEquiv : ρ.asModule ≃+ V to translate terms.

Equations
Instances For
instance Representation.instAddCommMonoidAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :
Equations
instance Representation.instInhabitedAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :
Equations
• = { default := 0 }
noncomputable instance Representation.asModuleModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :

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

Equations
instance Representation.instModuleAsModuleToSemiringInstAddCommMonoidAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :
Equations
def Representation.asModuleEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) :

The additive equivalence from the Module (MonoidAlgebra 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
Instances For
@[simp]
theorem Representation.asModuleEquiv_map_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (r : ) (x : ) :
(r x) = () ()
@[simp]
theorem Representation.asModuleEquiv_symm_map_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (r : k) (x : V) :
(r x) = (algebraMap k ()) r
@[simp]
theorem Representation.asModuleEquiv_symm_map_rho {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (g : G) (x : V) :
((ρ g) x) = () g
noncomputable def Representation.ofModule' {k : Type u_1} {G : Type u_2} [] [] (M : Type u_4) [] [Module k M] [Module () M] [IsScalarTower k () M] :

Build a Representation k G M from a [Module (MonoidAlgebra k G) M].

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

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

Equations
Instances For
noncomputable def Representation.ofModule {k : Type u_1} {G : Type u_2} [] [] (M : Type u_4) [] [Module () M] :

Build a Representation from a [Module (MonoidAlgebra k G) M].

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

Equations
Instances For

## ofModule and asModule are inverses. #

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

See Rep.equivalenceModuleMonoidAlgebra for the full statement.

Starting with ρ : Representation k G V, converting to a module and back again we have a Representation k G (restrictScalars k (MonoidAlgebra k G) ρ.asModule). To compare these, we use the composition of restrictScalarsAddEquiv and ρ.asModuleEquiv.

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

@[simp]
theorem Representation.ofModule_asAlgebraHom_apply_apply {k : Type u_1} {G : Type u_2} [] [] (M : Type u_4) [] [Module () M] (r : ) (m : RestrictScalars k () M) :
= (AddEquiv.symm ()) (r () m)
@[simp]
theorem Representation.ofModule_asModule_act {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (g : G) (x : ) :
x = () ( ((ρ g) ( (() x))))
theorem Representation.smul_ofModule_asModule {k : Type u_1} {G : Type u_2} [] [] (M : Type u_4) [] [Module () M] (r : ) :
() ( (r m)) = r ()
instance Representation.instAddCommGroupAsModuleToCommSemiringToAddCommMonoid {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [I : ] [Module k V] (ρ : ) :
Equations
noncomputable def Representation.ofMulAction (k : Type u_1) [] (G : Type u_2) [] (H : Type u_3) [] :

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

Equations
• = { toOneHom := { toFun := fun (g : G) => Finsupp.lmapDomain k k fun (x : H) => g x, map_one' := }, map_mul' := }
Instances For
theorem Representation.ofMulAction_def {k : Type u_1} [] {G : Type u_2} [] {H : Type u_3} [] (g : G) :
() g = Finsupp.lmapDomain k k fun (x : H) => g x
theorem Representation.ofMulAction_single {k : Type u_1} [] {G : Type u_2} [] {H : Type u_3} [] (g : G) (x : H) (r : k) :
(() g) () = Finsupp.single (g x) r
def Representation.ofDistribMulAction (k : Type u_1) (G : Type u_2) (A : Type u_3) [] [] [] [Module k A] [] [] :

Turns a k-module A with a compatible DistribMulAction of a monoid G into a k-linear G-representation on A.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Representation.ofDistribMulAction_apply_apply {k : Type u_1} {G : Type u_2} {A : Type u_3} [] [] [] [Module k A] [] [] (g : G) (a : A) :
( g) a = g a
def Representation.ofMulDistribMulAction (M : Type u_1) (G : Type u_2) [] [] [] :

Turns a CommGroup G with a MulDistribMulAction of a monoid M into a ℤ-linear M-representation on Additive G.

Equations
Instances For
@[simp]
theorem Representation.ofMulDistribMulAction_apply_apply (M : Type u_1) (G : Type u_2) [] [] [] (g : M) (a : ) :
@[simp]
theorem Representation.ofMulAction_apply {k : Type u_1} {G : Type u_2} [] [] {H : Type u_4} [] (g : G) (f : H →₀ k) (h : H) :
((() g) f) h = f (g⁻¹ h)
Equations
• One or more equations did not get rendered due to their size.
theorem Representation.ofMulAction_self_smul_eq_mul {k : Type u_1} {G : Type u_2} [] [] (x : ) (y : ) :
x y = x * y
@[simp]
theorem Representation.ofMulActionSelfAsModuleEquiv_symm_apply {k : Type u_1} {G : Type u_2} [] [] :
∀ (a : G →₀ k), (LinearEquiv.symm Representation.ofMulActionSelfAsModuleEquiv) a = .invFun a
@[simp]
theorem Representation.ofMulActionSelfAsModuleEquiv_apply {k : Type u_1} {G : Type u_2} [] [] :
∀ (a : ), Representation.ofMulActionSelfAsModuleEquiv a = .toFun a
noncomputable def Representation.ofMulActionSelfAsModuleEquiv {k : Type u_1} {G : Type u_2} [] [] :

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
• One or more equations did not get rendered due to their size.
Instances For
def Representation.asGroupHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k 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
Instances For
theorem Representation.asGroupHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρ : ) (g : G) :
() = ρ g
noncomputable def Representation.tprod {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [] [] [] [Module k V] [] [Module k 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
• = { toOneHom := { toFun := fun (g : G) => TensorProduct.map (ρV g) (ρW g), map_one' := }, map_mul' := }
Instances For
@[simp]
theorem Representation.tprod_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [] [] [] [Module k V] [] [Module k W] (ρV : ) (ρW : ) (g : G) :
() g = TensorProduct.map (ρV g) (ρW g)
theorem Representation.smul_tprod_one_asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [] [] [] [Module k V] [] [Module k W] (ρV : ) (r : ) (x : V) (y : W) :
let x' := x; let z := x ⊗ₜ[k] y; r z = (r x') ⊗ₜ[k] y
theorem Representation.smul_one_tprod_asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [] [] [] [Module k V] [] [Module k W] (ρW : ) (r : ) (x : V) (y : W) :
let y' := y; let z := x ⊗ₜ[k] y; r z = x ⊗ₜ[k] (r y')
def Representation.linHom {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [] [] [] [Module k V] [] [Module k W] (ρV : ) (ρ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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Representation.linHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [] [] [] [Module k V] [] [Module k W] (ρV : ) (ρW : ) (g : G) (f : V →ₗ[k] W) :
(() g) f = ρW g ∘ₗ f ∘ₗ ρV g⁻¹
def Representation.dual {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Representation.dual_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [] [] [] [Module k V] (ρV : ) (g : G) :
() g = Module.Dual.transpose (ρV g⁻¹)
theorem Representation.dualTensorHom_comm {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [] [] [] [Module k V] [] [Module k W] (ρV : ) (ρW : ) (g : G) :
∘ₗ TensorProduct.map (() g) (ρW g) = () g ∘ₗ

Given $k$-modules $V, W$, there is a homomorphism $φ : V^* ⊗ W → Hom_k(V, W)$ (implemented by LinearAlgebra.Contraction.dualTensorHom`). 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.