English
Assuming HasExactColimitsOfShape J C, the mapShortComplex construction preserves exactness across colimits with domain/source cocones coherently matching the original short complex.
Русский
Полагая HasExactColimitsOfShape J C, конструкция mapShortComplex сохраняет точность при колимитах, если коконы согласованы с исходным коротким комплексом.
LaTeX
$$$\\text{(mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact}$$$
Lean4
/-- Assuming `HasExactColimitsOfShape J C`, this lemma rephrases the exactness
of the functor `colim : (J ⥤ C) ⥤ C` by saying that if `S : ShortComplex (J ⥤ C)`
is exact, then the short complex obtained by taking the colimits is exact,
where we allow the replacement of the chosen colimit cocones of the
colimit API by arbitrary colimit cocones. -/
theorem exact_mapShortComplex : (mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact :=
by
refine (ShortComplex.exact_iff_of_iso ?_).2 (hS.map colim)
refine
ShortComplex.isoMk (IsColimit.coconePointUniqueUpToIso hc₁ (colimit.isColimit _))
(IsColimit.coconePointUniqueUpToIso hc₂ (colimit.isColimit _))
(IsColimit.coconePointUniqueUpToIso hc₃ (colimit.isColimit _)) (hc₁.hom_ext (fun j ↦ ?_))
(hc₂.hom_ext (fun j ↦ ?_))
· dsimp
rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc, colimit.cocone_ι, ι_colimMap, reassoc_of% (hf j),
IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
· dsimp
rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc, colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]
