Theorems · Theorem · commutative algebra

Ring.DirectLimit.of.zero_exact

∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f' : (i j : ι) → i ≤ j → G i →+* G j} [DirectedSystem G fun i j h => ⇑(f' i j h)] [IsDirectedOrder ι] {i : ι}
  {x : G i}, (Ring.DirectLimit.of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) i) x = 0 → ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

A component that corresponds to zero in the direct limit is already zero in some bigger module in the directed system.

Defined in

Mathlib.Algebra.Colimit.Ring

Cited by

0 results in Mathlib

Foundations

Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderCommRingDirectedSystemIsDirectedOrder