English
In a Noetherian module, the index set of any basis is finite; the map fintypeBasisIndex assigns finite index to a basis.
Русский
В противном случае, в негеодостаточной модуле множество индексов базиса конечно; отображение fintypeBasisIndex приписывает базису конечный индекс.
LaTeX
$$$$ \\text{If } [IsNoetherian\\ K\\ V] \\\\text{ then } \\text{Basis.ofVectorSpace } K V \\text{ has finite index.} $$$$
Lean4
/-- A module over a division ring is Noetherian if and only if
its dimension (as a cardinal) is strictly less than the first infinite cardinal `ℵ₀`.
-/
theorem iff_rank_lt_aleph0 : IsNoetherian K V ↔ Module.rank K V < ℵ₀ :=
by
let b := Basis.ofVectorSpace K V
rw [← b.mk_eq_rank'', lt_aleph0_iff_set_finite]
constructor
· intro
exact (Basis.ofVectorSpaceIndex.linearIndependent K V).set_finite_of_isNoetherian
· intro hbfinite
refine @isNoetherian_of_linearEquiv K (⊤ : Submodule K V) V _ _ _ _ _ (LinearEquiv.ofTop _ rfl) (id ?_)
refine isNoetherian_of_fg_of_noetherian _ ⟨Set.Finite.toFinset hbfinite, ?_⟩
rw [Set.Finite.coe_toFinset, ← b.span_eq, Basis.coe_ofVectorSpace, Subtype.range_coe]
