instPreservesColimitsOfShapeSingle

English

An instance asserting that the shape J preserves colimits for the single complex HomologicalComplex C c i.

Русский

Экземпляр, утверждающий, что форма J сохраняет колимиты для единственного комплекса HomologicalComplex C c i.

LaTeX

$$$ \mathrm{PreservesColimitsOfShape}(J, \mathrm{HomologicalComplex.single}(C,c,i)) $$$

Lean4

noncomputable instance : PreservesColimitsOfShape J (single C c i) :=
  preservesColimitsOfShape_of_eval _
    (fun j => by
      by_cases h : j = i
      · subst h
        exact preservesColimitsOfShape_of_natIso (singleCompEvalIsoSelf C c j).symm
      · exact Functor.preservesColimitsOfShape_of_isZero _ (isZero_single_comp_eval C c _ _ h) _)

Похожие утверждения