OAI/GroupTheory/PolycyclicRecognition/Geometry/LieAdjointSmoothness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smoothness of the actual adjoint action

Conjugation fixes the identity, so its parameter-dependent derivative has constant source and target tangent spaces. The general derivative theorem therefore gives smoothness in the ordinary operator norm.

  1. def OAI.PolycyclicRecognition.adjointLinearMap line 22
  2. theorem OAI.PolycyclicRecognition.contMDiff_conjugationDifferentialHom line 25