English
There is an equivalence of categories between the functor category C ⥤ D ⥤ E and the functor category (C × D) ⥤ E, given by currying and uncurrying.
Русский
Существует эквивалентность категорий между функторными категориями C ⥤ D ⥤ E и (C × D) ⥤ E, задаваемая каррированием/раскрещиванием.
LaTeX
$$$ \mathrm{uncurry} : (C \to D \to E) \;\simeq\; (C \times D \to E) \quad \text{with inverse } \mathrm{curry}. $$$
Lean4
/-- The uncurrying functor, taking a functor `C ⥤ (D ⥤ E)` and producing a functor `(C × D) ⥤ E`.
-/
@[simps]
def uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E
where
obj
F :=
{ obj := fun X => (F.obj X.1).obj X.2
map := fun {X} {Y} f => (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2
map_comp := fun f g =>
by
simp only [prod_comp_fst, prod_comp_snd, Functor.map_comp, NatTrans.comp_app, Category.assoc]
slice_lhs 2 3 => rw [← NatTrans.naturality]
rw [Category.assoc] }
map
T :=
{ app := fun X => (T.app X.1).app X.2
naturality := fun X Y f => by
simp only [Category.assoc]
slice_lhs 2 3 => rw [NatTrans.naturality]
slice_lhs 1 2 => rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
rw [Category.assoc] }
