homologyMap_comp — Mathlib

English

homologyMap(φ1 ≫ φ2) = homologyMap φ1 ≫ homologyMap φ2 under HasHomology assumptions.

Русский

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

LaTeX

$$$\mathrm{homologyMap}(φ_1 \;≫\; φ_2) = \mathrm{homologyMap}(φ_1) \; \circ \mathrm{homologyMap}(φ_2)$$$

Lean4

@[simp]
theorem homologyMap_comp [HasHomology S₁] [HasHomology S₂] [HasHomology S₃] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) :
    homologyMap (φ₁ ≫ φ₂) = homologyMap φ₁ ≫ homologyMap φ₂ :=
  homologyMap'_comp _ _ _ _ _

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