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

theorem IsNoetherian.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

The dimension of a noetherian module over a division ring, 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 = Basis.fintypeIndexOfRankLtAleph0 b (_ : Module.rank K V < Cardinal.aleph0)

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) : Set.Finite s

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 = Set.Finite.toFinset (_ : Set.Finite (Basis.ofVectorSpaceIndex K V))

@[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 // 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 // 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 FiniteDimensional.finsetBasisIndex. This is in contrast to the result finite_basis_index (Basis.ofVectorSpace K V), which provides a set and a Set.finite.

Equations

• One or more equations did not get rendered due to their size.

@[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.