OAI/GroupTheory/PolycyclicRecognition/Analysis/TupleChainPrism.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The prism on free homogeneous chains

Linearization of the tuple homotopy gives the chain homotopy. The formulas below identify its components with the alternating prism and boundary.

  1. def OAI.PolycyclicRecognition.tupleFreeSimplicial line 19
  2. def OAI.PolycyclicRecognition.tupleChainComplex line 22
  3. def OAI.PolycyclicRecognition.tupleChainMap line 25
  4. def OAI.PolycyclicRecognition.tupleChainPrism line 30
  5. theorem OAI.PolycyclicRecognition.tupleChainMap_single line 33
  6. theorem OAI.PolycyclicRecognition.tupleChainComplex_boundary line 40
  7. theorem OAI.PolycyclicRecognition.tupleChainPrism_single line 50