OAI/Geometry/NilpotentCharts/Adjoint.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The adjoint action and nilpotence from differentiated group commutators.

  1. def OAI.RawLieAdjoint.derivative line 19
  2. lemma OAI.RawLieAdjoint.mul_derivative_one line 21
  3. lemma OAI.RawLieAdjoint.product_derivative_one line 55
  4. lemma OAI.RawLieAdjoint.inv_derivative_one line 71
  5. lemma OAI.RawLieAdjoint.derivative_comp_one line 88
  6. def OAI.RawLieAdjoint.commMap line 99
  7. lemma OAI.RawLieAdjoint.commMap_one line 102
  8. lemma OAI.RawLieAdjoint.commMap_smooth line 104
  9. def OAI.RawLieAdjoint.iterComm line 110
  10. lemma OAI.RawLieAdjoint.iterComm_one line 115
  11. lemma OAI.RawLieAdjoint.iterComm_smooth line 120
  12. lemma OAI.RawLieAdjoint.iterComm_mem line 126
  13. lemma OAI.RawLieAdjoint.iterComm_derivative line 132
  14. lemma OAI.RawLieAdjoint.nilpotent_mixed_derivative line 143
  15. lemma OAI.RawLieAdjoint.exists_common_kernel line 156
  16. lemma OAI.RawLieAdjoint.conjugation_smooth line 176
  17. def OAI.RawLieAdjoint.adjoint line 180
  18. lemma OAI.RawLieAdjoint.commMap_add_adjoint line 182
  19. theorem OAI.RawLieAdjoint.exists_commutator_kernel line 196
  20. theorem OAI.RawLieAdjoint.exists_adjoint_fixed line 204