English
The equivalence of categories between C ⥤ D ⥤ E and C × D ⥤ E is given by currying and uncurry with unit/counit isomorphisms; in particular, uncurry is an equivalence with inverse curry.
Русский
Эквивалентность категорий между C ⥤ D ⥤ E и C × D ⥤ E задаётся каррированием и раскрещиванием с тождественными дугами; в частности, uncurry является эквивалентностью с обратной curry.
LaTeX
$$$ \mathrm{uncurry} \dashv \mathrm{curry} \quad \text{and} \quad \mathrm{uncurry} \circ \mathrm{curry} \simeq \mathrm{Id}, \quad \mathrm{curry} \circ \mathrm{uncurry} \simeq \mathrm{Id}. $$$
Lean4
/-- The equivalence of functor categories given by currying/uncurrying.
-/
@[simps!]
def currying : C ⥤ D ⥤ E ≌ C × D ⥤ E where
functor := uncurry
inverse := curry
unitIso := NatIso.ofComponents (fun _ ↦ NatIso.ofComponents (fun _ ↦ NatIso.ofComponents (fun _ ↦ Iso.refl _)))
counitIso :=
NatIso.ofComponents
(fun F ↦
NatIso.ofComponents (fun _ ↦ Iso.refl _)
(by
rintro ⟨X₁, X₂⟩ ⟨Y₁, Y₂⟩ ⟨f₁, f₂⟩
dsimp at f₁ f₂ ⊢
simp only [← F.map_comp, prod_comp, Category.comp_id, Category.id_comp]))
