epi_iff_isIso_inr

Mathlib.CategoryTheory.Limits.EpiMono

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

English

Let hc be IsColimit c. Then Epi f holds if and only if c.inr is an isomorphism.

Русский

Пусть hc — IsColimit c. Тогда f эпиморфизм тогда и только если c.inr — изоморфизм.

LaTeX

$$$ IsColimit\, c \rightarrow (Epi\, f \iff IsIso\, c.inr) $$$

Lean4

theorem epi_iff_isIso_inr (hc : IsColimit c) : Epi f ↔ IsIso c.inr :=
  epi_iff_isIso_inl (PushoutCocone.flipIsColimit hc)

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

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

Разделы

Аффилиация

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