English
The composition of two discrete monoidal functors is again a discrete monoidal functor, with a canonical monoidal isomorphism between their composite and the monoidal functor of the composite of homomorphisms.
Русский
Композиция двух дискретных моноидальных функторов снова является дискретным моноидальным функтором, существует каноническая моноидальная изоморфность между их композициями.
LaTeX
$$$ \\text{monoidalFunctorComp}(F,G) : Discrete.monoidalFunctor F \\circ Discrete.monoidalFunctor G \\cong Discrete.monoidalFunctor (G \\circ F)$$$
Lean4
/-- The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.
-/
@[to_additive Discrete.addMonoidalFunctorComp /-- The monoidal natural isomorphism corresponding to
composing two additive morphisms. -/
]
def monoidalFunctorComp (F : M →* N) (G : N →* K) :
Discrete.monoidalFunctor F ⋙ Discrete.monoidalFunctor G ≅ Discrete.monoidalFunctor (G.comp F) :=
Iso.refl _
