hasForgetToMon — Mathlib

English

There is a forgetful functor GrpWithZero → MonCat forgetting the zero-structure while preserving monoid structure, defined by X ↦ MonCat.of X and f ↦ MonCat.ofHom f.toMonoidHom.

Русский

Существует забывающий функтор GrpWithZero → MonCat, который забывает нулевую структуру, сохраняя моноидную структуру: X ↦ MonCat.of X, f ↦ MonCat.ofHom f.toMonoidHom.

LaTeX

$$$\text{forget}_2 : \mathrm{GrpWithZero} \to \mathrm{MonCat}$ with $\mathrm{forget}_2(X) = \mathrm{MonCat.of}(X)$ and $\mathrm{forget}_2(f) = \mathrm{MonCat.ofHom}(f^{\text{toMonoidHom}})$$$

Lean4

instance hasForgetToMon : HasForget₂ GrpWithZero MonCat where
  forget₂ :=
    { obj := fun X => MonCat.of X
      map := fun f => MonCat.ofHom f.toMonoidHom }

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