liftHomotopyZeroZero_comp — Mathlib

English

Naturality with respect to inverses of isomorphisms in projective resolutions.

Русский

Натурализм относительно обратных изоморфизмов в разрешениях проективных.

LaTeX

$$$\forall X,Y, f, P,Q, (comm : (P.iso.inv) ≫ (projectiveResolutions C).map f = ...)$$$

Lean4

@[reassoc (attr := simp)]
theorem liftHomotopyZeroZero_comp {Y Z : C} {P : ProjectiveResolution Y} {Q : ProjectiveResolution Z}
    (f : P.complex ⟶ Q.complex) (comm : f ≫ Q.π = 0) : liftHomotopyZeroZero f comm ≫ Q.complex.d 1 0 = f.f 0 :=
  Q.exact₀.liftFromProjective_comp _ _

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