homotopyEquiv_inv_π — Mathlib

English

The homotopy equivalence between resolutions intertwines the first projection with the connecting morphism π.

Русский

Гомотопическое эквивалент между разрешениями переплетает первую проекцию с сопряженным отображением π.

LaTeX

$$$(homotopyEquiv P Q).hom ≫ Q.π = P.π$$$

Lean4

@[reassoc (attr := simp)]
theorem homotopyEquiv_inv_π {X : C} (P Q : ProjectiveResolution X) : (homotopyEquiv P Q).inv ≫ P.π = Q.π := by
  simp [homotopyEquiv]

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