OAI/GroupTheory/PolycyclicRecognition/Geometry/AutomaticSmoothAlgebraHom.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Automatic smoothness of continuous homomorphisms into algebra units

Products of one-parameter subgroups supply coordinates of the second kind. The integral argument for continuous algebra-valued one-parameter groups then proves smoothness in those coordinates.

  1. theorem OAI.PolycyclicRecognition.contDiff_comp_exponentialProduct line 24
  2. theorem OAI.PolycyclicRecognition.contMDiffAt_one_of_continuous_unitsHom line 53
  3. theorem OAI.PolycyclicRecognition.contMDiff_of_continuous_unitsHom line 72