English
A fundamental associativity relation holds among shifted inverses in ShiftMkCore; the two different ways of regrouping correspond to the same morphism after applying the appropriate associator.
Русский
Существует базовая ассоциативность между смещёнными обратными морморфизмами в ShiftMkCore; два способа перегруппировки дают один и тот же морфизм после применения ассоциатора.
LaTeX
$$$(h.F\\,m_3).map((h.add\\,m_1,m_2)^{-1}.app\\,X)\\;\\gg\\;(h.add\\,(m_1+m_2),m_3)^{-1}.app\\,X = (h.add\\,m_2,m_3)^{-1}.app\\,(h.F\\,m_1).obj X \\,\\gg\\; (h.add\\,m_1,(m_2+m_3))^{-1}.app\\,X \\,\\gg\\; \\mathrm{eqToHom}(...)$$$
Lean4
@[reassoc]
theorem assoc_inv_app (h : ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C) :
(h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ (h.add (m₁ + m₂) m₃).inv.app X =
(h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₁ (m₂ + m₃)).inv.app X ≫ eqToHom (by rw [add_assoc]) :=
by
rw [← cancel_mono ((h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)), Category.assoc,
Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id,
h.assoc_hom_app, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
rfl
