English
The colimit functor preserves homology for diagrams in AddCommGrpCat.
Русский
Колимитный функтор сохраняет гомологию для диаграмм в AddCommGrpCat.
LaTeX
$$$\operatorname{colim.PreservesHomology}$$$
Lean4
noncomputable instance : (colim (J := J) (C := AddCommGrpCat.{u})).PreservesHomology :=
Functor.preservesHomology_of_map_exact _
(fun S hS ↦ by
replace hS := fun j => hS.map ((evaluation _ _).obj j)
simp only [ShortComplex.ab_exact_iff_ker_le_range] at hS ⊢
intro x (hx : _ = _)
dsimp at hx
rcases Concrete.colimit_exists_rep S.X₂ x with ⟨j, y, rfl⟩
rw [← ConcreteCategory.comp_apply, colimMap_eq, colimit.ι_map, ConcreteCategory.comp_apply, ←
map_zero (colimit.ι S.X₃ j).hom] at hx
rcases Concrete.colimit_exists_of_rep_eq.{u, u, u} S.X₃ _ _ hx with ⟨k, e₁, e₂, hk⟩
rw [map_zero, ← ConcreteCategory.comp_apply, ← NatTrans.naturality, ConcreteCategory.comp_apply] at hk
rcases hS k hk with ⟨t, ht⟩
use colimit.ι S.X₁ k t
erw [← ConcreteCategory.comp_apply, colimit.ι_map, ConcreteCategory.comp_apply, ht]
exact colimit.w_apply S.X₂ e₁ y)
