hasColimitsOfShape_grothendieck — Mathlib

English

There exists a colimit for G whenever the fiberwise construction fiberwiseColimit G has a colimit and the fiberwise conditions hold as above.

Русский

Существует колимит для G, если fiberingобразование fiberwiseColimit G имеет колимит и выполняются условия по волокнам.

LaTeX

$$$[\mathrm{HasColimit}(\mathrm{fiberwiseColimit}\ G)] \Rightarrow \mathrm{HasColimit}(G).$$$

Lean4

@[instance]
theorem hasColimitsOfShape_grothendieck [∀ X, HasColimitsOfShape (F.obj X) H] [HasColimitsOfShape C H] :
    HasColimitsOfShape (Grothendieck F) H where
  has_colimit _ := hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit _

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