A module over a division ring is noetherian if and only if it is finite.

theorem IsNoetherian.iff_rank_lt_aleph0 {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] : IsNoetherian K V ↔ Module.rank K V < Cardinal.aleph0

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 ℵ₀.

noncomputable def IsNoetherian.fintypeBasisIndex {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [IsNoetherian K V] (b : Basis ι K V) : Fintype ι

In a noetherian module over a division ring, all bases are indexed by a finite type.

Equations

• IsNoetherian.fintypeBasisIndex b = b.fintypeIndexOfRankLtAleph0 ⋯

noncomputable instance IsNoetherian.instFintypeElemOfVectorSpaceIndex {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] : Fintype ↑(Basis.ofVectorSpaceIndex K V)

In a noetherian module over a division ring, Basis.ofVectorSpace is indexed by a finite type.

Equations

• IsNoetherian.instFintypeElemOfVectorSpaceIndex = IsNoetherian.fintypeBasisIndex (Basis.ofVectorSpace K V)

theorem IsNoetherian.finite_basis_index {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} {s : Set ι} [IsNoetherian K V] (b : Basis (↑s) K V) : s.Finite

In a noetherian module over a division ring, if a basis is indexed by a set, that set is finite.

noncomputable def IsNoetherian.finsetBasisIndex (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] : Finset V

In a noetherian module over a division ring, there exists a finite basis. This is the indexing Finset.

Equations

• IsNoetherian.finsetBasisIndex K V = ⋯.toFinset

@[simp]

theorem IsNoetherian.coe_finsetBasisIndex (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] : ↑(IsNoetherian.finsetBasisIndex K V) = Basis.ofVectorSpaceIndex K V

@[simp]

theorem IsNoetherian.coeSort_finsetBasisIndex (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] : { x : V // x ∈ IsNoetherian.finsetBasisIndex K V } = ↑(Basis.ofVectorSpaceIndex K V)

noncomputable def IsNoetherian.finsetBasis (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] : Basis { x : V // x ∈ IsNoetherian.finsetBasisIndex K V } K V

In a noetherian module over a division ring, there exists a finite basis. This is indexed by the Finset IsNoetherian.finsetBasisIndex. This is in contrast to the result finite_basis_index (Basis.ofVectorSpace K V), which provides a set and a Set.Finite.

Equations

• IsNoetherian.finsetBasis K V = (Basis.ofVectorSpace K V).reindex (⋯.mpr (Equiv.refl ↑(Basis.ofVectorSpaceIndex K V)))

@[simp]

theorem IsNoetherian.range_finsetBasis (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] : Set.range ⇑(IsNoetherian.finsetBasis K V) = Basis.ofVectorSpaceIndex K V

theorem IsNoetherian.iff_fg {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] : IsNoetherian K V ↔ Module.Finite K V

A module over a division ring is noetherian if and only if it is finitely generated.