English
The induction functor Ind_φ is left adjoint to the restriction functor Res_φ along φ: G → H.
Русский
Индукционная функторная конструкция Ind_φ является левым сопряжением к ограничению Res_φ вдоль φ: G → H.
LaTeX
$$$$\mathrm{Ind}_\phi \dashv \mathrm{Res}_\phi.$$$$
Lean4
/-- Given a group homomorphism `φ : G →* H`, the induction functor `Rep k G ⥤ Rep k H` is left
adjoint to the restriction functor along `φ`. -/
@[simps! unit_app_hom_hom counit_app_hom_hom]
noncomputable def indResAdjunction : indFunctor k φ ⊣ Action.res _ φ :=
Adjunction.mkOfHomEquiv
{ homEquiv A B := (indResHomEquiv φ A B).toEquiv
homEquiv_naturality_left_symm _
_ := Action.hom_ext _ _ <| ModuleCat.hom_ext <| IndV.hom_ext _ _ fun _ => by ext; simp
homEquiv_naturality_right := by intros; rfl }
