ExtensionColimits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.extensionEvalIso line 15
Source documentation
Evaluation of extension at an index in its image is the original evaluation, naturally on all complexes and chain maps.
```
def extensionEvalIso (i : ι) (j : ι') (h : e.f i=j) :
    e.extendFunctor C ⋙ HomologicalComplex.eval C c' j ≅ HomologicalComplex.eval C c i :=
…
```
theorem OAI.DerivedBar.extensionPreservesColimit line 26
Source documentation
Extension by zero preserves the actual colimit, proved degreewise including the zero degrees. In particular it preserves the count coproduct.
```
theorem extensionPreservesColimit {J : Type z} [Category.{z'} J] [HasColimitsOfShape J C]
    (F : J ⥤ HomologicalComplex C c) : PreservesColimit F (e.extendFunctor C) := by
…
```