coindResAdjunction_homEquiv_apply

English

For B ∈ Rep(k,G) and f: coind S.subtype A ⟶ B, the hom-equivalence applied to f equals indResHomEquiv with the coind iso applied to f.

Русский

Для B ∈ Rep(k,G) и f: coind S.subtype A ⟶ B, применение гом-эквивалентности к f равно indResHomEquiv после применения коинд-изоморфизма к f.

LaTeX

$$$ (\mathrm{coindResAdjunction}_{k,S}).\mathrm{homEquiv}_{A,B} \; f = \mathrm{indResHomEquiv}_{S.subtype,A,B} \bigl((\mathrm{indCoindIso}_{A}).hom \circ f\bigr) $$$

Lean4

theorem coindResAdjunction_homEquiv_apply {B : Rep k G} (f : coind S.subtype A ⟶ B) :
    (coindResAdjunction k S).homEquiv _ _ f = indResHomEquiv S.subtype A B ((indCoindIso A).hom ≫ f) :=
  by
  simp only [coindResAdjunction, Adjunction.ofNatIsoLeft, indResAdjunction, Adjunction.mkOfHomEquiv_homEquiv]
  rfl

Похожие утверждения