OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentModelConstruction.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Concrete steps in nilpotent Lie model construction
The abelian case, codimension-one splitting, polynomial derivation actions and the actual semidirect tangent bracket give model existence by dimension induction. Only finite BCH on the already constructed smaller models remains an input.
This file declares nothing itself. It gathers the 7 imports below, so a file that imports it gets all of them.
Imports
- OAI.GroupTheory.PolycyclicRecognition.Geometry.AbelianLieModel
- OAI.GroupTheory.PolycyclicRecognition.Algebra.AbelianDynkinInput
- OAI.GroupTheory.PolycyclicRecognition.Algebra.NilpotentIdealDerivation
- OAI.GroupTheory.PolycyclicRecognition.Algebra.PolynomialDerivationAction
- OAI.GroupTheory.PolycyclicRecognition.Geometry.NilpotentDerivationFlowDerivative
- OAI.GroupTheory.PolycyclicRecognition.Geometry.NilpotentSemidirectGroup
- OAI.GroupTheory.PolycyclicRecognition.Geometry.NilpotentLieExistenceConstruction