prod' — Mathlib

English

Naturality of the product of natural transformations: the square commutes for composed morphisms in the product category.

Русский

Натуральность произведения натуральных преобразований: квадрат диаграммы коммутирует для композиции морфизмов в произведении категорий.

LaTeX

$$$\\mathrm{NatTrans.prod}(\\alpha,\\beta)$ is natural, i.e. it respects composition: the naturality squares commute.$$

Lean4

/-- The Cartesian product of two natural transformations where both functors have the
same source. -/
@[simps! app_fst app_snd]
def prod' {F G : A ⥤ B} {H K : A ⥤ C} (α : F ⟶ G) (β : H ⟶ K) : F.prod' H ⟶ G.prod' K where app X := (α.app X, β.app X)

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