instHomFunctorAssociator — Mathlib

English

For lax monoidal functors F, G, H, the associator hom (F ∘ G) ∘ H → F ∘ (G ∘ H) is monoidal.

Русский

Для лаксомониальных функторов F, G, H гом ассоциатора между (F ∘ G) ∘ H и F ∘ (G ∘ H) моноидален.

LaTeX

$$IsMonoidal(F.associator G H).hom$$

Lean4

instance (F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') [F.LaxMonoidal] [G.LaxMonoidal] [H.LaxMonoidal] :
    NatTrans.IsMonoidal (Functor.associator F G H).hom
    where
  unit := by simp only [comp_obj, comp_ε, assoc, Functor.map_comp, associator_hom_app, comp_id, Functor.comp_map]
  tensor X
    Y := by
    simp only [comp_obj, comp_μ, associator_hom_app, Functor.comp_map, map_comp, comp_id, tensorHom_id, id_whiskerRight,
      assoc, id_comp]

Похожие утверждения