English
A strengthened naturality of μ for a morphism f on the first factor and a morphism g on the second factor holds, ensuring compatibility with tensoring.
Русский
Усиленное натурализм μ для морфизма f на первом факторе и g на втором факторе сохраняет совместимость с тензоризацией.
LaTeX
$$$ (F.obj g).app((F.obj m).obj X) \\circ (F.obj n').map((F.map f).app X) \\circ (μ F m' n').app X = (μ F m n).app X \\circ (F.map (f ⊗ₘ g)).app X $$$
Lean4
@[reassoc]
theorem μ_naturality₂ {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) [F.LaxMonoidal] :
(F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
(μ F m n).app X ≫ (F.map (f ⊗ₘ g)).app X :=
by
have := congr_app (μ_natural F f g) X
dsimp at this
simpa using this
