Q_map_eq_of_homotopy — Mathlib

English

If f and g are homotopic, then their images under Q-map coincide: Q.map f = Q.map g when there is a homotopy between f and g.

Русский

Если f и g гомотопны, то их образы под Q-мэппингом совпадают: Q.map f = Q.map g при существовании гомотопии между f и g.

LaTeX

$$$ \operatorname{Homotopy}(f,g) \Rightarrow Q(map\ f) = Q(map\ g). $$$

Lean4

theorem Q_map_eq_of_homotopy {K L : HomologicalComplex C c} {f g : K ⟶ L} (h : Homotopy f g) : Q.map f = Q.map g :=
  (ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization h).map_eq Q

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