English
Let F be a lax monoidal functor between monoidal categories. For any morphisms f: X → Y and g: X' → Y', the coherence morphism μ is natural in both arguments, i.e. the following square commutes: (F.map f ⊗ F.map g) followed by μ_Y,Y' equals μ_X,X' followed by F.map (f ⊗ g).
Русский
Пусть F — слабомоноидальная функция между моноидальными категориями. Для любых морфизмов f: X → Y и g: X' → Y' когерентное отображение μ естественно по обеим аргументам: (F.map f ⊗ F.map g) затем μ_Y,Y' равно μ_X,X' затем F.map (f ⊗ g).
LaTeX
$$$\\big( F\\map f \\otimes F\\map g \\big) \\\\circ \\mu_{X,X'}^F \;=\; \\mu_{Y,Y'}^F \\circ F\\map (f \\otimes g)$$$
Lean4
@[reassoc (attr := simp)]
theorem μ_natural {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
(F.map f ⊗ₘ F.map g) ≫ μ F Y Y' = μ F X X' ≫ F.map (f ⊗ₘ g) := by simp [tensorHom_def]
