LieIntegrationInput.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Published integration input for nilpotent subalgebras

J. M. Lee, Introduction to Smooth Manifolds, second edition, GTM 218, Springer (2013), Theorem 20.19 (p.530) and Proposition 20.8(g) (p.520). https://doi.org/10.1007/978-1-4419-9982-5 Theorem 20.19 integrates a Lie algebra homomorphism from a simply connected Lie group; Proposition 20.8(g) supplies exponential compatibility. We retain only nilpotent source groups, the smooth homomorphism, its prescribed differential and its action on the intrinsic exponential. Closedness is proved separately from the already available global charts, rather than added to the input.

def OAI.PolycyclicRecognition.NilpotentLieIntegrationInput line 34
Source documentation
Nilpotent-domain specialization of Lie's integration theorem and naturality of the exponential.
```
def NilpotentLieIntegrationInput : Prop :=
…
```
theorem OAI.PolycyclicRecognition.exists_closed_integration line 46
Source documentation
Integration plus the two global charts yields a closed subgroup map whose range is exactly the exponential image of the Lie-algebra range.
```
theorem exists_closed_integration
    [SimplyConnectedSpace N]
    (integrate : NilpotentLieIntegrationInput (EN := EN) (N := N) (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentLieIntegrationInput