isZero_leftDerived_obj_projective_succ

English

Higher left-derived functors vanish on projective objects: for any X projective and any n, (F.leftDerived (n+1)).obj X is zero.

Русский

Более высокие левые производные исчезают на проективных объектах: для любого проективного X и любого n, (F.leftDerived (n+1)).obj X = 0.

LaTeX

$$$\forall X\ [\text{Projective } X], \forall n, IsZero\left((F.leftDerived (n+1)).\!\!\! .obj X\right).$$$

Lean4

/-- The higher derived functors vanish on projective objects. -/
theorem isZero_leftDerived_obj_projective_succ (F : C ⥤ D) [F.Additive] (n : ℕ) (X : C) [Projective X] :
    IsZero ((F.leftDerived (n + 1)).obj X) :=
  by
  refine IsZero.of_iso ?_ ((ProjectiveResolution.self X).isoLeftDerivedObj F (n + 1))
  erw [← HomologicalComplex.exactAt_iff_isZero_homology]
  exact ShortComplex.exact_of_isZero_X₂ _ (F.map_isZero (by apply isZero_zero))

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