compatibilityOfZerosOfIsLimitKernelFork

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

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

← MathLib Explorer

Lean4

/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the left homology map
data (for the identity of `S`) which relates the left homology data
`LeftHomologyData.ofIsLimitKernelFork` and `ofZeros` . -/
@[simps]
def compatibilityOfZerosOfIsLimitKernelFork (hf : S.f = 0) (hg : S.g = 0) (c : KernelFork S.g) (hc : IsLimit c) :
    LeftHomologyMapData (𝟙 S) (LeftHomologyData.ofIsLimitKernelFork S hf c hc) (LeftHomologyData.ofZeros S hf hg)
    where
  φK := c.ι
  φH := c.ι

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

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

Разделы

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

Аффилиация

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