scilib documentation

field_theory.finiteness

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
theorem is_noetherian.iff_rank_lt_aleph_0 {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] :
is_noetherian K V ↔ module.rank K V < cardinal.aleph_0

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
theorem is_noetherian.rank_lt_aleph_0 (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [is_noetherian K V] :
module.rank K V < cardinal.aleph_0

The dimension of a noetherian module over a division ring, as a cardinal, is strictly less than the first infinite cardinal ℵ₀.

source
noncomputable def is_noetherian.fintype_basis_index {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} [is_noetherian K V] (b : basis ι K V) :
fintype ι

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

Equations
source
@[protected, instance]
noncomputable def is_noetherian.basis.of_vector_space_index.fintype {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] [is_noetherian K V] :
fintype ↥(basis.of_vector_space_index K V)

In a noetherian module over a division ring, basis.of_vector_space is indexed by a finite type.

Equations
source
theorem is_noetherian.finite_basis_index {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] {ι : Type u_1} {s : set ι} [is_noetherian 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.

source
noncomputable def is_noetherian.finset_basis_index (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [is_noetherian K V] :
finset V

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

Equations
source
@[simp]
theorem is_noetherian.coe_finset_basis_index (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [is_noetherian K V] :
↑(is_noetherian.finset_basis_index K V) = basis.of_vector_space_index K V
source
@[simp]
theorem is_noetherian.coe_sort_finset_basis_index (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [is_noetherian K V] :
↥(is_noetherian.finset_basis_index K V) = ↥(basis.of_vector_space_index K V)
source
noncomputable def is_noetherian.finset_basis (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [is_noetherian K V] :
basis ↥(is_noetherian.finset_basis_index K V) K V

In a noetherian module over a division ring, there exists a finite basis. This is indexed by the finset finite_dimensional.finset_basis_index. This is in contrast to the result finite_basis_index (basis.of_vector_space K V), which provides a set and a set.finite.

Equations
source
@[simp]
theorem is_noetherian.range_finset_basis (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V] [is_noetherian K V] :
set.range ⇑(is_noetherian.finset_basis K V) = basis.of_vector_space_index K V
source
theorem is_noetherian.iff_fg {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module K V] :
is_noetherian K V ↔ module.finite K V

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