English
Finite implies Artinian again (duplicate perspective).
Русский
Финитность снова даёт артинановость.
LaTeX
$$$[Finite\\ M] \\Rightarrow IsArtinian\\ R\\ M$$$
Lean4
/-- A sequence `f` of submodules of an Artinian module,
with the supremum `f (n+1)` and the infimum of `f 0`, ..., `f n` being ⊤,
is eventually ⊤. -/
theorem disjoint_partial_infs_eventually_top (f : ℕ → Submodule R M)
(h : ∀ n, Disjoint (partialSups (OrderDual.toDual ∘ f) n) (OrderDual.toDual (f (n + 1)))) :
∃ n : ℕ, ∀ m, n ≤ m → f m = ⊤ := by
-- A little off-by-one cleanup first:
rsuffices ⟨n, w⟩ : ∃ n : ℕ, ∀ m, n ≤ m → OrderDual.toDual f (m + 1) = ⊤
· use n + 1
rintro (_ | m) p
· cases p
· apply w
exact Nat.succ_le_succ_iff.mp p
obtain ⟨n, w⟩ := monotone_stabilizes (partialSups (OrderDual.toDual ∘ 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
