monoidalFunctorMonoidal — Mathlib

English

For a monoid homomorphism F: M →* N, the induced functor Discrete.monoidalFunctor F carries a monoidal structure; i.e. Discrete.monoidalFunctor F is a monoidal functor.

Русский

Для гомоморфизма F: M →* N индуцированный функтор Discrete.monoidalFunctor F имеет моноидальную структуру; то есть Discrete.monoidalFunctor F является моноидальным функтором.

LaTeX

$$$ (Discrete.monoidalFunctor F).Monoidal $$$

Lean4

@[to_additive Discrete.addMonoidalFunctorMonoidal]
instance monoidalFunctorMonoidal (F : M →* N) : (Discrete.monoidalFunctor F).Monoidal :=
  Functor.CoreMonoidal.toMonoidal
    { εIso := Discrete.eqToIso F.map_one.symm
      μIso := fun m₁ m₂ ↦ Discrete.eqToIso (F.map_mul _ _).symm }

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