Irreducible representations

This file defines irreducible monoid representations.

@[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.

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

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

@[deprecated Representation.isSimpleModule_iff_irreducible_ofModule (since := "2026-02-09")]

theorem Representation.is_simple_module_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

Alias of Representation.isSimpleModule_iff_irreducible_ofModule.

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

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

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

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

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