map_id — Mathlib

English

Let f: X0 → X1 be a morphism. In the two-point composable arrows construction, the two endpoint components of map f are identities. Specifically, for i = 0 or i = 1, the i-th diagonal map is the identity on the corresponding object.

Русский

Пусть f: X0 → X1 — морфизм. В конструкции двупунктированных композиционных стрел Mk₁ компоненты отображения по концу равны единичному морфизму соответствующего объекта: для i = 0 и i = 1 отображение на i-ом канале есть единичный морфизм.

LaTeX

$$$\forall i : \text{Fin}(2),\ map\ f\ i\ i = 𝟙_{X_i}$$$

Lean4

theorem map_id (i : Fin 2) : map f i i (by simp) = 𝟙 _ :=
  match i with
  | 0 => rfl
  | 1 => rfl

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