OAI/GroupTheory/PolycyclicRecognition/Algebra/LeftTangentTrivialization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Left translation identifies the tangent fibers

The differential of translation back to the identity is an actual continuous linear equivalence. Its matrix in any fixed local tangent chart varies smoothly. These facts supply the frame for the left-invariant metric.

  1. def OAI.PolycyclicRecognition.leftLogDerivative line 22
  2. def OAI.PolycyclicRecognition.leftTranslateDerivative line 25
  3. theorem OAI.PolycyclicRecognition.leftTranslate_leftLog line 28
  4. theorem OAI.PolycyclicRecognition.leftLog_leftTranslate line 48
  5. def OAI.PolycyclicRecognition.leftTangentEquiv line 68
  6. theorem OAI.PolycyclicRecognition.leftLogDerivative_mul line 78
  7. theorem OAI.PolycyclicRecognition.contMDiffAt_leftLogDerivative line 92