lift_commutes — Mathlib

English

The lift map intertwines the differentials: lift f P Q ≫ Q.π = P.π ≫ (ChainComplex.single₀).map f.

Русский

Лифт–отображение взаимно совместимо с дифференциалами: lift f P Q затем Q.π равно P.π затем отображение f на одном компоненте цепного комплекса.

LaTeX

$$$\forall f:P.complex ⟶ Q.complex,\ lift f P Q \,\gg \, Q.\pi = P.\pi \,\gg \, (ChainComplex.single_0).map f$$$

Lean4

/-- The resolution maps intertwine the lift of a morphism and that morphism. -/
@[reassoc (attr := simp)]
theorem lift_commutes {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) :
    lift f P Q ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f :=
  by
  ext
  simp [lift, liftFZero, liftFOne]

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