Documentation

TauCeti.RepresentationTheory.OfModule

The representation carried by a k[G]-module #

Mathlib's Representation.ofModule' M reads a k[G]-module M whose k-module structure is already the restriction of its k[G]-module structure as a representation of G on M itself, rather than on a type synonym. That is the convenient form -- a left ideal, say, stays a left ideal -- but nothing is recorded about it, so the general theory of representations, which runs on the type synonym ρ.asModule, cannot be applied to it.

This file records what is needed to pass between the two. The algebra map of ofModule' M is the given action (TauCeti.Representation.asAlgebraHom_ofModule'), so (ofModule' M).asModule is M again, with the same k[G]-action (TauCeti.Representation.ofModule'AsModuleEquiv). Consequently ofModule' M is irreducible exactly when M is a simple k[G]-module (TauCeti.Representation.isIrreducible_ofModule'_iff), which is how a module built by hand -- a left ideal, for instance -- is recognised as an irreducible representation. That last statement is stated here, beside the comparison of modules it is read off from, rather than among the self-contained criteria of TauCeti.RepresentationTheory.Irreducible, which say nothing about where the representation came from.

Characters are read off in the same spirit: the character of ofModule' of a finite product of k[G]-modules is the sum of the characters of the factors (TauCeti.Representation.char_ofModule'_pi), and a factor ρ.asModule contributes the character of ρ itself (Representation.char_ofModule'_asModule). Together they compute the character of a direct sum of representations assembled as a k[G]-module.

Main results #

source
@[simp]
theorem TauCeti.Representation.ofModule'_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_3) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] (g : G) (x : M) :
((Representation.ofModule' M) g) x = MonoidAlgebra.single g 1 • x

A group element acts on Representation.ofModule' M through the corresponding group-algebra basis element.

source
theorem TauCeti.Representation.asAlgebraHom_ofModule' {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_3) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] :
(Representation.ofModule' M).asAlgebraHom = Algebra.lsmul k k M

The algebra map of Representation.ofModule' M is the action of k[G] on M that it was built from.

source
@[simp]
theorem TauCeti.Representation.asAlgebraHom_ofModule'_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_3) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] (r : MonoidAlgebra k G) (x : M) :
((Representation.ofModule' M).asAlgebraHom r) x = r • x
source
noncomputable def TauCeti.Representation.ofModule'AsModuleEquiv {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_3) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] :
(Representation.ofModule' M).asModule ≃ₗ[MonoidAlgebra k G] M

The k[G]-module underlying Representation.ofModule' M is M itself. The map is the identity; the content is that the two k[G]-actions agree.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Representation.ofModule'AsModuleEquiv_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_3) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] (x : (Representation.ofModule' M).asModule) :
    (ofModule'AsModuleEquiv M) x = x

    TauCeti.Representation.ofModule'AsModuleEquiv is the identity map: its two sides are the same type, and all it records is that their k[G]-actions agree.

    source
    theorem TauCeti.Representation.isIrreducible_ofModule'_iff {k : Type u_1} {G : Type u_2} [Field k] [Monoid G] (M : Type u_3) [AddCommGroup M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] :
    (Representation.ofModule' M).IsIrreducible ↔ IsSimpleModule (MonoidAlgebra k G) M

    Representation.ofModule' M is irreducible exactly when M is a simple k[G]-module. This is the form of Representation.irreducible_iff_isSimpleModule_asModule that applies to a module given in advance, with no type synonym in the way.

    source
    @[simp]
    theorem TauCeti.Representation.char_ofModule'_pi {k : Type u_1} {G : Type u_2} [Field k] [Monoid G] {ι : Type u_3} [Fintype ι] (M : ι → Type u_4) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module k (M i)] [(i : ι) → Module (MonoidAlgebra k G) (M i)] [∀ (i : ι), IsScalarTower k (MonoidAlgebra k G) (M i)] [∀ (i : ι), FiniteDimensional k (M i)] (g : G) :
    (Representation.ofModule' ((i : ι) → M i)).character g = ∑ i : ι, (Representation.ofModule' (M i)).character g

    The character of Representation.ofModule' of a finite product of k[G]-modules is the sum of the characters of the factors. This is the finite-product counterpart of Representation.char_prod, for representations read off a k[G]-module; a factor of the form ρ.asModule is then evaluated by Representation.char_ofModule'_asModule.

    source
    @[simp]
    theorem Representation.char_ofModule'_asModule {k : Type u_1} {G : Type u_2} [Field k] [Monoid G] {V : Type u_3} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) :
    (ofModule' ρ.asModule).character g = ρ.character g

    The character of Representation.ofModule' ρ.asModule is the character of ρ. This lets a character computed on a k[G]-module assembled from asModule summands be expressed through the original representations.