coindResAdjunction_unit_app — Mathlib

English

For any A ∈ Rep k S, the unit component of the adjunction at A is the composition of the unit from Ind-Res with the res map through indCoindIso.

Русский

Для любого A ∈ Rep k S компонент unit при оценке на A является композицией unit из Ind-Res через indCoindIso.

LaTeX

$$$ (\mathrm{coindResAdjunction}_{k,S}).\mathrm{unit}.app A = (\mathrm{indResAdjunction}_{k,S.subtype}).\mathrm{unit}.app A \circ (\mathrm{Action.res}_{k,S.subtype}).map (\mathrm{indCoindIso}_{A}).hom $$$

Lean4

@[simp]
theorem coindResAdjunction_unit_app :
    (coindResAdjunction k S).unit.app A =
      (indResAdjunction k S.subtype).unit.app A ≫ (Action.res _ S.subtype).map (indCoindIso A).hom :=
  by
  ext
  simp [coindResAdjunction, Adjunction.ofNatIsoLeft, Adjunction.equivHomsetLeftOfNatIso, indResAdjunction]

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