OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialNaturality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Naturality of the intrinsic exponential

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.mfderiv_hom_invariant line 23
  2. theorem OAI.PolycyclicRecognition.invariant_integralCurve_map line 57
  3. theorem OAI.PolycyclicRecognition.IsGroupExponential.map_of_mdifferentiable line 74

    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
…