colimitLimitToLimitColimit — Mathlib

English

A specialized variant: for functor F: Prod J K → Type v, the limit projection at j matches the colimit's structure.

Русский

Специальный вариант: для F: Prod J K → Type v предельная проекция на j совпадает с структурой колимита.

LaTeX

$$$\\text{ι_colimitLimitToLimitColimit}(F) = \\dots$ (specialized form)$$

Lean4

/-- The universal morphism
$\colim_k \lim_j F(j,k) → \lim_j \colim_k F(j, k)$.
-/
noncomputable def colimitLimitToLimitColimit :
    colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) ⟶ limit (curry.obj F ⋙ colim) :=
  limit.lift (curry.obj F ⋙ colim)
    { pt := _
      π :=
        { app := fun j =>
            colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
              { pt := _
                ι :=
                  { app := fun k =>
                      limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k
                    naturality := by
                      intro k k' f
                      simp only [Functor.comp_obj, lim_obj, colimit.cocone_x, Functor.const_obj_obj, Functor.comp_map,
                        lim_map, curry_obj_obj_obj, Prod.swap_obj, limMap_π_assoc, curry_obj_map_app, Prod.swap_map,
                        Functor.const_obj_map, Category.comp_id]
                      rw [map_id_left_eq_curry_map, colimit.w] } }
          naturality := by
            intro j j' f
            dsimp
            ext k
            simp only [Functor.comp_obj, lim_obj, Category.id_comp, colimit.ι_desc, colimit.ι_desc_assoc,
              Category.assoc, ι_colimMap, curry_obj_obj_obj, curry_obj_map_app]
            rw [map_id_right_eq_curry_swap_map, limit.w_assoc] } }

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