monoidalFunctorComp_isMonoidal — Mathlib

English

The monoidal structure on the composed functor Discrete.monoidalFunctorComp F G is monoidal, i.e. the natural transformation hom is monoidal.

Русский

Моноидальная структура композиции функторов образуется так, чтобы натуральное преобразование гом было моноидальным.

LaTeX

$$$ \\text{monoidalFunctorComp\_isMonoidal}(F,G) : NatTrans.IsMonoidal(Discrete.monoidalFunctorComp F G).hom$$$

Lean4

@[to_additive Discrete.addMonoidalFunctorComp_isMonoidal]
instance monoidalFunctorComp_isMonoidal (F : M →* N) (G : N →* K) :
    NatTrans.IsMonoidal (Discrete.monoidalFunctorComp F G).hom
    where
  unit := by
    dsimp only [comp_ε, monoidalFunctorComp, Iso.refl, Discrete.monoidalFunctor_ε]
    simp [eqToHom_map]
  tensor _
    _ := by
    dsimp only [comp_μ, monoidalFunctorComp, Iso.refl, Discrete.monoidalFunctor_μ]
    simp [eqToHom_map]

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