English
The product of two lax monoidal functors F: C → D and G: E → C′ carries a lax monoidal structure obtained componentwise from F and G; in particular, the unit, multiplication, and coherence maps are given by pairing those of F and G.
Русский
Произведение двух ленивомоноидальных функторов F: C → D и G: E → C′ образует леномоноидальную структуру, получаемую по компонентам от F и G; в частности, единичный и умножение, а также соответствующие соотношения образуются попарно из структур F и G.
LaTeX
$$$\text{prod}(F,G) \text{ is lax monoidal, with } ε_{\text{prod}(F,G)} = (ε_F, ε_G),\; μ_{X,Y}^{\text{prod}(F,G)} = (μ_{X,Y}^F, μ_{X,Y}^G),\; \text{etc.}$$$
Lean4
instance : (prod F G).LaxMonoidal where
ε := (ε F, ε G)
μ X Y := (μ F _ _, μ G _ _)
μ_natural_left _
_ := by
ext
all_goals
simp only [prod_obj, prodMonoidal_tensorObj, prod_map, prodMonoidal_whiskerRight, prod_comp, μ_natural_left]
μ_natural_right _
_ := by
ext
all_goals
simp only [prod_obj, prodMonoidal_tensorObj, prod_map, prodMonoidal_whiskerLeft, prod_comp, μ_natural_right]
associativity _ _
_ := by
ext
all_goals
simp only [prod_obj, prodMonoidal_tensorObj, prodMonoidal_whiskerRight, prodMonoidal_associator, Iso.prod_hom,
prod_map, prod_comp, LaxMonoidal.associativity, prodMonoidal_whiskerLeft]
left_unitality
_ := by
ext
all_goals
simp only [prodMonoidal_tensorUnit, prod_obj, prodMonoidal_tensorObj, prodMonoidal_leftUnitor_hom_fst,
LaxMonoidal.left_unitality, prodMonoidal_whiskerRight, prod_map, prodMonoidal_leftUnitor_hom_snd, prod_comp]
right_unitality
_ := by
ext
all_goals
simp only [prod_obj, prodMonoidal_tensorUnit, prodMonoidal_tensorObj, prodMonoidal_rightUnitor_hom_fst,
LaxMonoidal.right_unitality, prodMonoidal_whiskerLeft, prod_map, prodMonoidal_rightUnitor_hom_snd, prod_comp]
