OAI/GroupTheory/PolycyclicRecognition/Geometry/DynkinGlobalExponential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global nilpotent exponential coordinates from finite BCH

Finite BCH gives invertible translations on the Lie algebra. Local exponential coordinates therefore extend to a covering; simple connectedness removes its fibers. The global-chart assumption is not used.

  1. theorem OAI.PolycyclicRecognition.nilpotentGlobalExponentialChart_of_dynkin line 25