English
The equation relating fromLeftDerivedZero' and the mapped chain components holds as stated.
Русский
Утверждение, связывающее fromLeftDerivedZero' и отображения в отображении мономных компонентов удовлетворяет условию.
LaTeX
$$$ F.fromLeftDerivedZero.app X = (P.isoLeftDerivedObj F 0).hom \circ (ChainComplex.isoHomologyι₀ _) .hom \circ P.fromLeftDerivedZero' F $$$
Lean4
theorem fromLeftDerivedZero_eq {X : C} (P : ProjectiveResolution X) (F : C ⥤ D) [F.Additive] :
F.fromLeftDerivedZero.app X =
(P.isoLeftDerivedObj F 0).hom ≫ (ChainComplex.isoHomologyι₀ _).hom ≫ P.fromLeftDerivedZero' F :=
by
dsimp [Functor.fromLeftDerivedZero, isoLeftDerivedObj]
have h₁ :=
ProjectiveResolution.fromLeftDerivedZero'_naturality (𝟙 X) P (projectiveResolution X) (lift (𝟙 X) _ _) (by simp) F
have h₂ :
(P.isoLeftDerivedToHomotopyCategoryObj F).inv =
(F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map (lift (𝟙 X) _ _) :=
id_comp _
simp only [Functor.map_id, comp_id] at h₁
rw [assoc, ← cancel_epi ((HomotopyCategory.homologyFunctor _ _ 0).map (P.isoLeftDerivedToHomotopyCategoryObj F).inv),
← Functor.map_comp_assoc, Iso.inv_hom_id, Functor.map_id, id_comp, ← h₁, h₂, ←
HomologicalComplex.homologyι_naturality_assoc]
erw [← NatTrans.naturality_assoc]
rfl
