NilpotentQuotientIntegration.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating a nilpotent algebra quotient with a continuous section

Lee's Lie correspondence supplies the integrated homomorphism. Surjectivity, the kernel description, and compact lifts follow from the exponential charts.

theorem OAI.PolycyclicRecognition.exists_surjective_integration_with_section line 27
Source documentation
A surjective Lie algebra homomorphism integrates to a surjective group homomorphism with a continuous section obtained from a linear section in logarithmic coordinates.
```
theorem exists_surjective_integration_with_section
    [SimplyConnectedSpace N]
    (integrate : NilpotentLieIntegrationInput (EN := EN) (N := N) (EG := EQ) (G := Q))
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentLieIntegrationInput