English
Let M be Artinian over R with Nontrivial R. If s ⊆ M is linearly independent, then s is finite.
Русский
Пусть M артинанов как R-модуль; если s ⊆ M линейно независимо, то множество s конечно.
LaTeX
$$$[Nontrivial\\ R] \\land [IsArtinian\\ R\\ M] \\Rightarrow (LinearIndependent\\ R\\ (Subtype.val : s \\to M) \\Rightarrow s.Finite)$$$
Lean4
theorem finite_of_linearIndependent [Nontrivial R] [h : IsArtinian R M] {s : Set M}
(hs : LinearIndependent R ((↑) : s → M)) : s.Finite :=
by
refine by_contradiction fun hf ↦ (RelEmbedding.wellFounded_iff_isEmpty.1 h.wf).elim' ?_
have f : ℕ ↪ s := Set.Infinite.natEmbedding s hf
have : ∀ n, (↑) ∘ f '' {m | n ≤ m} ⊆ s := by
rintro n x ⟨y, _, rfl⟩
exact (f y).2
have : ∀ a b : ℕ, a ≤ b ↔ span R (Subtype.val ∘ f '' {m | b ≤ m}) ≤ span R (Subtype.val ∘ f '' {m | a ≤ m}) :=
by
intro a b
rw [span_le_span_iff hs (this b) (this a), Set.image_subset_image_iff (Subtype.coe_injective.comp f.injective),
Set.subset_def]
simp only [Set.mem_setOf_eq]
exact ⟨fun hab x ↦ hab.trans, (· _ le_rfl)⟩
exact
⟨⟨fun n ↦ span R (Subtype.val ∘ f '' {m | n ≤ m}), fun x y ↦
by
rw [le_antisymm_iff, ← this y x, ← this x y]
exact fun ⟨h₁, h₂⟩ ↦ le_antisymm_iff.2 ⟨h₂, h₁⟩⟩,
by
intro a b
conv_rhs => rw [GT.gt, lt_iff_le_not_ge, this, this, ← lt_iff_le_not_ge]
rfl⟩
