Mathlib.FieldTheory.Finiteness

IsNoetherian.iff_rank_lt_aleph0 theorem

: IsNoetherian K V ↔ Module.rank K V < ℵ₀

Full source

/-- 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 : IsNoetherianIsNoetherian 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]

Noetherian Module Characterization over Division Rings: $\text{IsNoetherian}\,K\,V \leftrightarrow \text{rank}_K V < \aleph_0$

Informal description

A module $V$ over a division ring $K$ is Noetherian if and only if its dimension (as a cardinal number) is strictly less than $\aleph_0$, the first infinite cardinal. In other words, $\text{IsNoetherian}\,K\,V \leftrightarrow \text{rank}_K V < \aleph_0$.

IsNoetherian.fintypeBasisIndex definition

{ι : Type*} [IsNoetherian K V] (b : Basis ι K V) : Fintype ι

Full source

/-- In a noetherian module over a division ring, all bases are indexed by a finite type. -/
noncomputable def fintypeBasisIndex {ι : Type*} [IsNoetherian K V] (b : Basis ι K V) : Fintype ι :=
  b.fintypeIndexOfRankLtAleph0 (rank_lt_aleph0 K V)

Finiteness of basis index set for Noetherian modules over division rings

Informal description

Given a vector space $ V $ over a division ring $ K $ that is Noetherian, and a basis $ b $ indexed by a type $ \iota $, the index set $ \iota $ is finite. In other words, every basis of a Noetherian module over a division ring is indexed by a finite set.

IsNoetherian.instFintypeElemOfVectorSpaceIndex instance

[IsNoetherian K V] : Fintype (Basis.ofVectorSpaceIndex K V)

Full source

/-- In a noetherian module over a division ring,
`Basis.ofVectorSpace` is indexed by a finite type. -/
noncomputable instance [IsNoetherian K V] : Fintype (Basis.ofVectorSpaceIndex K V) :=
  fintypeBasisIndex (Basis.ofVectorSpace K V)

Finiteness of Basis Index Set in Noetherian Vector Spaces

Informal description

For a vector space $V$ over a division ring $K$, if $V$ is Noetherian, then the indexing set of the basis obtained from `Basis.ofVectorSpace` is finite.

IsNoetherian.finite_basis_index theorem

{ι : Type*} {s : Set ι} [IsNoetherian K V] (b : Basis s K V) : s.Finite

Full source

/-- In a noetherian module over a division ring,
if a basis is indexed by a set, that set is finite. -/
theorem finite_basis_index {ι : Type*} {s : Set ι} [IsNoetherian K V] (b : Basis s K V) :
    s.Finite :=
  b.finite_index_of_rank_lt_aleph0 (rank_lt_aleph0 K V)

Finiteness of Basis Index Set in Noetherian Modules over Division Rings

Informal description

Let $V$ be a Noetherian module over a division ring $K$, and let $b$ be a basis for $V$ indexed by a subset $s$ of a type $\iota$. Then the indexing set $s$ is finite.

IsNoetherian.finsetBasisIndex definition

[IsNoetherian K V] : Finset V

Full source

/-- In a noetherian module over a division ring,
there exists a finite basis. This is the indexing `Finset`. -/
noncomputable def finsetBasisIndex [IsNoetherian K V] : Finset V :=
  (finite_basis_index (Basis.ofVectorSpace K V)).toFinset

Finite basis indexing set for a Noetherian module

Informal description

Given a Noetherian module $V$ over a division ring $K$, this definition constructs a finite indexing set (as a `Finset`) for a basis of $V$ as a vector space. The basis is obtained by extending the empty set to a maximal linearly independent subset of $V$ and then converting this finite set to a `Finset`.

IsNoetherian.coe_finsetBasisIndex theorem

[IsNoetherian K V] : (↑(finsetBasisIndex K V) : Set V) = Basis.ofVectorSpaceIndex K V

Full source

@[simp]
theorem coe_finsetBasisIndex [IsNoetherian K V] :
    (↑(finsetBasisIndex K V) : Set V) = Basis.ofVectorSpaceIndex K V :=
  Set.Finite.coe_toFinset _

Equality of Basis Indexing Sets in Noetherian Modules

Informal description

For a Noetherian module $V$ over a division ring $K$, the underlying set of the finite basis indexing set `finsetBasisIndex K V` is equal to the indexing set `Basis.ofVectorSpaceIndex K V` used to construct a basis for $V$ as a vector space.

IsNoetherian.coeSort_finsetBasisIndex theorem

[IsNoetherian K V] : (finsetBasisIndex K V : Type _) = Basis.ofVectorSpaceIndex K V

