OAI/GroupTheory/PolycyclicRecognition/Geometry/SemidirectIntegration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating a codimension-one semidirect product

An equivariant homomorphism on the ideal and the complementary exponential curve give the required homomorphism, with its actual manifold derivative.

  1. def OAI.PolycyclicRecognition.derivationSemidirectHom line 28
  2. theorem OAI.PolycyclicRecognition.derivationSemidirectHom_apply line 50
  3. theorem OAI.PolycyclicRecognition.contMDiff_derivationSemidirectHom line 53
  4. theorem OAI.PolycyclicRecognition.hasMFDerivAt_derivationSemidirectHom line 60