instConcreteCategoryMonoidHomCarrier

English

There is a concrete category structure on CommGrpCat whose morphisms are MonoidHom between underlying carriers.

Русский

Существует конкретная структура категории на CommGrpCat, чьи морфизмы — MonoidHom между базовыми носителями.

LaTeX

$$$ \\mathrm{Hom}_{\\mathrm{CommGrpCat}}(X,Y) = \\mathrm{MonoidHom}(X.{\\mathrm carrier}, Y.{\\mathrm carrier}) $$$

Lean4

@[to_additive]
instance : ConcreteCategory CommGrpCat (· →* ·) where
  hom := Hom.hom'
  ofHom := Hom.mk

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