instConcreteCategoryMonoidHomCarrier

English

MonCat is endowed with a concrete category structure: morphisms are MonoidHom on carriers and the ofHom operation gives the carrier-level morphisms.

Русский

MonCat оборудована структурой конкретной категории: морфизмы задаются как гомоморфизмы моноидов между носителями, а ofHom задаёт соответствие на носителях.

LaTeX

$$$\text{MonCat is a ConcreteCategory with }\mathrm{Hom}(X,Y)=\mathrm{MonoidHom}(X\;\text{carrier}, Y\;\text{carrier})\text{ and }\mathrm{ofHom}=\mathrm{Hom.mk}.$$$

Lean4

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

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