OAI/GroupTheory/PolycyclicRecognition/Algebra/SimpleAlgebraAction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A simple algebra action fills all endomorphisms

Schur's lemma identifies the commutant with the scalar field. Jacobson density then gives the full endomorphism algebra in finite dimension.

  1. theorem OAI.PolycyclicRecognition.simple_algebra_action_surjective line 14
  2. theorem OAI.PolycyclicRecognition.irreducible_algebra_span_surjective line 34
  3. theorem OAI.PolycyclicRecognition.irreducible_linear_span_eq_top line 51