OAI/GroupTheory/PolycyclicRecognition/Geometry/LieHomDifferential.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.mdifferentiable_hom_of_mdifferentiableAt_one line 19

   Source documentation

   Differentiability at the identity suffices for a group homomorphism.

   theorem mdifferentiable_hom_of_mdifferentiableAt_one (φ : G →* H)
       (hφ : MDifferentiableAt (𝓘(ℝ, E)) (𝓘(ℝ, F)) φ 1) :
       MDifferentiable (𝓘(ℝ, E)) (𝓘(ℝ, F)) φ := by
   …

2. theorem OAI.PolycyclicRecognition.contMDiff_hom_of_contMDiffAt_one line 39

   Source documentation

   The same translation argument propagates smoothness from the identity.

   theorem contMDiff_hom_of_contMDiffAt_one (φ : G →* H)
       (hφ : ContMDiffAt (𝓘(ℝ, E)) (𝓘(ℝ, F)) ∞ φ 1) :
       ContMDiff (𝓘(ℝ, E)) (𝓘(ℝ, F)) ∞ φ := by
   …

3. theorem OAI.PolycyclicRecognition.IsGroupExponential.map_of_mdifferentiableAt_one line 58
4. theorem OAI.PolycyclicRecognition.hom_eq_of_exponential_surjective line 69

   Source documentation

   In exponential coordinates, a homomorphism is determined by its differential at the identity.

   theorem hom_eq_of_exponential_surjective [T2Space H]
       {ExpG : GroupLieAlgebra (𝓘(ℝ, E)) G → G}
       {ExpH : GroupLieAlgebra (𝓘(ℝ, F)) H → H}
       (hG : IsGroupExponential ExpG) (hH : IsGroupExponential ExpH)
       (hExpG : Function.Surjective ExpG)
       (φ ψ : G →* H)
       (hφ : MDifferentiableAt (𝓘(ℝ, E)) (𝓘(ℝ, F)) φ 1)
       (hψ : MDifferentiableAt (𝓘(ℝ, E)) (𝓘(ℝ, F)) ψ 1)
       (hderiv : ∀ v, mfderiv (𝓘(ℝ, E)) (𝓘(ℝ, F)) φ 1 v =
         mfderiv (𝓘(ℝ, E)) (𝓘(ℝ, F)) ψ 1 v) : φ = ψ := by
   …