isIso_fst_of_mono

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.isIso_fst_of_mono

English

Let f: X → Y and f is mono. Then pullback.fst f f is an isomorphism.

Русский

Пусть f: X → Y моно. Тогда pullback.fst f f — изоморфизм.

LaTeX

$$$IsIso\ (pullback.fst\ f\ f)$$$

Lean4

instance isIso_fst_of_mono : IsIso (pullback.fst f f) :=
  PullbackCone.isIso_fst_of_mono_of_isLimit (getLimitCone (cospan f f)).isLimit

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

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

Разделы

Аффилиация

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