hom — Mathlib

English

The morphism from X to Y in CommGrpCat can be viewed as a MonoidHom between their underlying carriers.

Русский

Гомоморфизм в CommGrpCat между X и Y может рассматриваться как MonoidHom между их носителями.

LaTeX

$$$ \\mathrm{CommGrpCat}.Hom.hom: X \\to Y \\;\\subseteq\\; \\mathrm{MonoidHom}(X.{\\mathrm carrier}, Y.{\\mathrm carrier}) $$$

Lean4

/-- Turn a morphism in `CommGrpCat` back into a `MonoidHom`. -/
@[to_additive /-- Turn a morphism in `AddCommGrpCat` back into an `AddMonoidHom`. -/
    ]
abbrev hom {X Y : CommGrpCat.{u}} (f : Hom X Y) :=
  ConcreteCategory.hom (C := CommGrpCat) f

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