prod' — Mathlib

English

The diag functor carries a Monoidal instance making the diagonal into a monoidal functor.

Русский

Диагональный функтор обладает моноидальной структурой, превращая диагональный функтор в моноидальный.

LaTeX

$$$ (\mathrm{diag}\, C).Monoidal = \text{CoreMonoidal}(C) $$$

Lean4

/-- The functor `C ⥤ D × E` obtained from two lax monoidal functors is lax monoidal. -/
instance prod' : (prod' F G).LaxMonoidal :=
  inferInstanceAs (diag C ⋙ prod F G).LaxMonoidal

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