English
The instance asserting that M.freeYonedaCoproductsCokernelCofork is a colimit in the relevant diagram, i.e., the cokernel cofork is the colimit of the presentation of M by free Yoneda coproducts.
Русский
Экземпляр утверждает, что M.freeYonedaCoproductsCokernelCofork является колимитом в соответствующей диаграмме, то есть кокernel-кофорка выступает как колимит предствления M через свободные coproduct Yoneda.
LaTeX
$$IsColimit (M.freeYonedaCoproductsCokernelCofork)$$
Lean4
/-- If `M` is a presheaf of modules, the cokernel cofork
`M.freeYonedaCoproductsCokernelCofork` is a colimit, which means that
`M` can be expressed as a cokernel of the morphism `M.toFreeYonedaCoproduct`
between coproducts of free presheaves of modules on Yoneda presheaves. -/
noncomputable def isColimitFreeYonedaCoproductsCokernelCofork : IsColimit M.freeYonedaCoproductsCokernelCofork :=
by
let S := ShortComplex.mk _ _ M.toFreeYonedaCoproduct_fromFreeYonedaCoproduct
let T := ShortComplex.mk _ _ (kernel.condition M.fromFreeYonedaCoproduct)
let φ : S ⟶ T :=
{ τ₁ := fromFreeYonedaCoproduct _
τ₂ := 𝟙 _
τ₃ := 𝟙 _ }
exact ((ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).2 (T.exact_of_f_is_kernel (kernelIsKernel _))).gIsCokernel
