id_comp

Mathlib.CategoryTheory.Sigma.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sigma.SigmaHom.id_comp

English

In the Sigma-SigmaHom setting, the left identity holds: for any f: X ⟶ Y, we have 1_X ≫ f = f.

Русский

В системе Sigma-SigmaHom выполняется тождественное слепление: для любого f: X → Y имеем 𝟙 X ∘ f = f.

LaTeX

$$$ 𝟙_X \circ f = f. $$$

Lean4

theorem id_comp : ∀ {X Y : Σ i, C i} (f : X ⟶ Y), 𝟙 X ≫ f = f
  | _, _, mk _ => congr_arg mk (Category.id_comp _)

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

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

Разделы

Аффилиация

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