OAI/GroupTheory/PolycyclicRecognition/Algebra/ControlledPrismIdentity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The controlled prism identity

The identity is inherited from the actual simplicial chain homotopy, after the support estimate has placed every summand in the controlled complex.

  1. theorem OAI.PolycyclicRecognition.controlledLinearExtension_single line 18
  2. def OAI.PolycyclicRecognition.controlledLinearExtensionMap line 23
  3. theorem OAI.PolycyclicRecognition.controlledLinearExtension_injective line 33
  4. theorem OAI.PolycyclicRecognition.tupleChainComplex_boundary_linear line 42
  5. theorem OAI.PolycyclicRecognition.controlledLinearExtension_pullback line 51
  6. theorem OAI.PolycyclicRecognition.controlledLinearExtension_prism line 61