OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialTangentUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.IsGroupExponential.eq_of_oneParameter_eq line 16
2. theorem OAI.PolycyclicRecognition.conjugationDifferential_eq_of_exponential line 29

   Source documentation

   An exponential-compatible linear action is the actual tangent action; global injectivity of the exponential is not required.

   theorem conjugationDifferential_eq_of_exponential [T2Space G]
       {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp)
       (g : G) (A : GroupLieAlgebra (𝓘(ℝ, E)) G →ₗ[ℝ] GroupLieAlgebra (𝓘(ℝ, E)) G)
       (hA : ∀ v, Exp (A v) = g * Exp v * g⁻¹) :
       ∀ v, conjugationDifferentialHom g v = A v := by
   …

   Mentions: OAI.PolycyclicRecognition.conjugationDifferentialHom