compatibilityOfZerosOfIsLimitKernelFork

Lean4

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

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