functorEquiv_unit_app_app_inl — Mathlib

English

The unit component of the functor equivalence at X, on the left summand, is the identity on X(inl a).

Русский

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

LaTeX

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

Lean4

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

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