OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothHomLieDifferential.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Differentiating smooth Lie-group homomorphisms

The differential preserves brackets because the associated invariant vector fields are related by the homomorphism.

  1. def OAI.PolycyclicRecognition.homDifferentialLinear line 24
  2. theorem OAI.PolycyclicRecognition.mfderiv_hom_map_bracket line 28
  3. def OAI.PolycyclicRecognition.homLieDifferential line 43
  4. theorem OAI.PolycyclicRecognition.homLieDifferential_apply line 49