OAI/GroupTheory/PolycyclicRecognition/Geometry/AbelianLieModel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The abelian base case of nilpotent Lie model existence

An abelian real Lie algebra is integrated by its additive vector group. The equivalence below identifies the actual invariant-vector-field bracket.

  1. theorem OAI.PolycyclicRecognition.vectorGroup_invariantField line 36
  2. theorem OAI.PolycyclicRecognition.vectorGroup_bracket line 44
  3. def OAI.PolycyclicRecognition.abelianLieModel line 61

    Source documentation

    The additive group, equipped with its actual tangent Lie algebra.

    def abelianLieModel : NilpotentLieModel V := by
…

    Mentions: OAI.PolycyclicRecognition.NilpotentLieModel

  4. theorem OAI.PolycyclicRecognition.nilpotentLieExistenceInput_of_abelian line 77

    Source documentation

    No Lie-existence hypothesis is needed in the abelian base case.

    theorem nilpotentLieExistenceInput_of_abelian
    (L : Type*) [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L] [IsLieAbelian L] :
    NilpotentLieExistenceInput L := by
…

    Mentions: OAI.PolycyclicRecognition.NilpotentLieExistenceInput