toRightDerivedZero'_comp_iCycles — Mathlib

English

Let X be an object of an abelian category C with an injective resolution P of X and F a additive functor to D. Then the composition of P.toRightDerivedZero' F with the iCycles map is equal to F applied to the 0th component of P.

Русский

Пусть X — объект абелевой категории C, P — разрешение инъективности X, и F — аддитивная функция в D. Тогда композиция P.toRightDerivedZero' F с iCycles равна применению F к нулевому компоненту P.

LaTeX

$$$P.toRightDerivedZero' F ≫ \operatorname{HomologicalComplex.iCycles} \_\_ = F.map (P.ι.f 0)$$$

Lean4

@[reassoc (attr := simp)]
theorem toRightDerivedZero'_comp_iCycles {C} [Category C] [Abelian C] {X : C} (P : InjectiveResolution X) (F : C ⥤ D)
    [F.Additive] : P.toRightDerivedZero' F ≫ HomologicalComplex.iCycles _ _ = F.map (P.ι.f 0) := by
  simp [toRightDerivedZero']

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