English
Let X be an object of C and I the injective resolution; then F.toRightDerivedZero.app X equals the composite I.toRightDerivedZero' F followed by the canonical maps into homology and the right derived object.
Русский
Пусть X — объект C и I — разрешение; тогда F.toRightDerivedZero.app X равняется композиции I.toRightDerivedZero' F и канонических мап в гомологии и правоеDerived-объект.
LaTeX
$$$F.toRightDerivedZero.app X = I.toRightDerivedZero' F ≫ (\mathrm{CochainComplex.isoHomologyπ_0} ).hom ≫ (I.isoRightDerivedObj F 0).inv$$$
Lean4
theorem toRightDerivedZero_eq {X : C} (I : InjectiveResolution X) (F : C ⥤ D) [F.Additive] :
F.toRightDerivedZero.app X =
I.toRightDerivedZero' F ≫ (CochainComplex.isoHomologyπ₀ _).hom ≫ (I.isoRightDerivedObj F 0).inv :=
by
dsimp [Functor.toRightDerivedZero, isoRightDerivedObj]
have h₁ :=
InjectiveResolution.toRightDerivedZero'_naturality (𝟙 X) (injectiveResolution X) I (desc (𝟙 X) _ _) (by simp) F
simp only [Functor.map_id, id_comp] at h₁
have h₂ :
(I.isoRightDerivedToHomotopyCategoryObj F).hom =
(F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map (desc (𝟙 X) _ _) :=
comp_id _
rw [← cancel_mono ((HomotopyCategory.homologyFunctor _ _ 0).map (I.isoRightDerivedToHomotopyCategoryObj F).hom),
assoc, assoc, assoc, assoc, assoc, ← Functor.map_comp, Iso.inv_hom_id, Functor.map_id, comp_id, reassoc_of% h₁, h₂,
← HomologicalComplex.homologyπ_naturality_assoc]
erw [← NatTrans.naturality]
rfl
