leftDerivedZeroIsoSelf_inv_hom_id_app

English

For any projective resolution P of X, the morphism P.fromLeftDerivedZero' F is an isomorphism.

Русский

Для любого проектируемого разрешения P(X) отображение P.fromLeftDerivedZero' F является изоморфизмом.

LaTeX

$$$\\forall P,\\ \\operatorname{IsIso}(P.fromLeftDerivedZero'\\, F)$$$

Lean4

@[reassoc (attr := simp)]
theorem leftDerivedZeroIsoSelf_inv_hom_id_app (X : C) :
    F.leftDerivedZeroIsoSelf.inv.app X ≫ F.fromLeftDerivedZero.app X = 𝟙 _ :=
  F.leftDerivedZeroIsoSelf.inv_hom_id_app X

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