instIsRightAdjointGrpCatMonCatUnits

English

The functor MonCat.units is a right adjoint to forget₂ GrpCat MonCat; equivalently, forget₂ GrpCat MonCat ⊣ MonCat.units.

Русский

Функтор MonCat.units является правым сопряжением к forget₂ GrpCat MonCat; эквивалентно forget₂ GrpCat MonCat ⊣ MonCat.units.

LaTeX

$$$\text{forget}_{\,\GrpCat\to\MonCat} \dashv \text{MonCat.units}.$$$

Lean4

instance : MonCat.units.{u}.IsRightAdjoint :=
  ⟨_, ⟨GrpCat.forget₂MonAdj⟩⟩

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