fullyFaithfulForget₂ToGrp — Mathlib

English

The forgetful functor from commutative groups to groups is fully faithful.

Русский

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

LaTeX

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

Lean4

/-- The forgetful functor from commutative groups to groups is fully faithful. -/
@[to_additive fullyFaihtfulForget₂ToAddGrp /--
    The forgetful functor from additive commutative groups to additive groups is fully faithful. -/
    ]
def fullyFaithfulForget₂ToGrp : (forget₂ CommGrpCat.{u} GrpCat).FullyFaithful where preimage f := ofHom f.hom

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