English
Naturality of the totalShift1Iso_hom with respect to a morphism f: K → L: total.map f ≫ (L.totalShift1Iso).hom = (K.totalShift1Iso).hom ≫ total.map f⟦x⟧' .
Русский
Естественность totalShift1Iso_hom по отношению к морфизму f: K → L: total.map f ≫ (L.totalShift1Iso).hom = (K.totalShift1Iso).hom ≫ total.map f⟦x⟧'.
LaTeX
$$$\\text{totalShift}_1\\text{Iso}_\\text{hom\_naturality} : \\; total.map ((shiftFunctor_1\\ C\\ x).map f) (up \\mathbb{Z}) ≫ (L.totalShift_1^\\mathrm{Iso} x).\\mathrm{hom} = (K.totalShift_1^\\mathrm{Iso} x).\\mathrm{hom} ≫ (total.map f (up \\mathbb{Z}))⟦x⟧'$$$
Lean4
@[reassoc]
theorem totalShift₁Iso_hom_naturality [L.HasTotal (up ℤ)] :
total.map ((shiftFunctor₁ C x).map f) (up ℤ) ≫ (L.totalShift₁Iso x).hom =
(K.totalShift₁Iso x).hom ≫ (total.map f (up ℤ))⟦x⟧' :=
by
ext n i₁ i₂ h
dsimp at h ⊢
rw [ιTotal_map_assoc, L.ι_totalShift₁Iso_hom_f x i₁ i₂ n h _ rfl _ rfl,
K.ι_totalShift₁Iso_hom_f_assoc x i₁ i₂ n h _ rfl _ rfl]
dsimp
rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]
