instIsRightAdjointForget — Mathlib

English

The forgetful functor from commutative monoids to monoids has a right adjoint.

Русский

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

LaTeX

$$$\exists R:\text{MonCat} \to \text{CommMonCat},\; \text{forget} \dashv R,\; \forall C:\text{CommMonCat},\ M:\text{MonCat},\\ Hom_{\text{MonCat}}(\text{forget}(C), M) \cong Hom_{\text{CommMonCat}}(C, R(M)).$$$

Lean4

instance : (forget CommMonCat.{u}).IsRightAdjoint :=
  ⟨_, ⟨AddCommMonCat.adj.comp AddCommMonCat.equivalence.toAdjunction⟩⟩

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