instIsRightAdjointForget — Mathlib

English

The forgetful functor from ModuleCat(R) is a right adjoint to the free functor, i.e., the free-forgetful adjunction exists.

Русский

Забывающий функтор из ModuleCat(R) является правым соседом свободного функторa, существет свободно-забывающая адъюнкция.

LaTeX

$$$\mathrm{forget}(\mathrm{ModuleCat}(R)) \text{ is right adjoint to } \mathrm{free}$$$

Lean4

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

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