English
There is an adjunction with the restriction functor along φ as the left adjoint to the coinduction functor; equivalently, coinduction is right adjoint to restriction along φ.
Русский
Существуют смежности: ограничение вдоль φ является левым соседом коиндукции; соответственно коиндукция является правым соседом ограничения.
LaTeX
$$$\mathrm{Res}_\phi \dashv \mathrm{coindFunctor}_k\phi$$$
Lean4
/-- Given a monoid homomorphism `φ : G →* H`, the coinduction functor `Rep k G ⥤ Rep k H` is right
adjoint to the restriction functor along `φ`. -/
@[simps! counit_app_hom_hom unit_app_hom_hom]
noncomputable abbrev resCoindAdjunction : Action.res _ φ ⊣ coindFunctor k φ :=
Adjunction.mkOfHomEquiv
{ homEquiv X Y := (resCoindHomEquiv φ X Y).toEquiv
homEquiv_naturality_left_symm := by intros; rfl
homEquiv_naturality_right := by intros; ext; rfl }
