OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialSmoothHom.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smoothness and differential of exponential-compatible homomorphisms

Coordinates of the second kind reduce smoothness to the individual one-parameter subgroups. This applies to arbitrary finite-dimensional Lie group targets and does not assume a linear representation of the target.

  1. theorem OAI.PolycyclicRecognition.map_exponentialProduct line 28
  2. theorem OAI.PolycyclicRecognition.contMDiffAt_one_of_exponential_compatibility line 44
  3. theorem OAI.PolycyclicRecognition.contMDiff_of_exponential_compatibility line 80
  4. theorem OAI.PolycyclicRecognition.mfderiv_eq_of_exponential_compatibility line 102

    Source documentation

    Differentiating exponential compatibility recovers the specified linear map.

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