English
The equality for the app component of the right-derived natural transformation with respect to a chosen injective resolution follows the established formula.
Русский
Сцепленное равенство компоненты app для правой производной натурального преобразования следует из заданной формулы.
LaTeX
$$$\\text{(app X) of } (\\mathrm{rightDerivedToHomotopyCategory} \\alpha) = \\cdots$$$
Lean4
theorem rightDerivedToHomotopyCategory_app_eq {F G : C ⥤ D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C}
(P : InjectiveResolution X) :
(NatTrans.rightDerivedToHomotopyCategory α).app X =
(P.isoRightDerivedToHomotopyCategoryObj F).hom ≫
(HomotopyCategory.quotient _ _).map ((NatTrans.mapHomologicalComplex α _).app P.cocomplex) ≫
(P.isoRightDerivedToHomotopyCategoryObj G).inv :=
by
rw [← cancel_mono (P.isoRightDerivedToHomotopyCategoryObj G).hom, assoc, assoc, Iso.inv_hom_id, comp_id]
dsimp [isoRightDerivedToHomotopyCategoryObj, Functor.mapHomotopyCategoryFactors,
NatTrans.rightDerivedToHomotopyCategory]
rw [assoc]
erw [id_comp, comp_id]
obtain ⟨β, hβ⟩ := (HomotopyCategory.quotient _ _).map_surjective (iso P).hom
rw [← hβ]
dsimp
simp only [← Functor.map_comp, NatTrans.mapHomologicalComplex_naturality]
rfl
