English
The construction of the assignment X ↦ (injectiveResolution X).cocomplex is functorial up to homotopy, giving a functor to the homotopy category.
Русский
Построение резолюций инъективных резолюций задаёт функторность в гомотопической категории.
LaTeX
$$injectiveResolutions : C ⥤ HomotopyCategory C (ComplexShape.up ℕ)$$
Lean4
/-- Taking injective resolutions is functorial,
if considered with target the homotopy category
(`ℕ`-indexed cochain complexes and chain maps up to homotopy).
-/
def injectiveResolutions : C ⥤ HomotopyCategory C (ComplexShape.up ℕ)
where
obj X := (HomotopyCategory.quotient _ _).obj (injectiveResolution X).cocomplex
map f := (HomotopyCategory.quotient _ _).map (InjectiveResolution.desc f _ _)
map_id
X := by
rw [← (HomotopyCategory.quotient _ _).map_id]
apply HomotopyCategory.eq_of_homotopy
apply InjectiveResolution.descIdHomotopy
map_comp f
g := by
rw [← (HomotopyCategory.quotient _ _).map_comp]
apply HomotopyCategory.eq_of_homotopy
apply InjectiveResolution.descCompHomotopy
