English
Let F, G, H be additive functors between categories, with natural transformations α: F → G and β: G → H. Then the induced map on the homotopy category preserves composition, i.e. mapHomotopyCategory(α ∘ β) = mapHomotopyCategory(α) ∘ mapHomotopyCategory(β).
Русский
Пусть F, G, H — аддитивные функторы между категориями, α: F → G и β: G → H — натуральные отображения. Тогда полученная карта между гомотопическими категориями сохраняет композицию: mapHomotopyCategory(α ∘ β) = mapHomotopyCategory(α) ∘ mapHomotopyCategory(β).
LaTeX
$$$\\operatorname{mapHomotopyCategory}(\\alpha \\circ \\beta) = \\operatorname{mapHomotopyCategory}(\\alpha) \\circ \\operatorname{mapHomotopyCategory}(\\beta).$$$
Lean4
@[simp]
theorem mapHomotopyCategory_comp (c : ComplexShape ι) {F G H : V ⥤ W} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G)
(β : G ⟶ H) :
NatTrans.mapHomotopyCategory (α ≫ β) c = NatTrans.mapHomotopyCategory α c ≫ NatTrans.mapHomotopyCategory β c := by
cat_disch
