Documentation

Mathlib.FieldTheory.Finiteness

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
@[deprecated rank_lt_aleph0]
theorem IsNoetherian.rank_lt_aleph0 (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] :
Module.rank R M < Cardinal.aleph0

Alias of rank_lt_aleph0.

The rank of a finite module is finite.

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 : Basis ι K V) :
Fintype ι

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

Equations
Instances For
    source
    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
    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 : 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.

    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
    Instances For
      source
      @[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
      source
      @[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)
      source
      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
      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 ⇑(IsNoetherian.finsetBasis K V) = Basis.ofVectorSpaceIndex 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.