isColimitCoimage

Mathlib.CategoryTheory.Abelian.Exact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.Exact.isColimitCoimage

Lean4

/-- If `(f, g)` is exact, then `Abelian.coimage.π g` is a cokernel of `f`. -/
def isColimitCoimage (h : S.Exact) :
    IsColimit
      (CokernelCofork.ofπ (Abelian.coimage.π S.g) (Abelian.comp_coimage_π_eq_zero S.zero) : CokernelCofork S.f) :=
  by
  rw [exact_iff_kernel_ι_comp_cokernel_π_zero] at h
  refine
    CokernelCofork.IsColimit.ofπ _ _
      (fun u hu => cokernel.desc (kernel.ι S.g) u (by rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]))
      (by simp) ?_
  intro _ _ _ _ hm
  ext
  rw [hm, cokernel.π_desc]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru