comp_id

Mathlib.CategoryTheory.Sigma.Basic

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

English

In the Sigma-SigmaHom setting, composition with a right identity yields the original morphism: f ≫ 1_Y = f.

Русский

В системе Sigma-SigmaHom композиция с правой единицей возвращает исходную стрелку: f ≫ 𝟙_Y = f.

LaTeX

$$$ f \;\circ\; 1_Y = f. $$$

Lean4

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

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

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

Разделы

Аффилиация

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