hom — Mathlib

English

The morphism in GrpCat corresponds to a monoid hom between the underlying carriers.

Русский

Морфизм в GrpCat соответствует гомоморфизму моноидов между базовыми множествами.

LaTeX

$$$\GrpCat.Hom.hom: X \to Y \text{ is a MonoidHom on the underlying carriers.}$$$

Lean4

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

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