English
The counit component at A for the adjunction Res ⊣ Ind is given by the composite of the forgetful action map and the Ind-Coind isomorphism, as described by the explicit formula.
Русский
Компонента counit в точке A для пары рез-инд (Res ⊣ Ind) задаётся композицией отображения действия забывания и изоморфизма Ind-Coind, согласно явной формуле.
LaTeX
$$$(resIndAdjunction k S).counit.app A = (Action.res _ S.subtype).map (indCoindIso A).hom \; ∘ \; (resCoindAdjunction k S.subtype).counit.app A$$$
Lean4
/-- Given a finite index subgroup `S ≤ G`, `Ind_S^G` is right adjoint to the restriction functor
`Res k G ⥤ Res k S`, since it is naturally isomorphic to `Coind_S^G`. -/
noncomputable def resIndAdjunction : Action.res _ S.subtype ⊣ indFunctor k S.subtype :=
(resCoindAdjunction k S.subtype).ofNatIsoRight (indCoindNatIso k S).symm
