functorEquiv_unitIso_inv_app_app_inr

English

The inverse of the unit isomorphism at X, evaluated on the right summand, yields the identity on X(inr a').

Русский

Обратный образ изоморфизма единицы, применённый к X на правой summand, даёт тождество на X(inr a').

LaTeX

$$((\mathrm{unitIso}.inv.app X).app(\mathrm{inr}_{A A'}) = \mathrm{id}_{X(\mathrm{inr}_{A A'} a')})$$

Lean4

@[simp]
theorem functorEquiv_unitIso_inv_app_app_inr (X : A ⊕ A' ⥤ B) (a' : A') :
    ((functorEquiv A A' B).unitIso.inv.app X).app (.inr a') = 𝟙 (X.obj (.inr a')) :=
  rfl

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