Full source

@[simp]
theorem coeSort_finsetBasisIndex [IsNoetherian K V] :
    (finsetBasisIndex K V : Type _) = Basis.ofVectorSpaceIndex K V :=
  Set.Finite.coeSort_toFinset _

Equality of Basis Indexing Types for Noetherian Modules

Informal description

For a Noetherian module $V$ over a division ring $K$, the type of elements in the finite basis indexing set `finsetBasisIndex K V` is equal to the type of elements in the indexing set `Basis.ofVectorSpaceIndex K V` used to construct a basis for $V$ as a vector space.

IsNoetherian.finsetBasis definition

[IsNoetherian K V] : Basis (finsetBasisIndex K V) K V

Full source

/-- 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`.
-/
noncomputable def finsetBasis [IsNoetherian K V] : Basis (finsetBasisIndex K V) K V :=
  (Basis.ofVectorSpace K V).reindex (by rw [coeSort_finsetBasisIndex])

Finite basis for a Noetherian module over a division ring

Informal description

Given a Noetherian module $V$ over a division ring $K$, the function constructs a basis for $V$ indexed by the finite set `finsetBasisIndex K V`. This basis is obtained by reindexing the basis constructed via `Basis.ofVectorSpace K V` using the equality of the indexing types provided by `coeSort_finsetBasisIndex`.

IsNoetherian.range_finsetBasis theorem

[IsNoetherian K V] : Set.range (finsetBasis K V) = Basis.ofVectorSpaceIndex K V

Full source

@[simp]
theorem range_finsetBasis [IsNoetherian K V] :
    Set.range (finsetBasis K V) = Basis.ofVectorSpaceIndex K V := by
  rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]

Range of Finite Basis Vectors Equals Indexing Set in Noetherian Module

Informal description

For a Noetherian module $V$ over a division ring $K$, the range of the basis vectors in the finite basis constructed by `finsetBasis K V` is equal to the indexing set `Basis.ofVectorSpaceIndex K V` used to construct a basis for $V$ as a vector space.

Module.card_eq_pow_finrank theorem

[Fintype K] [Fintype V] : Fintype.card V = Fintype.card K ^ Module.finrank K V

Full source

theorem _root_.Module.card_eq_pow_finrank [Fintype K] [Fintype V] :
    Fintype.card V = Fintype.card K ^ Module.finrank K V := by
  let b := IsNoetherian.finsetBasis K V
  rw [Module.card_fintype b, ← Module.finrank_eq_card_basis b]

Cardinality of Finite Vector Space over Division Ring: $|V| = |K|^{\dim_K V}$

Informal description

Let $K$ be a finite division ring and $V$ a finite-dimensional vector space over $K$. Then the cardinality of $V$ is equal to the cardinality of $K$ raised to the power of the dimension of $V$ over $K$, i.e., $|V| = |K|^{\dim_K V}$.

Module.natCard_eq_pow_finrank theorem

[Module.Finite K V] : Nat.card V = Nat.card K ^ finrank K V

Full source

theorem _root_.Module.natCard_eq_pow_finrank [Module.Finite K V] :
    Nat.card V = Nat.card K ^ finrank K V := by
  let b := IsNoetherian.finsetBasis K V
  rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, finrank_eq_nat_card_basis b]

Cardinality of Finitely Generated Module over Division Ring as Power of Base Cardinality

Informal description

For a finitely generated module $V$ over a division ring $K$, the cardinality of $V$ (as a natural number) is equal to the cardinality of $K$ raised to the power of the finite rank of $V$ over $K$. That is, \[ \mathrm{card}(V) = \mathrm{card}(K)^{\mathrm{finrank}_K(V)}. \]

IsNoetherian.iff_fg theorem

: IsNoetherian K V ↔ Module.Finite K V

Full source

/-- A module over a division ring is noetherian if and only if it is finitely generated. -/
theorem iff_fg : IsNoetherianIsNoetherian K V ↔ Module.Finite K V := by
  constructor
  · intro h
    exact
      ⟨⟨finsetBasisIndex K V, by
          convert (finsetBasis K V).span_eq
          simp⟩⟩
  · rintro ⟨s, hs⟩
    rw [IsNoetherian.iff_rank_lt_aleph0, ← rank_top, ← hs]
    exact lt_of_le_of_lt (rank_span_le _) s.finite_toSet.lt_aleph0

Noetherian Module Characterization over Division Rings: Finitely Generated if and only if Noetherian

Informal description

A module $V$ over a division ring $K$ is Noetherian if and only if it is finitely generated.