Irreducible representations

This file defines irreducible monoid representations.

class 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) extends IsSimpleOrder (Subrepresentation ρ) : Prop

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

• exists_pair_ne : ∃ (x : Subrepresentation ρ) (y : Subrepresentation ρ), x ≠ y
• eq_bot_or_eq_top (a : Subrepresentation ρ) : a = ⊥ ∨ a = ⊤

theorem Representation.isIrreducible_iff {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 ↔ IsSimpleOrder (Subrepresentation ρ)

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.is_simple_module_iff_irreducible_ofModule {G : Type u_1} {k : Type u_2} [Monoid G] [Field k] (M : Type u_4) [AddCommGroup M] [Module (MonoidAlgebra k G) M] : IsSimpleModule (MonoidAlgebra k G) M ↔ (ofModule M).IsIrreducible