Basic facts about algebra representations

This file collects basic general facts about algebra representations. The purpose of this file is to have general results so that when we prove a corresponding fact about group representations (or Lie algebra representations etc), we can deduce them as special cases of facts from this file.

theorem IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed {A : Type u_1} {V : Type u_2} (k : Type u_3) [Field k] [Ring A] [Algebra k A] [AddCommGroup V] [Module k V] [Module A V] [IsScalarTower k A V] [IsSimpleModule A V] [FiniteDimensional k V] [IsAlgClosed k] : Function.Bijective ⇑(algebraMap k (Module.End A V))

Schur's Lemma: If V is a representation of an algebra A over an algebraically closed field k, then any endomorphism of V is scalar.

theorem IsSimpleModule.finrank_eq_one_of_isMulCommutative (A : Type u_1) (V : Type u_2) (k : Type u_3) [Field k] [Ring A] [Algebra k A] [AddCommGroup V] [Module k V] [Module A V] [IsScalarTower k A V] [IsSimpleModule A V] [FiniteDimensional k V] [IsAlgClosed k] [IsMulCommutative A] : Module.finrank k V = 1

Any finite-dimensional irreducible representation of a commutative algebra over an algebraically closed field is one-dimensional.