lift_commutes_zero — Mathlib

English

The equality liftFOne f P Q ≫ Q.π.f 0 = P.π.f 0 ≫ f holds, relating the zero-th components.

Русский

Равенство liftFOne f P Q ≫ Q.π.f 0 = P.π.f 0 ≫ f связывает нулевой компонент.

LaTeX

$$$ liftFOne(f,P,Q) \;≫\; Q.\pi.f 0 = P.\pi.f 0 \;≫\; f$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_commutes_zero {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) :
    (lift f P Q).f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f :=
  (HomologicalComplex.congr_hom (lift_commutes f P Q) 0).trans (by simp)

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