English
For B ∈ Rep(k,G) and A ∈ Rep(k,S) with a morphism f: B ⟶ (indFunctor k S.subtype).obj A, the inverse of the hom-equivalence is given by composing the inverse of resCoindHomEquiv with the symmetrized map, i.e., the symmetric version of the Hom-Equiv formula.
Русский
Для B ∈ Rep(k,G) и A ∈ Rep(k,S) с морфизмом f: B ⟶ (indFunctor k S.subtype).obj A, обратное отображение гом-эквивалентности задано композицией с симметрированной картой, то есть симметрическая версия формулы гом-эквивалентности.
LaTeX
$$$ (\mathrm{resIndAdjunction}_{k,S}).\mathrm{homEquiv}_{A,B}^{-1}(f) = (\mathrm{resCoindHomEquiv}_{S,\subtype})_{B A}^{-1} \bigl( f \; \circ\; (\mathrm{indCoindIso}_{A})\bigr) $$$
Lean4
theorem resIndAdjunction_homEquiv_symm_apply {B : Rep k G} (f : B ⟶ (indFunctor k S.subtype).obj A) :
((resIndAdjunction k S).homEquiv _ _).symm f = (resCoindHomEquiv S.subtype B A).symm (f ≫ (indCoindIso A).hom) :=
by
simp only [resIndAdjunction, Adjunction.ofNatIsoRight, resCoindAdjunction, Adjunction.mkOfHomEquiv_homEquiv]
rfl
