exists_iso_map

Mathlib.CategoryTheory.Subobject.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

/-- When `f : X ⟶ Y` is a monomorphism, `exists f` agrees with `map f`.
-/
theorem exists_iso_map (f : X ⟶ Y) [Mono f] : «exists» f = map f :=
  lower_iso _ _ (MonoOver.existsIsoMap f)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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