English
Let F1, F2, F3 be lax monoidal functors and G1, G2 be lax monoidal functors. If τ: F1 ⇒ F2 and τ′: G1 ⇒ G2 are monoidal natural transformations, then their horizontal composition τ ⧫ τ′ : F1 ∘ G1 ⇒ F2 ∘ G2 is monoidal.
Русский
Пусть F1, F2, F3 — лаксомониальные функторы, а G1, G2 — лаксомониальные функторы. Если τ: F1 ⇒ F2 и τ′: G1 ⇒ G2 — моноидальные натрансформации, то их горизонтальная композиция τ ⧫ τ′ : F1 ∘ G1 ⇒ F2 ∘ G2 является моноидальной.
LaTeX
$$$IsMonoidal(\tau \boxdot \tau')$$$
Lean4
instance hcomp {G₁ G₂ : D ⥤ E} [G₁.LaxMonoidal] [G₂.LaxMonoidal] (τ' : G₁ ⟶ G₂) [IsMonoidal τ] [IsMonoidal τ'] :
IsMonoidal (τ ◫ τ')
where
unit := by simp only [comp_obj, comp_ε, hcomp_app, assoc, naturality_assoc, unit_assoc, ← map_comp, unit]
tensor X
Y :=
by
simp only [comp_obj, comp_μ, hcomp_app, assoc, naturality_assoc, tensor_assoc, ← tensorHom_comp_tensorHom,
μ_natural_assoc]
simp only [← map_comp, tensor]
