monoidalFunctor_η — Mathlib

English

The η-structure of the discrete monoidal functor corresponds to the unit of F mapped to the monoidal unit, i.e. η(monoidalFunctor F) = Discrete.eqToHom(F.map_one).

Русский

η-структура дискретного моноидального функторa соответствует единице моноида через отображение F.map_one.

LaTeX

$$$ \\eta(\\text{monoidalFunctor } F) = \\mathrm{Discrete.eqToHom}(F.map\\_one).$$$

Lean4

@[to_additive Discrete.addMonoidalFunctor_η]
theorem monoidalFunctor_η (F : M →* N) : η (monoidalFunctor F) = Discrete.eqToHom F.map_one :=
  rfl

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