instIsRightAdjointTopCatForget₂

English

The forgetful functor forget₂ from TopModuleCat(R) to TopCat is a right adjoint to the free functor, i.e., free is left adjoint to forget.

Русский

Забывающий функтор forget₂ является правым сопряжённым к свободному функтору, то есть свободный функтор слева от forget.

LaTeX

$$$\text{free} \dashv \text{forget}_{TopModuleCat(R) \to TopCat}.$$$

Lean4

instance : (forget₂ (TopModuleCat.{max v u} R) TopCat).IsRightAdjoint :=
  ⟨_, ⟨freeAdj R⟩⟩

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