monoidalFunctor — Mathlib

English

A monoid homomorphism between monoids induces a monoidal functor between their discrete monoidal categories.

Русский

Гомоморфизм моноидов порождает моноидальный функтор между их дискретными моноидальными категориями.

LaTeX

$$$ F: M \to N \\Rightarrow \\text{MonoidalFunctor } F : \text{Discrete } M \to \text{Discrete } N $$$

Lean4

/-- A multiplicative morphism between monoids gives a monoidal functor between the corresponding
discrete monoidal categories.
-/
@[to_additive Discrete.addMonoidalFunctor]
def monoidalFunctor (F : M →* N) : Discrete M ⥤ Discrete N :=
  Discrete.functor (fun X ↦ Discrete.mk (F X))

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