English
Equivalence respects composition of SmallShiftedHom: equiv_W L (f.comp g h) equals (equiv_W L f).comp (equiv_W L g) h.
Русский
Эквивалентность сохраняет композицию SmallShiftedHom: equiv_W L (f.comp g h) = (equiv_W L f).comp (equiv_W L g) h.
LaTeX
$$$\mathrm{equiv}\,W\,L\big( f.\mathrm{comp}\ g\ h \big) = (\mathrm{equiv}\,W\,L f).\mathrm{comp}\ (\mathrm{equiv}\,W\,L g)\ h$$$
Lean4
theorem equiv_comp [HasSmallLocalizedShiftedHom.{w} W M X Y] [HasSmallLocalizedShiftedHom.{w} W M Y Z]
[HasSmallLocalizedShiftedHom.{w} W M X Z] [HasSmallLocalizedShiftedHom.{w} W M Z Z] {a b c : M}
(f : SmallShiftedHom.{w} W X Y a) (g : SmallShiftedHom.{w} W Y Z b) (h : b + a = c) :
equiv W L (f.comp g h) = (equiv W L f).comp (equiv W L g) h :=
by
dsimp [comp, equiv, ShiftedHom.comp]
erw [Iso.homToEquiv_apply, Iso.homToEquiv_apply, Iso.homToEquiv_apply, SmallHom.equiv_comp]
simp only [equiv_shift', Functor.comp_obj, Iso.app_hom, assoc, Iso.inv_hom_id_app, comp_id, Functor.map_comp]
rfl
