OAI/Algebra/Finitistic/Encoding/RelationVertexSequence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.RelationVertexSequence.arrowFamily line 22
  2. abbrev OAI.LittleFinitistic.RelationVertexSequence.relationFamily line 23
  3. def OAI.LittleFinitistic.RelationVertexSequence.oneSumIso line 25
  4. def OAI.LittleFinitistic.RelationVertexSequence.twoSumIso line 27
  5. theorem OAI.LittleFinitistic.RelationVertexSequence.p_square line 30
  6. theorem OAI.LittleFinitistic.RelationVertexSequence.q_entry line 41
  7. theorem OAI.LittleFinitistic.RelationVertexSequence.q_square line 56
  8. def OAI.LittleFinitistic.RelationVertexSequence.originalSequence line 67
  9. def OAI.LittleFinitistic.RelationVertexSequence.sequenceIso line 69
  10. theorem OAI.LittleFinitistic.RelationVertexSequence.shortExact line 75

    Source documentation

    The original source-zero p/q maps are a short exact relation sequence at the final vertex.

    theorem shortExact : ((originalSequence P D₀ D₁ D₂ f g).map (vertex P)).ShortExact :=
…

    Mentions: OAI.LittleFinitistic.RelationVertexSequence.originalSequence