fullyFaithfulForgetToMonCat — Mathlib

English

The forgetful functor forget₂ from CommMonCat to MonCat is fully faithful, i.e., it induces a bijection on Hom-sets for all objects.

Русский

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

LaTeX

$$$\mathrm{Hom}_{CommMonCat}(X,Y) \cong \mathrm{Hom}_{MonCat}(\mathrm{forget}_2 X, \mathrm{forget}_2 Y).$$$

Lean4

/-- The forgetful functor from `CommMonCat` to `MonCat` is fully faithful. -/
@[to_additive fullyFaithfulForgetToAddMonCat /--
    The forgetful functor from `AddCommMonCat` to `AddMonCat` is fully faithful. -/
    ]
def fullyFaithfulForgetToMonCat : (forget₂ CommMonCat.{u} MonCat.{u}).FullyFaithful where preimage f := ofHom f.hom

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