English
For a finite-index subgroup S ≤ G, the coinduction functor from Rep k S-subtype to Rep k G is left adjoint to the restriction functor Res k G ⥤ Rep k S, and it is naturally isomorphic to Ind_S^G.
Русский
Для подгруппы S⊆G с конечным индексом коиндукционный функтор от Rep k S-subtype к Rep k G является левым сопряжённым к ограничению, и он естественно изоморфирован Ind_S^G.
LaTeX
$$$ \mathrm{Coind}_S^G \dashv \mathrm{Res}_{S}^{G} \quad\text{and}\quad \mathrm{Coind}_S^G \cong \mathrm{Ind}_S^G $$$
Lean4
/-- Given a finite index subgroup `S ≤ G`, `Coind_S^G` is left adjoint to the restriction functor
`Res k G ⥤ Res k S`, since it is naturally isomorphic to `Ind_S^G`. -/
noncomputable def coindResAdjunction : coindFunctor k S.subtype ⊣ Action.res _ S.subtype :=
(indResAdjunction k S.subtype).ofNatIsoLeft (indCoindNatIso k S)
