colimitQuotientCoproduct_epi

Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

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

English

The colimit quotient coproduct map is epi in suitable size.

Русский

Ко-колимитный фактор копроизведения является эпиморфизмом в допустимом размере.

LaTeX

$$[HasColimitsOfSize w C] (F : J ⥤ C) : Epi (colimitQuotientCoproduct F)$$

Lean4

instance colimitQuotientCoproduct_epi [HasColimitsOfSize.{w, w} C] (F : J ⥤ C) : Epi (colimitQuotientCoproduct F) :=
  epi_comp _ _

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

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

Разделы

Аффилиация

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