isIso_inl_of_epi

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

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

English

If h: W → X is epi and f: X → Y, then HasPushout (h ≫ f) h.

Русский

Если h: W → X эпиморфизм и f: X → Y, то HasPushout (h ∘ f) h.

LaTeX

$$$\\text{HasPushout }(h\\circ f)\\, h$$$

Lean4

instance isIso_inl_of_epi : IsIso (pushout.inl f f) :=
  PushoutCocone.isIso_inl_of_epi_of_isColimit (getColimitCocone (span f f)).isColimit

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

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

Разделы

Аффилиация

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