homologyMap_comp — Mathlib

English

The homology map is compatible with composition: the homology map of a composition equals the composition of the homology maps.

Русский

Гомологическое отображение сохраняет композицию: отображение гомологии композиции равно композиции отображений гомологии.

LaTeX

$$$\operatorname{homologyMap}(\varphi \circ \psi) i = \operatorname{homologyMap}(\varphi) i \\circ \, \operatorname{homologyMap}(\psi) i$$$

Lean4

@[reassoc]
theorem homologyMap_comp : homologyMap (φ ≫ ψ) i = homologyMap φ i ≫ homologyMap ψ i :=
  by
  dsimp [homologyMap]
  rw [Functor.map_comp, ShortComplex.homologyMap_comp]

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