isColimitImage

Mathlib.CategoryTheory.Abelian.Exact

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

Lean4

/-- If `(f, g)` is exact, then `factorThruImage g` is a cokernel of `f`. -/
def isColimitImage (h : S.Exact) :
    IsColimit (CokernelCofork.ofπ (Limits.factorThruImage S.g) (comp_factorThruImage_eq_zero S.zero)) :=
  IsCokernel.cokernelIso _ _ h.isColimitCoimage (Abelian.coimageIsoImage' S.g) <|
    (cancel_mono (Limits.image.ι S.g)).1 <| by simp

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

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

Разделы

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

Аффилиация

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