cokernelToAbelianCoimage

Mathlib.Algebra.Homology.ShortComplex.Abelian

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

Lean4

/-- The canonical morphism `cokernel S.f ⟶ Abelian.coimage S.g` for a short complex `S`
in an abelian category. -/
noncomputable def cokernelToAbelianCoimage : cokernel S.f ⟶ Abelian.coimage S.g :=
  cokernel.desc S.f (Abelian.coimage.π S.g)
    (by simp only [← cancel_mono (Abelian.factorThruCoimage S.g), assoc, cokernel.π_desc, zero, zero_comp])

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

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

Разделы

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

Аффилиация

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