English
For B ∈ Rep(k,G) and f: A ⟶ (Action.res _ S.subtype).obj B, the symmetric version of the hom-equivalence equals inv composed with the inverse of indResHomEquiv.
Русский
Для B ∈ Rep(k,G) и f: A ⟶ (Action.res _ S.subtype).obj B, симметрическая версия гом-эквивалентности равна композиции с инверсией и посредством обратного indResHomEquiv.
LaTeX
$$$ ((\mathrm{resIndAdjunction}_{k,S}).\mathrm{homEquiv}_{A,B})^{-1} f = (\mathrm{resCoindHomEquiv}_{S,\subtype,B,A})^{-1} \Bigl( f \circ (\mathrm{indCoindIso}_{A}).hom \Bigr) $$$
Lean4
theorem coindResAdjunction_homEquiv_symm_apply {B : Rep k G} (f : A ⟶ (Action.res _ S.subtype).obj B) :
((coindResAdjunction k S).homEquiv _ _).symm f = (indCoindIso A).inv ≫ (indResHomEquiv S.subtype A B).symm f :=
by
simp only [coindResAdjunction, Adjunction.ofNatIsoLeft, indResAdjunction, Adjunction.mkOfHomEquiv_homEquiv]
rfl
