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

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

source
noncomputable def IsNoetherian.fintypeBasisIndex {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_1} [IsNoetherian K V] (b : Module.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 ⋯

Instances For

source
noncomputable instance IsNoetherian.instFintypeElemOfVectorSpaceIndex {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] :
Fintype ↑(Module.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 (Module.Basis.ofVectorSpace K V)

source
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 : Module.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.

source
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

Instances For

source
@[simp]
theorem IsNoetherian.coe_finsetBasisIndex (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] :
↑(finsetBasisIndex K V) = Module.Basis.ofVectorSpaceIndex K V
source
@[simp]
theorem IsNoetherian.coeSort_finsetBasisIndex (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] :
↥(finsetBasisIndex K V) = ↑(Module.Basis.ofVectorSpaceIndex K V)
source
noncomputable def IsNoetherian.finsetBasis (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] :
Module.Basis (↥(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 = (Module.Basis.ofVectorSpace K V).reindex (⋯.mpr (Equiv.refl ↑(Module.Basis.ofVectorSpaceIndex K V)))

Instances For

source
@[simp]
theorem IsNoetherian.range_finsetBasis (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] [IsNoetherian K V] :
Set.range ⇑(finsetBasis K V) = Module.Basis.ofVectorSpaceIndex K V
source
theorem Module.card_eq_pow_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [Fintype K] [Fintype V] :
Fintype.card V = Fintype.card K ^ finrank K V
source
theorem Module.natCard_eq_pow_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [Module.Finite K V] :
Nat.card V = Nat.card K ^ finrank K V
source
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.