isZero_rightDerived_obj_injective_succ

English

Higher right-derived functors vanish on injective objects: if X is injective, then R^{n+1}(F)(X) = 0 for all n.

Русский

Высшие правые производные на инъективных объектах равны нулю: если X инъективно, то R^{n+1}(F)(X)=0 для всех n.

LaTeX

$$$\\mathrm{IsZero}\\left((F.rightDerived (n+1)).obj X\\right)$ for injective X$$

Lean4

/-- The higher derived functors vanish on injective objects. -/
theorem isZero_rightDerived_obj_injective_succ (F : C ⥤ D) [F.Additive] (n : ℕ) (X : C) [Injective X] :
    IsZero ((F.rightDerived (n + 1)).obj X) :=
  by
  refine IsZero.of_iso ?_ ((InjectiveResolution.self X).isoRightDerivedObj F (n + 1))
  erw [← HomologicalComplex.exactAt_iff_isZero_homology]
  exact ShortComplex.exact_of_isZero_X₂ _ (F.map_isZero (by apply isZero_zero))

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