NilpotentLieModel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The simply connected nilpotent Lie models needed by Cartan factorization

J. M. Lee, Introduction to Smooth Manifolds, second edition (2013), Theorem 20.21, p.531, gives the simply connected integration of a finite dimensional real Lie algebra. For the nilpotent case, exponential coordinates have a finite polynomial BCH law: F. Baudoin, An Introduction to the Geometry of Stochastic Flows (2004), Appendix B.5–B.6, pp.123–126. These coordinates give the analytic Lie-group model used here. No metric-growth, Haar-volume, Cartan-factorization, or quasi-isometry conclusion is included in this input.

The universe of the model can be chosen to match the algebra by using its finite-dimensional coordinate space (or a lifted copy).

structure OAI.PolycyclicRecognition.NilpotentLieModel line 29
Source documentation
Only the finite-dimensional simply connected integration data. Haar measure and intrinsic exponentials are obtained from their separate input.
```
structure NilpotentLieModel (L : Type u) [LieRing L] [LieAlgebra ℝ L] where
…
```
def OAI.PolycyclicRecognition.NilpotentLieExistenceInput line 53
Source documentation
The nilpotent specialization of Lie correspondence in exponential polynomial coordinates.
```
def NilpotentLieExistenceInput (L : Type u) [LieRing L] [LieAlgebra ℝ L]
    [FiniteDimensional ℝ L] : Prop :=
…
```
theorem OAI.PolycyclicRecognition.NilpotentLieModel.tangent_nilpotent line 63
Source documentation
Nilpotence is transported to the actual tangent algebra; it is not an extra assumption about the chosen group.
```
theorem tangent_nilpotent (hnil : LieRing.IsNilpotent L) :
    LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, M.modelSpace)) M.carrier) :=
…
```

theorem OAI.PolycyclicRecognition.NilpotentLieModel.exists_exponential_chart line 69

Source documentation

The separate published exponential theorem supplies an actual chart on the chosen model.

theorem exists_exponential_chart (hnil : LieRing.IsNilpotent L)
    (haar : NilpotentExponentialHaarInput M.modelSpace M.carrier) :
    ∃ Exp : GroupLieAlgebra (𝓘(ℝ, M.modelSpace)) M.carrier → M.carrier,
      IsGroupExponential Exp ∧
      ∃ chart : GroupLieAlgebra (𝓘(ℝ, M.modelSpace)) M.carrier ≃ₜ M.carrier,
        ∀ x, chart x = Exp x := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput