OAI/GroupTheory/PolycyclicRecognition/Algebra/TuplePrism.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The simplicial prism on tuples

The universal homogeneous simplex on a set has one simplex for every tuple. Two maps of vertices are joined by the prism that uses the first map before a chosen vertex and the second map afterwards.

  1. def OAI.PolycyclicRecognition.tupleSimplicial line 20
  2. def OAI.PolycyclicRecognition.tupleSimplicialMap line 26
  3. def OAI.PolycyclicRecognition.tuplePrism line 30
  4. theorem OAI.PolycyclicRecognition.tuplePrism_zero line 35
  5. theorem OAI.PolycyclicRecognition.tuplePrism_first_face line 39
  6. theorem OAI.PolycyclicRecognition.tuplePrism_last_face line 44
  7. theorem OAI.PolycyclicRecognition.tupleSuccAbove_val line 49
  8. theorem OAI.PolycyclicRecognition.tuplePredAbove_val line 59
  9. theorem OAI.PolycyclicRecognition.tuplePrism_face_before line 69
  10. theorem OAI.PolycyclicRecognition.tuplePrism_face_middle line 82
  11. theorem OAI.PolycyclicRecognition.tuplePrism_face_after line 92
  12. theorem OAI.PolycyclicRecognition.tuplePrism_degeneracy_before line 105
  13. theorem OAI.PolycyclicRecognition.tuplePrism_degeneracy_after line 118
  14. def OAI.PolycyclicRecognition.tupleSimplicialHomotopy line 132

    Source documentation

    The usual prism is a genuine simplicial homotopy.

    def tupleSimplicialHomotopy (f g : A → B) :
    SimplicialObject.Homotopy (tupleSimplicialMap f) (tupleSimplicialMap g) where
…

    Mentions: OAI.PolycyclicRecognition.tupleSimplicialMap