homologyIsCokernel

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.homologyIsCokernel

Lean4

/-- `K.homology j` is the cokernel of `K.toCycles i j : K.X i ⟶ K.cycles j`
when `c.prev j = i`. -/
noncomputable def homologyIsCokernel (hi : c.prev j = i) [K.HasHomology j] :
    IsColimit (CokernelCofork.ofπ (K.homologyπ j) (K.toCycles_comp_homologyπ i j)) :=
  by
  subst hi
  exact (K.sc j).homologyIsCokernel

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

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

Разделы

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

Аффилиация

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