instFaithfulGrp_Forget₂Grp_ — Mathlib

English

The forgetful functor from commutative groups in a braided monoidal category to underlying monoids is faithful; distinct morphisms are distinguished by their underlying morphisms.

Русский

Забывающий функтор из коммутативных групп во встроенные моноиды верен: различные морфизмы различаются по своим подлежащим морфизмам.

LaTeX

$$$\\text{Forget}_{Grp_ C}: \\text{CommGrp}_C\\text{ Faithful}$$$

Lean4

instance : (forget₂Grp_ C).Faithful :=
  InducedCategory.faithful _

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