English
Let J be a small filtered category and F: J ⥤ CommRingCat be a diagram of commutative rings. If every object F.obj i is nontrivial, then the colimit object of F is nontrivial; equivalently, the underlying ring of the colimit is nonzero.
Русский
Пусть J — малая фильтрованная категория и F: J ⥤ CommRingCat — диаграмма коммутативных колец. Если для каждого i множество F.obj i не тривиально, то колимит диаграммы F непуст. то есть несводим к нулю.
LaTeX
$$$\operatorname{Nontrivial} (\mathrm{Limits}.colimit F)$$
Lean4
protected theorem nontrivial {F : J ⥤ CommRingCat.{v}} [IsFilteredOrEmpty J] [∀ i, Nontrivial (F.obj i)] {c : Cocone F}
(hc : IsColimit c) : Nontrivial c.pt := by
classical
cases isEmpty_or_nonempty J
· exact ((isColimitEquivIsInitialOfIsEmpty _ _ hc).to (.of (ULift ℤ))).hom.domain_nontrivial
have i := ‹Nonempty J›.some
refine ⟨c.ι.app i 0, c.ι.app i 1, fun h ↦ ?_⟩
have : IsFiltered J := ⟨⟩
obtain ⟨k, f, e⟩ := (Types.FilteredColimit.isColimit_eq_iff' (isColimitOfPreserves (forget _) hc) _ _).mp h
exact zero_ne_one (((F.map f).hom.map_zero.symm.trans e).trans (F.map f).hom.map_one)
