Documentation

Mathlib.RepresentationTheory.Basic

Monoid representations #

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

@[reducible, inline]
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_2 u_3)

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

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

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

Equations
@[simp]
theorem Representation.trivial_apply (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) :
((trivial k G V) 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) :

A predicate for representations that fix every element.

Instances
    instance Representation.instIsTrivialTrivial {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] :
    @[simp]
    theorem Representation.isTrivial_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) [ρ.IsTrivial] (g : G) :
    theorem Representation.isTrivial_apply {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) [ρ.IsTrivial] (g : G) (x : V) :
    (ρ g) x = x
    @[simp]
    theorem Representation.inv_self_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) (x : V) :
    (ρ g⁻¹) ((ρ g) x) = x
    @[simp]
    theorem Representation.self_inv_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) (x : V) :
    (ρ g) ((ρ g⁻¹) x) = x
    theorem Representation.apply_bijective {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) :
    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) :

    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
    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) :
    @[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) :
    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) :
    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) :
    ρ.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 VType 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
    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) :
    Equations
    noncomputable instance Representation.instModuleAsModule {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) :

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

    Equations
    instance Representation.instModuleAsModule_1 {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) :
    Equations
    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) :

    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
    @[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 : ρ.asModule) :
    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) :
    @[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) :
    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] :

    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
    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] :

    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

    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.single_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) (t : k) (g : G) (v : ρ.asModule) :
    def Representation.subrepresentation {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) (W : Submodule k V) (le_comap : ∀ (g : G), W Submodule.comap (ρ g) W) :

    Given a k-linear G-representation (V, ρ), this is the representation defined by restricting ρ to a G-invariant k-submodule of V.

    Equations
    @[simp]
    theorem Representation.subrepresentation_apply {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) (W : Submodule k V) (le_comap : ∀ (g : G), W Submodule.comap (ρ g) W) (g : G) :
    (ρ.subrepresentation W le_comap) g = (ρ g).restrict
    def Representation.quotient {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (W : Submodule k V) (le_comap : ∀ (g : G), W Submodule.comap (ρ g) W) :

    Given a k-linear G-representation (V, ρ) and a G-invariant k-submodule W ≤ V, this is the representation induced on V ⧸ W by ρ.

    Equations
    • ρ.quotient W le_comap = { toFun := fun (g : G) => W.mapQ W (ρ g) , map_one' := , map_mul' := }
    @[simp]
    theorem Representation.quotient_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (W : Submodule k V) (le_comap : ∀ (g : G), W Submodule.comap (ρ g) W) (g : G) :
    (ρ.quotient W le_comap) g = W.mapQ W (ρ g)
    theorem Representation.apply_eq_of_coe_eq {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) (S : Subgroup G) [IsTrivial (MonoidHom.comp ρ S.subtype)] (g h : G) (hgh : g = h) :
    ρ g = ρ h
    def Representation.ofQuotient {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) (S : Subgroup G) [S.Normal] [IsTrivial (MonoidHom.comp ρ S.subtype)] :

    Given a normal subgroup S ≤ G, a G-representation ρ which is trivial on S factors through G ⧸ S.

    Equations
    @[simp]
    theorem Representation.ofQuotient_coe_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) (S : Subgroup G) [S.Normal] [IsTrivial (MonoidHom.comp ρ S.subtype)] (g : G) (x : V) :
    ((ρ.ofQuotient S) g) x = (ρ g) x
    instance Representation.instAddCommGroupAsModule {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) :
    Equations
    noncomputable def Representation.ofMulAction (k : Type u_1) [CommSemiring k] (G : Type u_2) [Monoid G] (H : Type u_3) [MulAction G H] :

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

    Equations
    @[reducible, inline]
    noncomputable abbrev Representation.leftRegular (k : Type u_1) [CommSemiring k] (G : Type u_2) [Monoid G] :

    The natural k-linear G-representation on k[G] induced by left multiplication in G.

    Equations
    @[reducible, inline]
    noncomputable abbrev Representation.diagonal (k : Type u_1) [CommSemiring k] (G : Type u_2) [Monoid G] (n : ) :
    Representation k G ((Fin nG) →₀ k)

    The natural k-linear G-representation on k[Gⁿ] induced by left multiplication in G.

    Equations
    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) :
    (ofMulAction k G H) g = Finsupp.lmapDomain k k fun (x : H) => g x
    @[simp]
    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) :
    ((ofMulAction k G H) g) (Finsupp.single x r) = Finsupp.single (g x) r

    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) :
    ((ofDistribMulAction k G A) g) a = g 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) :
    (((ofMulAction k G H) g) f) h = f (g⁻¹ h)
    theorem Representation.ofMulAction_self_smul_eq_mul {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (x : MonoidAlgebra k G) (y : (ofMulAction k G G).asModule) :
    x y = x * y

    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
    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) :
    (ρ.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) :

    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} [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) :
    (ρV.tprod ρ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) :

    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
    • ρV.linHom ρW = { toFun := fun (g : G) => { toFun := fun (f : V →ₗ[k] W) => ρW g ∘ₗ f ∘ₗ ρV g⁻¹, map_add' := , map_smul' := }, map_one' := , map_mul' := }
    @[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) :
    ((ρV.linHom ρ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) :

    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
    • ρV.dual = { toFun := fun (g : G) => { toFun := fun (f : Module.Dual k V) => f ∘ₗ ρV g⁻¹, map_add' := , map_smul' := }, map_one' := , map_mul' := }
    @[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) :
    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 (ρV.dual g) (ρW g) = (ρV.linHom ρW) g ∘ₗ dualTensorHom k V W

    Given k-modules V,W, there is a homomorphism φ:VWHomk(V,W) (implemented by dualTensorHom in Mathlib/LinearAlgebra/Contraction.lean). Given representations of G on V and W,there are representations of G on VW and on Homk(V,W). This lemma says that φ is G-linear.

    noncomputable def Representation.finsupp {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) (α : Type u_6) :

    The representation on α →₀ A defined pointwise by a representation on A.

    Equations
    theorem Representation.finsupp_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) (α : Type u_6) (g : G) :
    (ρ.finsupp α) g = (Finsupp.lsum k) fun (i : α) => Finsupp.lsingle i ∘ₗ ρ g
    @[simp]
    theorem Representation.finsupp_single {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : Type u_3} {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) (g : G) (x : α) (a : A) :
    ((ρ.finsupp α) g) (Finsupp.single x a) = Finsupp.single x ((ρ g) a)
    @[reducible, inline]
    noncomputable abbrev Representation.free (k : Type u_6) (G : Type u_7) [CommSemiring k] [Monoid G] (α : Type u_8) :

    The representation on α →₀ k[G] defined pointwise by the left regular representation.

    Equations
    theorem Representation.free_single_single {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : Type u_3} (g h : G) (i : α) (r : k) :
    noncomputable def Representation.finsuppLEquivFreeAsModule (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : Type u_6) :

    The free k[G]-module on a type α is isomorphic to the representation free k G α.

    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable def Representation.freeAsModuleBasis (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : Type u_6) :
    Basis α (MonoidAlgebra k G) (free k G α).asModule

    α gives a k[G]-basis of the representation free k G α.

    Equations
    theorem Representation.free_asModule_free (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : Type u_6) :