colimit_exists_rep — Mathlib

English

Let F: J ⥤ SheafedSpace(C) with HasLimitsOfShape(Opposite J). For any x in the colimit of F, there exists i and y ∈ F(i) with (colimit.ι F i).base y = x.

Русский

Пусть F: J ⥤ SheafedSpace(C) имеет пределы формы Opposite J. Для любого x в колимите F существует i и y ∈ F(i) с (colimit.ι F i).base y = x.

LaTeX

$$∃ i (y : F.obj i), (colimit.ι F i).base y = x$$

Lean4

theorem colimit_exists_rep [HasLimitsOfShape Jᵒᵖ C] (x : colimit (C := SheafedSpace C) F) :
    ∃ (i : J) (y : F.obj i), (colimit.ι F i).base y = x :=
  Concrete.isColimit_exists_rep (F ⋙ SheafedSpace.forget C)
    (isColimitOfPreserves (SheafedSpace.forget _) (colimit.isColimit F)) x

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