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

@[inline, reducible]

abbrev Representation (k : Type u_1) (G : Type u_2) (V : Type u_3) [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] : Type (max u_3 u_2)

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

Equations

• Representation k G V = (G →* V →ₗ[k] V)

def Representation.trivial (k : Type u_1) {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] : Representation k G V

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

Equations

• Representation.trivial k = 1

theorem Representation.trivial_def (k : Type u_1) {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (g : G) (v : V) : ((Representation.trivial k) g) v = v

class Representation.IsTrivial {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Prop

A predicate for representations that fix every element.

• out : ∀ (g : G) (x : V), (ρ g) x = x

instance Representation.instIsTrivialTrivial {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] : Representation.IsTrivial (Representation.trivial k)

Equations

• (_ : Representation.IsTrivial (Representation.trivial k)) = (_ : Representation.IsTrivial (Representation.trivial k))

@[simp]

theorem Representation.apply_eq_self {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : V) [h : Representation.IsTrivial ρ] : (ρ g) x = x

noncomputable def Representation.asAlgebraHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : MonoidAlgebra k G →ₐ[k] Module.End 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

• Representation.asAlgebraHom ρ = (MonoidAlgebra.lift k G (Module.End k V)) ρ

theorem Representation.asAlgebraHom_def {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Representation.asAlgebraHom ρ = (MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ

@[simp]

theorem Representation.asAlgebraHom_single {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (r : k) : (Representation.asAlgebraHom ρ) (Finsupp.single g r) = r • ρ g

theorem Representation.asAlgebraHom_single_one {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) : (Representation.asAlgebraHom ρ) (Finsupp.single g 1) = ρ g

theorem Representation.asAlgebraHom_of {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) : (Representation.asAlgebraHom ρ) ((MonoidAlgebra.of k G) g) = ρ g

def Representation.asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] : Representation k G 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

• Representation.asModule x = V

instance Representation.instAddCommMonoidAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : AddCommMonoid (Representation.asModule ρ)

Equations

• Representation.instAddCommMonoidAsModule ρ = inferInstanceAs (AddCommMonoid V)

instance Representation.instInhabitedAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Inhabited (Representation.asModule ρ)

Equations

• Representation.instInhabitedAsModule ρ = { default := 0 }

noncomputable instance Representation.asModuleModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Module (MonoidAlgebra k G) (Representation.asModule ρ)

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

Equations

• Representation.asModuleModule ρ = Module.compHom V ↑(Representation.asAlgebraHom ρ)

instance Representation.instModuleAsModuleToSemiringInstAddCommMonoidAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Module k (Representation.asModule ρ)

Equations

• Representation.instModuleAsModuleToSemiringInstAddCommMonoidAsModule ρ = inferInstanceAs (Module k V)

def Representation.asModuleEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Representation.asModule ρ ≃+ 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

• Representation.asModuleEquiv ρ = AddEquiv.refl (Representation.asModule ρ)

@[simp]

theorem Representation.asModuleEquiv_map_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (r : MonoidAlgebra k G) (x : Representation.asModule ρ) : (Representation.asModuleEquiv ρ) (r • x) = ((Representation.asAlgebraHom ρ) r) ((Representation.asModuleEquiv ρ) x)

@[simp]

theorem Representation.asModuleEquiv_symm_map_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (r : k) (x : V) : (AddEquiv.symm (Representation.asModuleEquiv ρ)) (r • x) = (algebraMap k (MonoidAlgebra k G)) r • (AddEquiv.symm (Representation.asModuleEquiv ρ)) x

@[simp]

theorem Representation.asModuleEquiv_symm_map_rho {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : V) : (AddEquiv.symm (Representation.asModuleEquiv ρ)) ((ρ g) x) = (MonoidAlgebra.of k G) g • (AddEquiv.symm (Representation.asModuleEquiv ρ)) x

noncomputable def Representation.ofModule' {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] : Representation k G 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

• Representation.ofModule' M = (MonoidAlgebra.lift k G (M →ₗ[k] M)).symm (Algebra.lsmul k k M)

noncomputable def Representation.ofModule {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module (MonoidAlgebra k G) M] : Representation k G (RestrictScalars k (MonoidAlgebra k G) 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

• Representation.ofModule M = (MonoidAlgebra.lift k G (RestrictScalars k (MonoidAlgebra k G) M →ₗ[k] RestrictScalars k (MonoidAlgebra k G) M)).symm (RestrictScalars.lsmul k (MonoidAlgebra k G) M)

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} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module (MonoidAlgebra k G) M] (r : MonoidAlgebra k G) (m : RestrictScalars k (MonoidAlgebra k G) M) : ((Representation.asAlgebraHom (Representation.ofModule M)) r) m = (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) M)) (r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

@[simp]

theorem Representation.ofModule_asModule_act {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : RestrictScalars k (MonoidAlgebra k G) (Representation.asModule ρ)) : ((Representation.ofModule (Representation.asModule ρ)) g) x = (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule ρ))) ((AddEquiv.symm (Representation.asModuleEquiv ρ)) ((ρ g) ((Representation.asModuleEquiv ρ) ((RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule ρ)) x))))

