id_of_comp_left_id

Mathlib.CategoryTheory.Category.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.id_of_comp_left_id

English

If f : X → X satisfies f ≫ g = g for all g : X → Y, then f = id_X.

Русский

Если морфизм f: X → X удовлетворяет f ∘ g = g для всех g: X → Y, тогда f = id_X.

LaTeX

$$$ (\\forall Y\\; g:X\\to Y), f\\circ g = g \\Rightarrow f = \\mathrm{id}_X $$$

Lean4

theorem id_of_comp_left_id (f : X ⟶ X) (w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g) : f = 𝟙 X :=
  by
  convert w (𝟙 X)
  simp

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

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

Разделы

Аффилиация

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