English
In a Noetherian module, a sequence of submodules (f(n)) with the property that each successive partial supremum is disjoint from the next f(n+1) eventually stabilizes at zero; more precisely there exists n such that f(m) = 0 for all m ≥ n.
Русский
В Нетереоновом модуле последовательность подпрострам (f(n)) с условием, что частичные верхние пределы попарно непересекаются с следующими f(n+1), в конечном итоге становится нулевой; существует n such, что f(m) = 0 для всех m ≥ n.
LaTeX
$$$\exists n:\mathbb{N}, \forall m \ge n, f(m) = \bot$$$
Lean4
/-- A sequence `f` of submodules of a Noetherian module,
with `f (n+1)` disjoint from the supremum of `f 0`, ..., `f n`,
is eventually zero. -/
theorem disjoint_partialSups_eventually_bot (f : ℕ → Submodule R M) (h : ∀ n, Disjoint (partialSups f n) (f (n + 1))) :
∃ n : ℕ, ∀ m, n ≤ m → f m = ⊥ := by
-- A little off-by-one cleanup first:
suffices t : ∃ n : ℕ, ∀ m, n ≤ m → f (m + 1) = ⊥ by
obtain ⟨n, w⟩ := t
use n + 1
rintro (_ | m) p
· cases p
· apply w
exact Nat.succ_le_succ_iff.mp p
obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance (partialSups f)
refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩
simpa only [partialSups_add_one] using (w (m + 1) <| le_add_right p).symm.trans <| w m p
