English
Let f: K → L be a morphism of bicomplexes. The totalization functor, together with the second index shift by y, interacts naturally with f: the two ways of composing the total map and the shift isomorphisms yield the same morphism on the total complexes. In other words, shifting in the second index commutes with applying f up to the canonical isomorphisms provided by the total shift data.
Русский
Пусть f: K → L — гомоморфизм бикомплексів. Функтор полной фиксации (totalization) вместе с сдвигом по второй переменной на y ведут себя естественно по отношению к f: два способа композиции общего отображения и сдвига через изоморфизмы полной фиксации дают один и тот же морфизм между суммарными комплексами. Иными словами, сдвиг по второй координате коммутирует с приложением f вплоть до канонических изоморфизмов, заданных данными полного сдвига.
LaTeX
$$$\text{total.map} \big((\text{shiftFunctor}_2\ C\ y).map\ f\big) (\text{up}\ \mathbb{Z}) \;\;\; ≡\;\;\; (K.\text{totalShift}_2^y).\text{hom} \; \circ \; \text{total.map}\big(f, (\text{up}\ \mathbb{Z})\big)^{\langle y \rangle'}$$$
Lean4
@[reassoc]
theorem totalShift₂Iso_hom_naturality [L.HasTotal (up ℤ)] :
total.map ((shiftFunctor₂ C y).map f) (up ℤ) ≫ (L.totalShift₂Iso y).hom =
(K.totalShift₂Iso y).hom ≫ (total.map f (up ℤ))⟦y⟧' :=
by
ext n i₁ i₂ h
dsimp at h ⊢
rw [ιTotal_map_assoc, L.ι_totalShift₂Iso_hom_f y i₁ i₂ n h _ rfl _ rfl,
K.ι_totalShift₂Iso_hom_f_assoc y i₁ i₂ n h _ rfl _ rfl]
dsimp
rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul, Linear.units_smul_comp, ιTotal_map]