theorem Representation.smul_ofModule_asModule {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module (MonoidAlgebra k G) M] (r : MonoidAlgebra k G) (m : Representation.asModule (Representation.ofModule M)) : (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((Representation.asModuleEquiv (Representation.ofModule M)) (r • m)) = r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((Representation.asModuleEquiv (Representation.ofModule M)) m)

instance Representation.instAddCommGroupAsModuleToCommSemiringToAddCommMonoid {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [I : AddCommGroup V] [Module k V] (ρ : Representation k G V) : AddCommGroup (Representation.asModule ρ)

Equations

• Representation.instAddCommGroupAsModuleToCommSemiringToAddCommMonoid ρ = I

noncomputable def Representation.ofMulAction (k : Type u_1) [CommSemiring k] (G : Type u_2) [Monoid G] (H : Type u_3) [MulAction G H] : Representation k G (H →₀ k)

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

Equations

• One or more equations did not get rendered due to their size.

theorem Representation.ofMulAction_def {k : Type u_1} [CommSemiring k] {G : Type u_2} [Monoid G] {H : Type u_3} [MulAction G H] (g : G) : (Representation.ofMulAction k G H) g = Finsupp.lmapDomain k k fun (x : H) => g • x

theorem Representation.ofMulAction_single {k : Type u_1} [CommSemiring k] {G : Type u_2} [Monoid G] {H : Type u_3} [MulAction G H] (g : G) (x : H) (r : k) : ((Representation.ofMulAction k G H) g) (Finsupp.single x r) = Finsupp.single (g • x) r

def Representation.ofDistribMulAction (k : Type u_1) (G : Type u_2) (A : Type u_3) [CommSemiring k] [Monoid G] [AddCommMonoid A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] : Representation k G 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.

@[simp]

theorem Representation.ofDistribMulAction_apply_apply {k : Type u_1} {G : Type u_2} {A : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (g : G) (a : A) : ((Representation.ofDistribMulAction k G A) g) a = g • a

def Representation.ofMulDistribMulAction (M : Type u_1) (G : Type u_2) [Monoid M] [CommGroup G] [MulDistribMulAction M G] : Representation ℤ M (Additive G)

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

Equations

• Representation.ofMulDistribMulAction M G = MonoidHom.comp (↑(addMonoidEndRingEquivInt (Additive G))) (MonoidHom.comp (↑(monoidEndToAdditive G)) (MulDistribMulAction.toMonoidEnd M G))

@[simp]

theorem Representation.ofMulDistribMulAction_apply_apply (M : Type u_1) (G : Type u_2) [Monoid M] [CommGroup G] [MulDistribMulAction M G] (g : M) (a : Additive G) : ((Representation.ofMulDistribMulAction M G) g) a = Additive.ofMul (g • Additive.toMul a)

@[simp]

theorem Representation.ofMulAction_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] {H : Type u_4} [MulAction G H] (g : G) (f : H →₀ k) (h : H) : (((Representation.ofMulAction k G H) g) f) h = f (g⁻¹ • h)

noncomputable instance Representation.instHMulMonoidAlgebraToSemiringAsModuleFinsuppToZeroToCommMonoidWithZeroToMonoidToDivInvMonoidAddCommMonoidToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringModuleToModuleOfMulActionToMulAction {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] : HMul (MonoidAlgebra k G) (Representation.asModule (Representation.ofMulAction k G G)) (MonoidAlgebra k G)

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} [CommSemiring k] [Group G] (x : MonoidAlgebra k G) (y : Representation.asModule (Representation.ofMulAction k G G)) : x • y = x * y

@[simp]

theorem Representation.ofMulActionSelfAsModuleEquiv_symm_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] : ∀ (a : G →₀ k), (LinearEquiv.symm Representation.ofMulActionSelfAsModuleEquiv) a = (Representation.asModuleEquiv (Representation.ofMulAction k G G)).toEquiv.invFun a

@[simp]

theorem Representation.ofMulActionSelfAsModuleEquiv_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] : ∀ (a : Representation.asModule (Representation.ofMulAction k G G)), Representation.ofMulActionSelfAsModuleEquiv a = (Representation.asModuleEquiv (Representation.ofMulAction k G G)).toEquiv.toFun a

noncomputable def Representation.ofMulActionSelfAsModuleEquiv {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] : Representation.asModule (Representation.ofMulAction k G G) ≃ₗ[MonoidAlgebra k G] MonoidAlgebra 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

• One or more equations did not get rendered due to their size.

def Representation.asGroupHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid 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

• Representation.asGroupHom ρ = MonoidHom.toHomUnits ρ

theorem Representation.asGroupHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) : ↑((Representation.asGroupHom ρ) g) = ρ g

noncomputable def Representation.tprod {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) : Representation k G (TensorProduct 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Representation.tprod_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) : (Representation.tprod ρV ρW) 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} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (r : MonoidAlgebra k G) (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} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρW : Representation k G W) (r : MonoidAlgebra k G) (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} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Representation.linHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) (f : V →ₗ[k] W) : ((Representation.linHom ρV ρW) g) f = ρW g ∘ₗ f ∘ₗ ρV g⁻¹

def Representation.dual {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Representation.dual_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρV : Representation k G V) (g : G) : (Representation.dual ρV) 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} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) : dualTensorHom k V W ∘ₗ TensorProduct.map ((Representation.dual ρV) g) (ρW g) = (Representation.linHom ρV ρW) g ∘ₗ dualTensorHom k V W

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.