OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothLieNaturality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Naturality of the intrinsic exponential at C-infinity regularity

The exponential compatibility clause of Lie integration follows from the chain rule and uniqueness of invariant integral curves. No integration theorem or representation theorem is used here.

  1. theorem OAI.PolycyclicRecognition.SmoothLie.mfderiv_hom_invariant line 28
  2. theorem OAI.PolycyclicRecognition.SmoothLie.invariant_integralCurve_map line 62
  3. theorem OAI.PolycyclicRecognition.SmoothLie.IsGroupExponential.map_of_mdifferentiable line 79

    Source documentation

    Every differentiable homomorphism commutes with the intrinsic exponential.

    theorem IsGroupExponential.map_of_mdifferentiable [T2Space H]
    {ExpG : GroupLieAlgebra (𝓘(ℝ, E)) G → G}
    {ExpH : GroupLieAlgebra (𝓘(ℝ, F)) H → H}
    (hG : IsGroupExponential ExpG) (hH : IsGroupExponential ExpH)
    (φ : G →* H) (hφ : MDifferentiable (𝓘(ℝ, E)) (𝓘(ℝ, F)) φ)
    (v : GroupLieAlgebra (𝓘(ℝ, E)) G) :
    φ (ExpG v) = ExpH ((mfderiv (𝓘(ℝ, E)) (𝓘(ℝ, F)) φ 1) v) := by
…