instNontrivialCarrierColimitOfIsFilteredOrEmptyOfObj

English

If J is filtered or empty and F: J ⥤ CommRingCat has a colimit, and every F.obj i is nontrivial, then the carrier (underlying ring) of Limits.colimit F is nontrivial.

Русский

Если J слепо фильтрована или пустая и F: J ⥤ CommRingCat имеет колимит, и каждый F.obj i непуст, то носитель колимита R = Limits.colimit F непуст.

LaTeX

$$$\operatorname{Nontrivial} \big(\big(\mathrm{Limits}.colimit F\big).\text{carrier}\big)$$

Lean4

instance {F : J ⥤ CommRingCat.{v}} [IsFilteredOrEmpty J] [HasColimit F] [∀ i, Nontrivial (F.obj i)] :
    Nontrivial ↑(Limits.colimit F) :=
  FilteredColimits.nontrivial (getColimitCocone F).2

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