OAI/Algebra/Finitistic/Rectification/ZeroLastColumn.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.ZeroLastColumn.coneIso line 12
2. def OAI.LittleFinitistic.ZeroLastColumn.mappedTotalIso line 28

   Source documentation

   Taking an additive image that kills the relation column leaves precisely the ordinary cone.

   def mappedTotalIso (h₂ : IsZero ((F.mapHomologicalComplex (.up ℤ)).obj L₂)) :
       (F.mapHomologicalComplex (.up ℤ)).obj (total p q h) ≅
         mappingCone ((F.mapHomologicalComplex (.up ℤ)).map p) := by
   …