isColimit_exists_rep — Mathlib

English

Let F: J ⥤ SheafedSpace(C) be a diagram with a colimit cocone c. Then every element x of the colimit can be written as the image of some y ∈ F(i) for some i ∈ J, i.e., there exists i and y with (c.ι.app i).base y = x.

Русский

Пусть F: J ⥤ SheafedSpace(C) — диаграмма с колимитом c. Любой элемент x колимита можно представить как образ элемента y ∈ F(i) для некоторого i ∈ J, то есть существуют i и y такие, что (c.ι.app i).base y = x.

LaTeX

$$∃ (i : J) (y : F.obj i), (c.ι.app i).base y = x$$

Lean4

theorem isColimit_exists_rep [HasLimitsOfShape Jᵒᵖ C] {c : Cocone F} (hc : IsColimit c) (x : c.pt) :
    ∃ (i : J) (y : F.obj i), (c.ι.app i).base y = x :=
  Concrete.isColimit_exists_rep (F ⋙ forget C) (isColimitOfPreserves (forget C) hc) x

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