functorProdFunctorEquiv — Mathlib

English

There is an equivalence of categories between the product of functor categories (A ⥤ B) × (A ⥤ C) and the functor category A ⥤ (B × C).

Русский

Существует эквивалентность категорий между произведением категорий функторов (A ⥤ B) × (A ⥤ C) и категорией функторов A ⥤ (B × C).

LaTeX

$$$ (\\mathsf{Fun}(A,B) \\times \\mathsf{Fun}(A,C)) \\simeq \\mathsf{Fun}(A, B \\times C) $$$

Lean4

/-- The equivalence of categories between `(A ⥤ B) × (A ⥤ C)` and `A ⥤ (B × C)` -/
@[simps]
def functorProdFunctorEquiv : (A ⥤ B) × (A ⥤ C) ≌ A ⥤ B × C :=
  { functor := prodFunctorToFunctorProd A B C, inverse := functorProdToProdFunctor A B C,
    unitIso := functorProdFunctorEquivUnitIso A B C, counitIso := functorProdFunctorEquivCounitIso A B C, }

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