instIsRightAdjointCommGrpCatCommMonCatUnits

English

The Units functor on CommMonCat is a right adjoint; there is a corresponding forgetful adjunction with the units functor in CommMonCat.

Русский

Функтор Units на CommMonCat является правым сопряжением; существует соответствующее сопряжение забывания с функтором Units в CommMonCat.

LaTeX

$$$\text{CommMonCat.units} \text{ is a right adjoint.}$$$

Lean4

instance : CommMonCat.units.{u}.IsRightAdjoint :=
  ⟨_, ⟨CommGrpCat.forget₂CommMonAdj⟩⟩

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