English
For any B ∈ Rep(k,G), the counit component of the adjunction evaluated at B is the composite of the inverse of indCoindIso applied to (Action.res B) with the counit of the Ind-Res adjunction.
Русский
Для любого B ∈ Rep(k,G) компонент counit при оценке на B является композицией инверса indCoindIso применённого к (Action.res B) с counit Ind-Res сопряжения.
LaTeX
$$$ (\mathrm{coindResAdjunction}_{k,S}).\mathrm{counit}.app B = (\mathrm{indCoindIso} ((\mathrm{Action.res}_{k} S.subtype).obj B)).inv \circ (\mathrm{indResAdjunction}_{k,S.subtype}).\mathrm{counit}.app B $$$
Lean4
@[simp]
theorem coindResAdjunction_counit_app (B : Rep k G) :
(coindResAdjunction k S).counit.app B =
(indCoindIso <| (Action.res _ S.subtype).obj B).inv ≫ (indResAdjunction k S.subtype).counit.app B :=
by simp [coindResAdjunction, Adjunction.ofNatIsoLeft, Adjunction.equivHomsetLeftOfNatIso, indResAdjunction]
