Documentation

LeanPool.RegtsSevenster.RS.Classical.SchurTheory.NativeAction

The native simple-submodule representation #

The representation of a simple submodule of the regular module, carried on the canonically-instanced restricted-scalars subtype via Representation.ofModule': the algebra action is definitionally scalar multiplication, so no transparency options and no equivalence transport are needed.

source
@[reducible, inline]
abbrev RS.subCarrier {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) :
Type u_1

The canonically-instanced carrier.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance RS.instModuleMonoidAlgebraComplexSubCarrier {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) :
    Module (MonoidAlgebra ℂ G) (subCarrier S)

    The submodule carries the group-algebra action, definitionally by scalar multiplication.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance RS.instIsScalarTowerComplexMonoidAlgebraSubCarrier {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) :
    IsScalarTower ℂ (MonoidAlgebra ℂ G) (subCarrier S)

    The complex and group-algebra actions agree on scalars.

    source
    noncomputable def RS.rhoS {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) :
    Representation ℂ G (subCarrier S)

    The native representation of a submodule of the regular module.

    Equations
    Instances For
      source
      theorem RS.rhoS_asAlgebraHom_apply {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (y : MonoidAlgebra ℂ G) (m : subCarrier S) :
      ((rhoS S).asAlgebraHom y) m = y • m

      The algebra action of the native representation is scalar multiplication.

      source
      theorem RS.rhoS_apply {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (g : G) (m : subCarrier S) :
      ((rhoS S) g) m = MonoidAlgebra.single g 1 • m

      Its group action is scalar multiplication by the group element.

      source
      theorem RS.isIrredRep_rhoS {G : Type u_1} [Group G] (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)) (hS : IsSimpleModule (MonoidAlgebra ℂ G) ↥S) :
      IsIrredRep (rhoS S)

      The native representation of a simple submodule satisfies the invariant-submodule irreducibility.