homotopyEquiv_hom_π — Mathlib

English

In higher degrees, the lift is compatible with successive differentials up to a boundary term given by g and g'.

Русский

В более высоких степенях лифт совместим с последовательными дифференциалами до граничного терма, заданного g и g'.

LaTeX

$$$liftHomotopyZeroSucc(f,n,g,g',w) ≫ Q.complex.d (n+3)(n+2) = f.f(n+2) - P.complex.d _ _ ≫ g'$$$

Lean4

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

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