instIsLeftAdjointModuleCatForget₂

English

The forgetful functor forget₂ has both left and right adjoints given by the indiscrete topology and the module-topology construction.

Русский

У забывающего функтор forget₂ существуют и левый, и правый сопряженные, задаваемые indiscrete и конструкциями топологии модуля.

LaTeX

$$$forget₂ \\dashv indiscrete \\;\\text{and}\\; withModuleTopology \\dashv forget₂$$$

Lean4

instance : (forget₂ (TopModuleCat.{v} R) (ModuleCat.{v} R)).IsLeftAdjoint :=
  ⟨_, ⟨indiscreteAdj R⟩⟩

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