Documentation

Mathlib.RepresentationTheory.Irreducible

Irreducible representations #

This file defines irreducible monoid representations.

source
@[reducible, inline]
abbrev Representation.IsIrreducible {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) :
Prop

A representation ρ is irreducible if it is non-trivial and has no proper non-trivial subrepresentations.

Equations
Instances For
    source
    theorem Representation.irreducible_iff_isSimpleModule_asModule {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) :
    ρ.IsIrreducible ↔ IsSimpleModule (MonoidAlgebra k G) ρ.asModule
    source
    theorem Representation.isSimpleModule_iff_irreducible_ofModule {G : Type u_1} {k : Type u_2} [Monoid G] [Field k] (M : Type u_5) [AddCommGroup M] [Module (MonoidAlgebra k G) M] :
    IsSimpleModule (MonoidAlgebra k G) M ↔ (ofModule M).IsIrreducible
    source
    instance Representation.IsIrreducible.instIsSimpleModuleMonoidAlgebraAsModule {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] {ρ : Representation k G V} [ρ.IsIrreducible] :
    IsSimpleModule (MonoidAlgebra k G) ρ.asModule
    source
    theorem Representation.IsIrreducible.injective_or_eq_zero {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) [ρ.IsIrreducible] :
    Function.Injective ⇑f ∨ f = 0
    source
    theorem Representation.IsIrreducible.surjective_or_eq_zero {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} [ρ.IsIrreducible] (g : σ.IntertwiningMap ρ) :
    Function.Surjective ⇑g ∨ g = 0
    source
    theorem Representation.IsIrreducible.bijective_or_eq_zero {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} (f : ρ.IntertwiningMap σ) [ρ.IsIrreducible] [σ.IsIrreducible] :
    Function.Bijective ⇑f ∨ f = 0
    source
    instance Representation.IsIrreducible.instSubsingletonIntertwiningMapOfIsEmptyEquiv {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] {ρ : Representation k G V} {σ : Representation k G W} [ρ.IsIrreducible] [σ.IsIrreducible] [IsEmpty (ρ.Equiv σ)] :
    Subsingleton (ρ.IntertwiningMap σ)
    source
    theorem Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] {ρ : Representation k G V} [ρ.IsIrreducible] [FiniteDimensional k V] [IsAlgClosed k] :
    Function.Bijective ⇑(algebraMap k (ρ.IntertwiningMap ρ))
    source
    @[simp]
    theorem Representation.IsIrreducible.finrank_intertwiningMap_self {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [ρ.IsIrreducible] [FiniteDimensional k V] [IsAlgClosed k] :
    Module.finrank k (ρ.IntertwiningMap ρ) = 1
    source
    theorem Representation.IsIrreducible.finrank_eq_one_of_isMulCommutative {G : Type u_1} {k : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) [ρ.IsIrreducible] [FiniteDimensional k V] [IsAlgClosed k] [IsMulCommutative G] :
    Module.finrank k V = 1