LieConjugationDifferential.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

This constructs the adjoint action on the tangent space from the manifold derivative and proves its compatibility with the intrinsic exponential.

def OAI.PolycyclicRecognition.identityDifferential line 21
Source documentation
Differential at the identity, with the codomain identified using the homomorphism's identity law.
```
def identityDifferential (φ : G →* G) :
    GroupLieAlgebra (𝓘(ℝ, E)) G →L[ℝ] GroupLieAlgebra (𝓘(ℝ, E)) G :=
…
```
theorem OAI.PolycyclicRecognition.identityDifferential_comp line 26
theorem OAI.PolycyclicRecognition.identityDifferential_id line 43
theorem OAI.PolycyclicRecognition.contMDiff_conjugation line 48
def OAI.PolycyclicRecognition.conjugationDifferentialHom line 58
Source documentation
The adjoint action as a monoid homomorphism into continuous linear endomorphisms of the actual tangent Lie algebra.
```
def conjugationDifferentialHom :
    G →* (GroupLieAlgebra (𝓘(ℝ, E)) G →L[ℝ] GroupLieAlgebra (𝓘(ℝ, E)) G) where
…
```
theorem OAI.PolycyclicRecognition.conjugation_exponential line 78