OAI/GroupTheory/PolycyclicRecognition/Lattices/CartanNilshadow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The nilpotent Lie algebra attached to the Cartan height action

The graph of minus the semisimple height action is a Lie subalgebra of the affine derivation algebra. Its first coordinate is linearly the original Lie algebra, while its bracket has the semisimple action removed.

  1. def OAI.PolycyclicRecognition.cartanNilshadowSubalgebra line 22
  2. abbrev OAI.PolycyclicRecognition.CartanNilshadow line 42
  3. def OAI.PolycyclicRecognition.cartanNilshadowEquiv line 44
  4. instance OAI.PolycyclicRecognition.(instance at line 67) line 67
  5. theorem OAI.PolycyclicRecognition.cartanNilshadow_bracket line 70
  6. theorem OAI.PolycyclicRecognition.nilpotent_of_square_eq_mul line 79
  7. theorem OAI.PolycyclicRecognition.cartanNilshadow_nilpotent line 93

    Source documentation

    The Cartan graph is nilpotent; no nilshadow theorem is assumed.

    theorem cartanNilshadow_nilpotent : LieRing.IsNilpotent (CartanNilshadow T H) := by
…

    Mentions: OAI.PolycyclicRecognition.CartanNilshadow