compatibilityOfZerosOfIsColimitCokernelCofork

Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

← MathLib Explorer

Lean4

/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the right homology map
data (for the identity of `S`) which relates the right homology data `ofZeros` and
`ofIsColimitCokernelCofork`. -/
@[simps]
def compatibilityOfZerosOfIsColimitCokernelCofork (hf : S.f = 0) (hg : S.g = 0) (c : CokernelCofork S.f)
    (hc : IsColimit c) :
    RightHomologyMapData (𝟙 S) (RightHomologyData.ofZeros S hf hg)
      (RightHomologyData.ofIsColimitCokernelCofork S hg c hc)
    where
  φQ := c.π
  φH := c.π

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

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

Разделы

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

Аффилиация

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