coe_id — Mathlib

English

In a concrete category, the identity morphism corresponds to the identity function under the forgetful functor.

Русский

В конкретной категории тождественный морфизм соответствует тождественной функции под забывающим функтором.

LaTeX

$$$(\mathrm{forget})\_C(\mathrm{id}_X) = \mathrm{id}_{(\mathrm{forget})C X}$$$

Lean4

theorem coe_id {X : C} : (𝟙 X : X → X) = id :=
  (forget _).map_id X

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