English
Under a similar hypothesis, for all x in the colimit, r smul x = 0 implies x = 0.
Русский
При аналогичных предпосылках для любого элемента x в колимите, если r·x=0, то x=0.
LaTeX
$$$\\forall x:\\, \\mathrm{colimit}\ F,\\; r\\cdot x=0\\Rightarrow x=0$$$
Lean4
/-- if `r` has no zero smul divisors for all small-enough sections, then `r` has no zero smul divisors
in the colimit.
-/
theorem colimit_no_zero_smul_divisor (F : J ⥤ ModuleCat.{max t w} R) [PreservesColimit F (forget (ModuleCat R))]
[IsFiltered J] [HasColimit F] (r : R) (H : ∃ (j' : J), ∀ (j : J) (_ : j' ⟶ j), ∀ (c : F.obj j), r • c = 0 → c = 0)
(x : ToType (colimit F)) (hx : r • x = 0) : x = 0 := by
classical
obtain ⟨j, x, rfl⟩ := Concrete.colimit_exists_rep F x
rw [← map_smul (colimit.ι F j).hom] at hx
obtain ⟨j', i, h⟩ := Concrete.colimit_rep_eq_zero (hx := hx)
obtain ⟨j'', H⟩ := H
simpa [elementwise_of% (colimit.w F), map_zero] using
congr(colimit.ι F _
$(H (IsFiltered.sup { j, j', j'' } {⟨j, j', by simp, by simp, i⟩}) (IsFiltered.toSup _ _ <| by simp)
(F.map (IsFiltered.toSup _ _ <| by simp) x)
(by
rw [← IsFiltered.toSup_commutes (f := i) (mY := by simp) (mf := by simp), F.map_comp, ModuleCat.comp_apply,
← map_smul, ← map_smul, h, map_zero])))
