instIsRightAdjointModuleCatIndiscrete

Mathlib.Algebra.Category.ModuleCat.Topology.Basic

URI: https://scilib.ai/kg/mathlib#TopModuleCat.instIsRightAdjointModuleCatIndiscrete

English

The indiscrete functor is right adjoint to the forgetful functor for TopModuleCat.

Русский

Indiscrete-функтор является правым сопряженным забыванию для TopModuleCat.

LaTeX

$$$indiscrete \\dashv forget₂$$$

Lean4

instance : (indiscrete.{v} R).IsRightAdjoint :=
  ⟨_, ⟨indiscreteAdj R⟩⟩

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

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

Разделы

Аффилиация

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