epi_f

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity.epi_f

English

Under IsColimit,epi_f holds: the morphism f z is epi after pushing forward along the colimit cone.

Русский

При IsColimit сохраняется epi_f: f z эпиморфизм после проталкивания вдоль конуса колимита.

LaTeX

$$$\text{epi}_{f}(hc,z)$$$

Lean4

theorem epi_f [IsFiltered J] : Epi (f z) := by
  have := isIso_f hc z
  infer_instance

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

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

Разделы

Аффилиация

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