English
As above, the canonical isomorphism (InjectiveResolution.self X).toRightDerivedZero' F is always an isomorphism under the given hypotheses.
Русский
Как и выше, канонический изоморфизм (InjectiveResolution.self X).toRightDerivedZero' F всегда является изоморфизмом при данных предпосылках.
LaTeX
$$IsIso ( (InjectiveResolution.self X).toRightDerivedZero' F )$$
Lean4
/-- The natural transformation `F ⟶ F.rightDerived 0`. -/
noncomputable def toRightDerivedZero (F : C ⥤ D) [F.Additive] : F ⟶ F.rightDerived 0
where
app
X :=
(injectiveResolution X).toRightDerivedZero' F ≫
(CochainComplex.isoHomologyπ₀ _).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app _
naturality {X Y}
f := by
dsimp [rightDerived]
rw [assoc, assoc,
InjectiveResolution.toRightDerivedZero'_naturality_assoc f (injectiveResolution X) (injectiveResolution Y)
(InjectiveResolution.desc f _ _) (by simp),
← HomologicalComplex.homologyπ_naturality_assoc]
erw [← NatTrans.naturality]
rfl
