mono_of_mono_fac

Mathlib.CategoryTheory.Category.Basic

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

English

If h is mono and f ≫ g = h, then f is mono.

Русский

Если h моно и f ≫ g = h, тогда f моно.

LaTeX

$$$ [\\mathrm{Mono}\ h] (f:X\\to Y)(g:Y\\to Z) (f\\!\\gg\\! g = h) : \\mathrm{Mono}(f) $$$

Lean4

theorem mono_of_mono_fac {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [Mono h] (w : f ≫ g = h) : Mono f := by
  subst h; exact mono_of_mono f g

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

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

Разделы

Аффилиация

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