functorProdFunctorEquivUnitIso — Mathlib

English

Let A, B, C be categories. There exists a canonical natural isomorphism between the identity endofunctor on the product of functor categories and the round-trip functor obtained by first collecting into a functor to the product and then splitting back into a pair of functors: Id_{Prod(Fun(A,B), Fun(A,C))} ≅ (prodFunctorToFunctorProd A B C) ∘ (functorProdToProdFunctor A B C).

Русский

Пусть A, B, C — категории. Существуют каноническое естественное изоморование между тождественным функтором на произведение категорий функторов и обходной функторной композиции, получаемой сначала объединением в функтор в произведение, а затем разбиением обратно на пару функторов: Id_{Prod(Fun(A,B), Fun(A,C))} ≅ (prodFunctorToFunctorProd A B C) ∘ (functorProdToProdFunctor A B C).

LaTeX

$$$\\operatorname{Id}_{\\mathrm{Prod}(\\mathsf{Fun}(A,B),\\ \\mathsf{Fun}(A,C))} \\cong (\\mathrm{prodFunctorToFunctorProd}\\ A\\ B\\ C) \\circ (\\mathrm{functorProdToProdFunctor}\\ A\\ B\\ C).$$$

Lean4

/-- The unit isomorphism for `functorProdFunctorEquiv` -/
@[simps!]
def functorProdFunctorEquivUnitIso : 𝟭 _ ≅ prodFunctorToFunctorProd A B C ⋙ functorProdToProdFunctor A B C :=
  NatIso.ofComponents fun F =>
    Functor.prod'CompFst F.fst F.snd |>.prod (Functor.prod'CompSnd F.fst F.snd) |>.trans (prod.etaIso F) |>.symm

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