id_of_comp_right_id

Mathlib.CategoryTheory.Category.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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