functorProdFunctorEquivCounitIso — Mathlib

English

Let A, B, C be categories. There is a canonical natural isomorphism from the round-trip functor (functorProdToProdFunctor A B C) ∘ (prodFunctorToFunctorProd A B C) back to the identity functor on the corresponding functor category: (functorProdToProdFunctor A B C) ∘ (prodFunctorToFunctorProd A B C) ≅ Id_{Fun(A, B × C)}.

Русский

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

LaTeX

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

Lean4

/-- The counit isomorphism for `functorProdFunctorEquiv` -/
@[simps!]
def functorProdFunctorEquivCounitIso : functorProdToProdFunctor A B C ⋙ prodFunctorToFunctorProd A B C ≅ 𝟭 _ :=
  NatIso.ofComponents fun F => NatIso.ofComponents fun X => prod.etaIso (F.obj X)

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