instIsLeftAdjointIndFunctor

Mathlib.RepresentationTheory.Induced

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

English

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

Русский

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

LaTeX

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

Lean4

noncomputable instance : (indFunctor k φ).IsLeftAdjoint :=
  (indResAdjunction k φ).isLeftAdjoint

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

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

Разделы

Аффилиация

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