English
The inverse part of the isomorphism between F.leftDerivedToHomotopyCategory.obj X and the mapped resolution is natural in the morphism f: X → Y.
Русский
Обратная часть изоморфизма между F.leftDerivedToHomotopyCategory.obj X и образованной резольюции естественна по морфизму f: X → Y.
LaTeX
$$$\text{inv}: (P.isoLeftDerivedToHomotopyCategoryObj F).inv \circ F.leftDerivedToHomotopyCategory.map f = \cdots$ (naturality in f).$$
Lean4
@[reassoc]
theorem isoLeftDerivedToHomotopyCategoryObj_inv_naturality {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X)
(Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f) (F : C ⥤ D)
[F.Additive] :
(P.isoLeftDerivedToHomotopyCategoryObj F).inv ≫ F.leftDerivedToHomotopyCategory.map f =
(F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map φ ≫
(Q.isoLeftDerivedToHomotopyCategoryObj F).inv :=
by
dsimp [Functor.leftDerivedToHomotopyCategory, isoLeftDerivedToHomotopyCategoryObj]
rw [assoc, ← Functor.map_comp, iso_inv_naturality f P Q φ comm, Functor.map_comp]
erw [(F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.naturality_assoc]
rfl
