OAI/GroupTheory/PolycyclicRecognition/Algebra/AlternatingProductSubmersion.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Submersion of an alternating product from two linear images

If generators in the union of two images bracket-generate the limiting algebra, one fixed alternating product has a surjective differential. Identity factors pad the unused side of each generator slot. The rank is proved for the full product map, before restricting any parameters.

  1. def OAI.PolycyclicRecognition.alternatingCoordinateProduct line 21
  2. theorem OAI.PolycyclicRecognition.contDiff_alternatingCoordinateProduct line 27
  3. def OAI.PolycyclicRecognition.generatorPair line 36
  4. def OAI.PolycyclicRecognition.generatorPairParameters line 39
  5. theorem OAI.PolycyclicRecognition.alternatingCoordinateProduct_generatorPairParameters line 46
  6. theorem OAI.PolycyclicRecognition.exists_submersive_alternatingCoordinateProduct line 70