mono_ι — Mathlib

English

For a finitary extensive category and finite index i, the injection into the sigma-type coproduct is mono.

Русский

В конечной расширяемой категории и для конечного индекса i инъекция в копроизведение по сигмe моно.

LaTeX

$$$Mono(\Sigma.ι X i)$$$

Lean4

theorem mono_ι [FinitaryExtensive C] {ι : Type*} [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c)
    (i : Discrete ι) : Mono (c.ι.app i) :=
  mono_of_cofan_isVanKampen (isVanKampen_finiteCoproducts hc) _

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