instEpiDescι — Mathlib

English

If F has a colimit and F.obj has coproducts, then the map desc from the coproduct to the colimit is epi.

Русский

Если у F есть колимит, а у F.obj есть ко-продукты, то отображение desc до колимита является эпиморфизмом.

LaTeX

$$$\text{Epi} (\Sigma.\desc (\text{colimit.ι } F))$$$

Lean4

instance [HasColimit F] [HasCoproduct F.obj] : Epi (Sigma.desc (colimit.ι F)) where
  left_cancellation _ _
    h := by
    refine colimit.hom_ext fun j => ?_
    simpa using Sigma.ι _ j ≫= h

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