OAI/Algebra/Finitistic/Rectification/ConcreteAdjacentGraded.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.ConcreteAdjacentGraded.arrow01Sum line 15
2. def OAI.LittleFinitistic.ConcreteAdjacentGraded.arrow12Sum line 19
3. theorem OAI.LittleFinitistic.ConcreteAdjacentGraded.vertex1_arrow01_isIso line 23
4. theorem OAI.LittleFinitistic.ConcreteAdjacentGraded.vertex2_arrow12_isIso line 35
5. theorem OAI.LittleFinitistic.ConcreteAdjacentGraded.vertex1_cone_acyclic line 48

   Source documentation

   The first adjacent graded cone is acyclic for the actual arrow map.

   theorem vertex1_cone_acyclic :
       (CochainComplex.mappingCone
         ((AdjacentArrowSum.vertexComplex (composition P) 1).map (arrow01Sum P D))).Acyclic := by
   …

   Mentions: OAI.LittleFinitistic.AdjacentArrowSum.vertexComplex, OAI.LittleFinitistic.ConcreteAdjacentGraded.arrow01Sum

6. theorem OAI.LittleFinitistic.ConcreteAdjacentGraded.vertex2_cone_acyclic line 55

   Source documentation

   The second adjacent graded cone is acyclic for the actual arrow map.

   theorem vertex2_cone_acyclic :
       (CochainComplex.mappingCone
         ((AdjacentArrowSum.vertexComplex (composition P) 2).map (arrow12Sum P D))).Acyclic := by
   …

   Mentions: OAI.LittleFinitistic.AdjacentArrowSum.vertexComplex, OAI.LittleFinitistic.ConcreteAdjacentGraded.arrow12Sum