ι_of_coproductDisjoint

Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Mono.ι_of_coproductDisjoint

← MathLib Explorer

English

In a binary disjoint coproduct situation, the right leg is mono whenever the corresponding colimit exists.

Русский

В случае бинарного раздельного копродукта правая стрелка моно, если дан колимит.

LaTeX

$$$\\text{Mono}\\, g$$$

Lean4

instance _root_.CategoryTheory.Mono.ι_of_coproductDisjoint [HasCoproduct X] (i : ι) : Mono (Sigma.ι X i) :=
  CoproductDisjoint.mono_inj (colimit.isColimit _) i

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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