English
When the target group is zero, a shift iso-homap equals the zero morphism, reflecting the vanishing shift in zero cases.
Русский
Если цель нулевая, гом-апп изоморфии сдвига становится нулевым морфизмом.
LaTeX
$$$(F.shiftIso h).hom.app X = 0$ при нулевом контексте, соответствующем равенству нуля в группе M$$$
Lean4
/-- If `f : X ⟶ Y⟦m⟧`, `n + m = 0` and `ha' : m + a = a'`, this lemma relates the two
morphisms `F.shiftMap f a a' ha'` and `(F.shift a').map (f⟦n⟧')`. Indeed,
via canonical isomorphisms, they both identify to morphisms
`(F.shift a).obj X ⟶ (F.shift a').obj Y`.
-/
theorem shiftIso_hom_app_comp_shiftMap_of_add_eq_zero [F.ShiftSequence G] {X Y : C} {m : G} (f : X ⟶ Y⟦m⟧) (n : G)
(hnm : n + m = 0) (a a' : G) (ha' : m + a = a') :
(F.shiftIso n a' a (by rw [← ha', ← add_assoc, hnm, zero_add])).hom.app X ≫ F.shiftMap f a a' ha' =
(F.shift a').map
(f⟦n⟧' ≫
(shiftFunctorCompIsoId C m n (by rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero])).hom.app Y) :=
by
have hnm' : m + n = 0 := by rw [← add_left_inj m, add_assoc, hnm, zero_add, add_zero]
simp [F.shiftIso_hom_app_comp_shiftMap f n 0 hnm' a' a, shiftIso_zero_hom_app, shiftFunctorCompIsoId]
