map_id_id

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.coprod.map_id_id

English

In a binary coproduct X ⨿ Y, the map coprod.map (id X) (id Y) is the identity on X ⨿ Y.

Русский

Для копрода X ⨿ Y отображение coprod.map (id X) (id Y) есть тождество на X ⨿ Y.

LaTeX

$$$\forall X,Y\; [HasBinaryCoproduct X Y],\; coprod.map (id X) (id Y) = id_{X\sqcup Y}.$$$

Lean4

@[simp]
theorem map_id_id {X Y : C} [HasBinaryCoproduct X Y] : coprod.map (𝟙 X) (𝟙 Y) = 𝟙 _ := by ext <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru