homologyMap_eq — Mathlib

English

If two chain maps f and g are homotopic via a homotopy ho, then the induced maps on homology are equal for every degree i; i.e., the homology maps of f and g agree.

Русский

Если два цепных отображения f и g соединены гомотопией ho, то индуцируемые отображения на гомологии совпадают для каждой степени i.

LaTeX

$$$\\operatorname{homologyMap}(f,i) = \\operatorname{homologyMap}(g,i) \\quad \\text{for all } i$$$

Lean4

theorem homologyMap_eq (ho : Homotopy f g) (i : ι) [K.HasHomology i] [L.HasHomology i] :
    homologyMap f i = homologyMap g i :=
  ShortComplex.Homotopy.homologyMap_congr (ho.toShortComplex i)

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