Theorems · Theorem · ring theory

IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed

∀ {A : Type u_1} {V : Type u_2} (k : Type u_3) [inst : Field k] [inst_1 : Ring A] [inst_2 : Algebra k A]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : Module A V] [inst_6 : 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.

Defined in

Mathlib.RepresentationTheory.AlgebraRepresentation.Basic

Cited by

2 results in Mathlib

Foundations

Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldRingAlgebraAddCommGroupModuleModuleIsScalarTowerIsSimpleModuleFiniteDimensionalIsAlgClosed