instIsRightAdjointActionModuleCatRes

Mathlib.RepresentationTheory.Induced

URI: https://scilib.ai/kg/mathlib#Rep.instIsRightAdjointActionModuleCatRes

English

The restriction functor along φ is right adjoint to the induction functor, i.e., Res_φ ⊣ Ind_φ.

Русский

Ограничение вдоль φ является правым сопряженным индуцирующему функтору: Res_φ ⊣ Ind_φ.

LaTeX

$$$$\mathrm{Res}_\phi \dashv \mathrm{Ind}_\phi.$$$$

Lean4

noncomputable instance : (Action.res (ModuleCat.{u} k) φ).IsRightAdjoint :=
  (indResAdjunction k φ).isRightAdjoint

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

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

Разделы

Аффилиация

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