colimit_rep_eq_zero — Mathlib

English

If in a family of modules over a ring with no zero smul divisors for small-enough sections, then the colimit also has no zero smul divisors.

Русский

Если в семействе модулей над кольцом нет нулевых делителей при умножении на элементы по небольшим разделам, то и колимит не имеет таких делителей.

LaTeX

$$$\\forall R:\\, \\text{Ring},\\; F:\\, J \\to \\mathrm{ModuleCat}(R),\\; r:\\, R,\\; (\\exists j', \\forall j\\,(j'\\to j),\\forall c:\\, F.obj j,\\; r\\cdot c=0\\Rightarrow c=0)\\Rightarrow \\forall x:\\, \\mathrm{colimit}\ F,\\; r\\cdot x=0\\Rightarrow x=0$$$

Lean4

theorem colimit_rep_eq_zero (F : J ⥤ ModuleCat.{max t w} R) [PreservesColimit F (forget (ModuleCat R))] [IsFiltered J]
    [HasColimit F] (j : J) (x : F.obj j) (hx : colimit.ι F j x = 0) : ∃ (j' : J) (i : j ⟶ j'), (F.map i).hom x = 0 :=
  by
  rw [show 0 = colimit.ι F j 0 by simp, colimit_rep_eq_iff_exists] at hx
  obtain ⟨j', i, y, g⟩ := hx
  exact ⟨j', i, g ▸ by simp⟩

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