Commit 2026-01-30 17:31 8514bd72

View on Github →

feat: Schur's lemma for monoid representations (#33802) Adds an algebra instance on the set of intertwining maps. Proves various versions of Schur's lemma for monoid representations and proves that a finite-dimensional irreducible representation of a commutative monoid is one-dimensional.

Estimated changes

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RepresentationTheory/Intertwining.lean

added theorem Representation.IntertwiningMap.algebraMap_apply

added theorem Representation.IntertwiningMap.coe_mk

added theorem Representation.IntertwiningMap.coe_mul

added theorem Representation.IntertwiningMap.coe_one

added def Representation.IntertwiningMap.comp

added def Representation.IntertwiningMap.equivAlgEnd

added def Representation.IntertwiningMap.id

deleted theorem Representation.IntertwiningMap.id_apply

added def Representation.IntertwiningMap.llcomp

added theorem Representation.IntertwiningMap.mul_apply

Modified Mathlib/RepresentationTheory/Irreducible.lean

added theorem Representation.IsIrreducible.algebraMap_intertwiningMap_bijective_of_isAlgClosed

added theorem Representation.IsIrreducible.bijective_or_eq_zero

added theorem Representation.IsIrreducible.finrank_eq_one_of_isMulCommutative

added theorem Representation.IsIrreducible.injective_or_eq_zero