functorEquiv_unit_app_app_inr — Mathlib

English

The unit component of the functor equivalence at X, on the right summand, is the identity on X(inr a').

Русский

Единичный компонент эквивалентности функторов для правой части суммирования равен тождественному отображению на X(inr a').

LaTeX

$$((\mathrm{functorEquiv} A A' B).unit.app X).app(\mathrm{inr}_{A A'}) = \mathrm{id}_{X(\mathrm{inr}_{A A'} a')}$$

Lean4

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

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