instIsLeftAdjointCommMonCatUnderMonoidAlgebra

Mathlib.Algebra.Category.Ring.Adjunctions

URI: https://scilib.ai/kg/mathlib#CommRingCat.instIsLeftAdjointCommMonCatUnderMonoidAlgebra

English

For any commutative ring R, monoidAlgebra is a left adjoint to Under.forget in CommRingCat.

Русский

Для любого кольца R моноидалгебра является левым адъюнктом к Under.forget в CommRingCat.

LaTeX

$$$R.monoidAlgebra \dashv Under.forget R$$$

Lean4

instance (R : CommRingCat) : (monoidAlgebra.{u, u} R).IsLeftAdjoint :=
  ⟨_, ⟨CommRingCat.monoidAlgebraAdj R⟩⟩

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

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

Разделы

Аффилиация

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