prod' — Mathlib

English

For functors F: A → B and G: A → C, there is a product functor F ×' G: A → B × C, defined by F ×' G (a) = (F(a), G(a)) and (F ×' G)(f) = (F(f), G(f)).

Русский

Пусть F: A → B и G: A → C. Тогда существует произведение F ×' G: A → B × C, задаваемое $(F \\times' G)(a)=(F(a), G(a))$ и $(F \\times' G)(f)=(F(f), G(f))$.

LaTeX

$$$\\mathrm{prod'}(F,G): A \\to B \\times C$ with $\\mathrm{obj}(a)=(F(a),G(a))$ and $\\mathrm{map}(f)=(F(f),G(f))$.$$

Lean4

/-- Similar to `prod`, but both functors start from the same category `A` -/
@[simps]
def prod' (F : A ⥤ B) (G : A ⥤ C) : A ⥤ B × C
    where
  obj a := (F.obj a, G.obj a)
  map f := (F.map f, G.map f)

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