hasForgetToSemigroup — Mathlib

English

There is an adjunction between free MonCat and forgetful functor to Semigrp (for monoids). The hom-equivalence induces the adjunction a la free ⊣ forget.

Русский

Существует сопряжение между свободной и забывающей конструкциями для моноидов; эквиваленция гомоморфизмов порождает данное сопряжение.

LaTeX

$$MonCat.adjoinOneAdj : adjoinOne ⊣ forget₂ MonCat Semigrp$$

Lean4

@[to_additive]
instance hasForgetToSemigroup : HasForget₂ MonCat Semigrp where
  forget₂ :=
    { obj := fun M => Semigrp.of M
      map f := Semigrp.ofHom f.hom.toMulHom }

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