epi

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cofork.IsColimit.epi

English

If s is a colimit cocone for the pair f,g, then the cocone leg s.π is an epimorphism.

Русский

Если s является колимитным ко-конусом пары f,g, то факт s.π является эпиморфизмом.

LaTeX

$$$\text{If } s \text{ is a colimit cocone for } f,g, \text{ then } s.\pi \text{ is epi}. $$$

Lean4

theorem epi {s : Cofork f g} (hs : IsColimit s) : Epi s.π where left_cancellation _ _ h := hom_ext hs h

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

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

Разделы

Аффилиация

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