English
Naturality of δ with respect to associativity is reflected in a mixed composition with tensorHoms.
Русский
Натуральность δ по отношению к ассоциатору отражается в смешанной композиции с tensorHoms.
LaTeX
$$$δ F X (Y ⊗ Z) ∘ (F.map (α_{X Y Z})^{−1}) = (α_{F X F Y F Z})^{−1} ∘ μ_F X Y ∘ δ F Y Z ∘ μ_F (X ⊗ Y) Z$$$
Lean4
@[simps]
instance comp : (F ⋙ G).OplaxMonoidal where
η := G.map (η F) ≫ η G
δ X Y := G.map (δ F X Y) ≫ δ G _ _
δ_natural_left {X Y} f
X' := by
dsimp
rw [assoc, δ_natural_left, ← G.map_comp_assoc, δ_natural_left, map_comp, assoc]
δ_natural_right _
_ := by
dsimp
rw [assoc, δ_natural_right, ← G.map_comp_assoc, δ_natural_right, map_comp, assoc]
oplax_associativity X Y
Z := by
dsimp
rw [comp_whiskerRight, assoc, assoc, assoc, δ_natural_left_assoc, associativity, ← G.map_comp_assoc, ←
G.map_comp_assoc, assoc, associativity, map_comp, map_comp, assoc, assoc, MonoidalCategory.whiskerLeft_comp,
δ_natural_right_assoc]
