forget₂_commMonCat_map_ofHom — Mathlib

English

The forgetful functor from CommGrpCat to CommMonCat (commutative groups to commutative monoids) is fully faithful, i.e., morphisms are determined by their underlying monoid homomorphisms.

Русский

Забывающий функтор из CommGrpCat в CommMonCat полностью верен, то есть мороморфизмы задаются их базовыми моноидными гомоморфизмами.

LaTeX

$$$$ (\text{forget}_{CommGrpCat,CommMonCat})\text{ is fully faithful}. $$$$

Lean4

@[to_additive (attr := simp)]
theorem forget₂_commMonCat_map_ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) :
    (forget₂ CommGrpCat CommMonCat).map (ofHom f) = CommMonCat.ofHom f :=
  rfl

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