instIsRightAdjointForget

Mathlib.Algebra.Category.AlgCat.Basic

URI: https://scilib.ai/kg/mathlib#AlgCat.instIsRightAdjointForget

English

The forgetful functor Forget: AlgCat R → RingCat is the right adjoint to the free functor Free_R.

Русский

Забывающий функтор Forget: AlgCat R → RingCat является правым сопряжённым к свободному функтору Free_R.

LaTeX

$$$\\text{Forget}_{\\mathrm{AlgCat}(R)\\to \\mathrm{RingCat}} = (\\mathrm{Free}_R)^{\\ast}$$$

Lean4

instance : (forget (AlgCat.{u} R)).IsRightAdjoint :=
  (adj R).isRightAdjoint

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru