map_id — Mathlib

English

For any bifunctor F : C × D ⥤ E and objects X ∈ C, Y ∈ D, F maps the pair of identity morphisms to the identity: F.map (id_X, id_Y) = id_{F(X,Y)}.

Русский

Для любого бисюфунктора F : C × D ⥤ E и объектов X ∈ C, Y ∈ D, F преобразует пару тождественных морфизмов в тождественный морфизм: F.map (id_X, id_Y) = id_{F(X,Y)}.

LaTeX

$$$F.map (\\mathrm{id}_X, \\mathrm{id}_Y) = \\mathrm{id}_{F(X,Y)}$$$

Lean4

@[simp]
theorem map_id (F : C × D ⥤ E) (X : C) (Y : D) : F.map ((𝟙 X) ×ₘ (𝟙 Y)) = 𝟙 (F.obj (X, Y)) :=
  F.map_id (X, Y)

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