OAI/GroupTheory/PolycyclicRecognition/Algebra/ChartedVectorFieldBracket.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Lie brackets in vector-space charts

The source chart is used only locally. This bridges the differential of an algebra-valued map with the intrinsic bracket of vector fields.

  1. def OAI.PolycyclicRecognition.chartVectorField line 23
  2. theorem OAI.PolycyclicRecognition.mlieBracket_eq_chartBracket line 26
  3. theorem OAI.PolycyclicRecognition.differentiableAt_chartVectorField line 43
  4. theorem OAI.PolycyclicRecognition.fderiv_chart_comp line 52
  5. theorem OAI.PolycyclicRecognition.mfderiv_chart_symm_base line 68
  6. theorem OAI.PolycyclicRecognition.chartVectorField_related line 76
  7. theorem OAI.PolycyclicRecognition.fderiv_chart_comp_base line 96
  8. theorem OAI.PolycyclicRecognition.mfderiv_mlieBracket_of_related line 111