OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialIntegralCurve.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic exponential curves and the invariant vector field

The group law and derivative at zero determine the global differential equation of an intrinsic exponential curve.

  1. theorem OAI.PolycyclicRecognition.IsGroupExponential.isMIntegralCurve line 22
  2. theorem OAI.PolycyclicRecognition.IsGroupExponential.unique line 72

    Source documentation

    The intrinsic characterization determines the exponential uniquely. This uses manifold ODE uniqueness for the already constructed invariant vector field, with no external Lie-theoretic input.

    theorem IsGroupExponential.unique [T2Space G]
    {Exp Exp' : GroupLieAlgebra (𝓘(ℝ, E)) G → G}
    (hExp : IsGroupExponential Exp) (hExp' : IsGroupExponential Exp') : Exp = Exp' := by
…