cokernelCofork

Mathlib.Algebra.Homology.Embedding.ExtendHomology

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.extend.leftHomologyData.cokernelCofork

Lean4

/-- Auxiliary definition for `extend.leftHomologyData`. -/
noncomputable def cokernelCofork :
    CokernelCofork
      ((isLimitKernelFork K e hj' hk hk' cone hcone).lift (KernelFork.ofι ((K.extend e).d i' j') (d_comp_d _ _ _ _))) :=
  CokernelCofork.ofπ cocone.π
    (by
      rw [← lift_d_comp_eq_zero_iff K e hj' hi hi' hk hk' cone hcone]
      exact cocone.condition)

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

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

Разделы

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

Аффилиация

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