hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit

English

Suppose that for every X ∈ C and for every morphism f: X → Y in C, the fibered diagram F.map f ⋙ Grothendieck.ι F Y ⋙ G has a colimit, and that the entire fiberwiseColimit G has a colimit. Then the total functor G has a colimit.

Русский

Пусть для каждого X ∈ C и каждого морфизма f: X → Y в C тяготеющие к диаграмме колимиты существуют, и что всякая fiberwiseColimit G имеет колимит. Тогда суммарный функтор G имеет колимит.

LaTeX

$$$\Big( \forall X,Y,f, \mathrm{HasColimit}(F.map f \circ \iota_F Y \circ G) \Big) \\ \land \mathrm{HasColimit}(\mathrm{fiberwiseColimit}\, G) \Rightarrow \mathrm{HasColimit}(G).$$$

Lean4

/-- We can infer that a functor `G : Grothendieck F ⥤ H`, with `F : C ⥤ Cat`, has a colimit from
the fact that each of its fibers has a colimit and that these fiberwise colimits, as a functor
`C ⥤ H` have a colimit. -/
@[local instance]
theorem hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit : HasColimit G where
  exists_colimit := ⟨⟨_, isColimitCoconeOfFiberwiseCocone (colimit.isColimit _)⟩⟩

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