colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom

English

There is a canonical isomorphism between the colimit over the swapped product and the colimit over the original product, expressing the Fubini-type interchange for colimits

Русский

Существует канонический изоморфизм между колимитой по переставленной произведению и колимитой по исходному произведению, выражающий перестановку Фубини для колимитов

LaTeX

$$$\\text{colimit}\\bigl(\\mathrm{curry.obj}(\\mathrm{Prod.swap } K J \\;\\gg\\; G) \\;\\gg\\; \\mathrm{colim}\\bigr) \\cong \\text{colimit}\\bigl(\\mathrm{curry.obj} G \\gg\\; \\mathrm{colim}\\bigr)$$

Lean4

@[simp]
theorem colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom {j} {k} :
    colimit.ι _ j ≫
        colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
          (colimitCurrySwapCompColimIsoColimitCurryCompColim G).hom =
      (colimit.ι _ k ≫ colimit.ι (curry.obj G ⋙ colim) j : _ ⟶ colimit (curry.obj G ⋙ colim)) :=
  by
  dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
  slice_lhs 1 3 => simp only []
  simp

Похожие утверждения