liftFOne_zero_comm — Mathlib

English

The lift operation satisfies a commutativity relation with f and the differentials at index 0.

Русский

Операция lift удовлетворяет коммутативному отношению с f и дифференциалами в нулевой позиции.

LaTeX

$$$\forall Y Z f P Q,\ liftFOne(f,P,Q)\;\text{and}\; Q.\!\!\;d_0$ satisfy a certain commutation with $P.\!\!\;d_0$ and $f$$$

Lean4

@[simp]
theorem liftFOne_zero_comm {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y) (Q : ProjectiveResolution Z) :
    liftFOne f P Q ≫ Q.complex.d 1 0 = P.complex.d 1 0 ≫ liftFZero f P Q := by apply Q.exact₀.liftFromProjective_comp

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