English
The Cartesian product of two natural transformations α: F ⟶ G and β: H ⟶ I is a natural transformation α.prod β: F.prod H ⟶ G.prod I, whose component at X is (α.app X.1, β.app X.2).
Русский
Декартово произведение двух натуральных преобразований α: F ⟶ G и β: H ⟶ I образует натуральное преобразование α.prod β: F.prod H ⟶ G.prod I с компонентами (α.app X.1, β.app X.2).
LaTeX
$$$\\mathrm{prod} (\\alpha, \\beta): F \\mathrm{prod} H \\to G \\mathrm{prod} I$, with $(\\mathrm{app}\\ X)=(\\alpha.app\,X.1, \\beta.app\,X.2)$.$$
Lean4
/-- The Cartesian product of two natural transformations. -/
@[simps! app_fst app_snd]
def prod {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) : F.prod H ⟶ G.prod I where
app
X :=
(α.app X.1, β.app X.2)
/- Again, it is inadvisable in Lean 3 to setup a notation `α × β`;
use instead `α.prod β` or `NatTrans.prod α β`. -/
