cancel_mono_id

Mathlib.CategoryTheory.Category.Basic

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

English

If g ≫ f = f with f mono, then g = id_Y.

Русский

Если g ≫ f = f и f моно, то g = id_Y.

LaTeX

$$$ (g:Y\\to Y)\\; [\\mathrm{Mono} f] \\; (g \\circ f) = f \\iff g = \\mathrm{id}_Y $$$

Lean4

theorem cancel_mono_id (f : X ⟶ Y) [Mono f] {g : X ⟶ X} : g ≫ f = f ↔ g = 𝟙 X :=
  by
  convert cancel_mono f
  simp

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

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

Разделы

Аффилиация

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