English
A proof sketch for the shift sequence in the opposite setting respecting the Additive structure.
Русский
Краткое доказательство для последовательности сдвигов в противоположной обстановке с учётом аддитивной структуры.
LaTeX
$$$\\text{proof of ShiftSequenceOppositeAddCommGrpCatObj}$$$
Lean4
noncomputable instance (B : C) : (preadditiveYoneda.obj B).ShiftSequence ℤ
where
sequence n := preadditiveYoneda.obj (B⟦n⟧)
isoZero := preadditiveYoneda.mapIso ((shiftFunctorZero C ℤ).app B)
shiftIso n a a'
h :=
NatIso.ofComponents
(fun A ↦
AddEquiv.toAddCommGrpIso
{ toEquiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' h).symm
map_add' := fun _ _ ↦ ShiftedHom.opEquiv'_symm_add _ _ _ h })
(by intros; ext; apply ShiftedHom.opEquiv'_symm_comp _ _ _ h)
shiftIso_zero a := by ext; apply ShiftedHom.opEquiv'_zero_add_symm
shiftIso_add n m a a' a'' ha'
ha'' := by
ext _ x
exact ShiftedHom.opEquiv'_add_symm n m a a' a'' ha' ha'' x.op
