English
There is an equality expressing F.fromLeftDerivedZero.app X equals the composition through isoLeftDerivedObj and fromLeftDerivedZero'.
Русский
Существует равенство, выражающее F.fromLeftDerivedZero.app X через композицию через isoLeftDerivedObj и fromLeftDerivedZero'.
LaTeX
$$$ F.fromLeftDerivedZero.app X = (P.isoLeftDerivedObj F 0).hom \circ (ChainComplex.isoHomologyι₀ _) .hom \circ P.fromLeftDerivedZero' F$$$
Lean4
/-- The natural transformation `F.leftDerived 0 ⟶ F`. -/
noncomputable def fromLeftDerivedZero (F : C ⥤ D) [F.Additive] : F.leftDerived 0 ⟶ F
where
app
X :=
(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app _ ≫
(ChainComplex.isoHomologyι₀ _).hom ≫ (projectiveResolution X).fromLeftDerivedZero' F
naturality {X Y}
f := by
dsimp [leftDerived]
rw [assoc, assoc, ←
ProjectiveResolution.fromLeftDerivedZero'_naturality f (projectiveResolution X) (projectiveResolution Y)
(ProjectiveResolution.lift f _ _) (by simp),
← HomologicalComplex.homologyι_naturality_assoc]
erw [← NatTrans.naturality_assoc]
rfl
