English
Let P be a projective resolution of an object Z. Then the cokernel cofork associated to the map P.complex.X1 → P.complex.X0 is a colimit diagram; equivalently, Z is the cokernel of that map.
Русский
Пусть P — проективное разрешение Z. Тогда кофорк-кофорка, связанная с отображением P.complex.X1 → P.complex.X0, образует колимит; эквивалентно, Z является cokernel этого отображения.
LaTeX
$$$IsColimit\bigl(P.cokernelCofork\bigr)$$
Lean4
/-- `Z` is the cokernel of `P.complex.X 1 ⟶ P.complex.X 0` when `P : ProjectiveResolution Z`. -/
noncomputable def isColimitCokernelCofork : IsColimit (P.cokernelCofork) :=
by
refine IsColimit.ofIsoColimit (P.complex.opcyclesIsCokernel 1 0 (by simp)) ?_
refine Cofork.ext (P.complex.isoHomologyι₀.symm ≪≫ isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso _ _ _) ?_
rw [← cancel_mono (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 _).inv, ← cancel_mono (isoHomologyι₀ _).hom]
dsimp
simp only [isoHomologyι₀_inv_naturality_assoc, p_opcyclesMap_assoc, single₀_obj_zero, assoc, Iso.hom_inv_id, comp_id,
isoHomologyι_inv_hom_id, singleObjHomologySelfIso_inv_homologyι, singleObjOpcyclesSelfIso_hom, single₀ObjXSelf,
Iso.refl_inv, id_comp]
