opcyclesIsCokernel

Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

Lean4

/-- Via `S.pOpcycles : S.X₂ ⟶ S.opcycles`, the object `S.opcycles` identifies to the
cokernel of `S.f : S.X₁ ⟶ S.X₂`. -/
noncomputable def opcyclesIsCokernel : IsColimit (CokernelCofork.ofπ S.pOpcycles S.f_pOpcycles) :=
  S.rightHomologyData.hp

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

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

Разделы

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

Аффилиация

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