liftHomotopyZeroSucc_comp — Mathlib

English

The level-1 homotopy respects the differential at index 1 with a correction term from level 0.

Русский

Гомотопия уровня 1 совместима с дифференциалом на индексе 1, с поправкой из уровня 0.

LaTeX

$$$liftHomotopyZeroOne(f,comm) ≫ Q.complex.d 2 1 = f.f 1 - P.complex.d 1 0 ≫ liftHomotopyZeroZero(f,comm)$$$

Lean4

@[reassoc (attr := simp)]
theorem liftHomotopyZeroSucc_comp {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z}
    (f : P.complex ⟶ Q.complex) (n : ℕ) (g : P.complex.X n ⟶ Q.complex.X (n + 1))
    (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2))
    (w : f.f (n + 1) = P.complex.d (n + 1) n ≫ g + g' ≫ Q.complex.d (n + 2) (n + 1)) :
    liftHomotopyZeroSucc f n g g' w ≫ Q.complex.d (n + 3) (n + 2) = f.f (n + 2) - P.complex.d _ _ ≫ g' :=
  (Q.exact_succ (n + 1)).liftFromProjective_comp _ _

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