functorEquiv_unitIso_inv_app_app_inl

English

The inverse of the unit isomorphism at X, evaluated on the left summand, yields the identity on X(inl a).

Русский

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

LaTeX

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

Lean4

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

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