isColimitCokernelCofork

Mathlib.Algebra.Homology.Embedding.ExtendHomology

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork

Lean4

/-- The colimit cokernel cofork of `(K.extend e).d i' j'` that is deduced from a
colimit cokernel cofork of `K.d i j`. -/
noncomputable def isColimitCokernelCofork : IsColimit (cokernelCofork K e hj' hi hi' cocone) :=
  CokernelCofork.isColimitOfIsColimitOfIff hcocone ((K.extend e).d i' j') (extendXIso K e hj')
    (d_comp_eq_zero_iff K e hj' hi hi')

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

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

Разделы

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

Аффилиация

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