map_mk

Mathlib.CategoryTheory.Subobject.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.map_mk

English

If f is mono, exists f agrees with map f.

Русский

Если f моно, то exists f совпадает с map f.

LaTeX

$$$\text{exists}(f) = \mathrm{map}(f)\quad (\text{for mono } f)$$$

Lean4

theorem map_mk {A X Y : C} (i : A ⟶ X) [Mono i] (f : X ⟶ Y) [Mono f] : (map f).obj (mk i) = mk (i ≫ f) :=
  rfl

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

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

Разделы

Аффилиация

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