prodFunctorToFunctorProd — Mathlib

English

The forward direction for the equivalence between functor product and product of functors: (A ⥤ B) × (A ⥤ C) ⥤ A ⥤ B × C is given by F ↦ (F.1.prod' F.2).

Русский

Прямая часть эквивалентности между произведением функторов и функтором-произведением: (A ⥤ B) × (A ⥤ C) ⥤ A ⥤ B × C задана F ↦ (F.1.prod' F.2).

LaTeX

$$$\\mathrm{prodFunctorToFunctorProd}: (A \\to B) \\times (A \\to C) \\to A \\to B \\times C$ with $\\mathrm{obj}F = F_1 \\mathrm{prod}' F_2$ and $\\mathrm{map}\\;\\alpha = \\mathrm{NatTrans.prod}'(\\alpha_1, \\alpha_2)$.$$

Lean4

/-- The forward direction for `functorProdFunctorEquiv` -/
@[simps]
def prodFunctorToFunctorProd : (A ⥤ B) × (A ⥤ C) ⥤ A ⥤ B × C
    where
  obj F := F.1.prod' F.2
  map {F G} f := NatTrans.prod' f.1 f.2

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