resIndAdjunction_unit_app — Mathlib

English

The unit component at B for the adjunction Res ⊣ Ind is given by the composite of the counit and the inverse of the Ind-Coind isomorphism, as specified by the formula.

Русский

Компонента unit в точке B для пары смежности Res ⊣ Ind задаётся композицией counit и обратного Ind-Coind изоморфизма, согласно формуле.

LaTeX

$$$(resIndAdjunction k S).unit.app B = (resCoindAdjunction k S.subtype).unit.app B \; ∘ \; (indCoindIso ((Action.res _ S.subtype).obj B)).inv$$$

Lean4

@[simp]
theorem resIndAdjunction_unit_app (B : Rep k G) :
    (resIndAdjunction k S).unit.app B =
      (resCoindAdjunction k S.subtype).unit.app B ≫ (indCoindIso ((Action.res _ S.subtype).obj B)).inv :=
  rfl

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