prodFunctor — Mathlib

English

The Cartesian product functor between functor categories: (A ⥤ B) × (C ⥤ D) ⥤ (Prod A C) ⥤ Prod B D, sending (F,G) to F.prod G.

Русский

Декартово произведение функторов: (A ⥤ B) × (C ⥤ D) ⥤ (A×C) ⥤ (B×D), переводя пары (F,G) в F.prod G.

LaTeX

$$$\\mathrm{prodFunctor}: (A \\to B) \\times (C \\to D) \\to \\mathrm{Functor}(A\\times C, B\\times D)$ defined by $\\mathrm{obj}(F,G) = F.obj \\times G.obj$, $\\mathrm{map}(\\alpha,\\beta) = \\mathrm{NatTrans.prod}(\\alpha,\\beta)$.$$

Lean4

/-- The Cartesian product functor between functor categories -/
@[simps]
def prodFunctor : (A ⥤ B) × (C ⥤ D) ⥤ A × C ⥤ B × D
    where
  obj FG := FG.1.prod FG.2
  map nm := NatTrans.prod nm.1 nm.2

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