instFullGrpCatForget₂ — Mathlib

English

The forgetful functor forget₂ CommGrpCat GrpCat is full; every GrpCat-morphism between underlying objects comes from a CommGrpCat-morphism.

Русский

Забывающий функтор forget₂ CommGrpCat GrpCat полон: каждый мороморфизм в GrpCat между соответствующими объектами исходит из мороморфизма CommGrpCat.

LaTeX

$$$$ (\text{forget}_{\mathrm{CommGrpCat},\mathrm{GrpCat}}).\text{Full}. $$$$

Lean4

@[to_additive]
instance : (forget₂ CommGrpCat.{u} GrpCat).Full :=
  fullyFaithfulForget₂ToGrp.full

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