rank_le_one_iff
theorem rank_le_one_iff :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Module.rank K V ≤ 1 ↔ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v
The theorem states that for any division ring `K` and any vector space `V` over `K`, the dimension of the vector space is at most `1` if and only if there exists a single vector `v₀` in `V` such that every vector in `V` is a scalar multiple of `v₀`. In other words, all vectors in `V` can be represented as multiples of `v₀`. This is a characterization of one-dimensional vector spaces.
More concisely: A vector space over a division ring has dimension at most 1 if and only if it is spanned by a single vector.
|
rank_dual_eq_card_dual_of_aleph0_le_rank
theorem rank_dual_eq_card_dual_of_aleph0_le_rank :
∀ {K : Type u_2} {V : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Cardinal.aleph0 ≤ Module.rank K V → Module.rank K (V →ₗ[K] K) = Cardinal.mk (V →ₗ[K] K)
The **Erdős-Kaplansky Theorem** over a field states that for any field `K` and any `V` that is an additive commutative group and a module over `K`, if the cardinality of `V` (denoted as `Module.rank K V`) is at least as large as the smallest infinite cardinal (`Cardinal.aleph0`), then the rank of the dual module (`V →ₗ[K] K`) is equal to the cardinal number of the dual module (`Cardinal.mk (V →ₗ[K] K)`). In other words, when the module `V` has an infinite dimension at least as large as `ℵ₀`, the dimension of its dual space is exactly the cardinality of the set of its linear functionals.
More concisely: For any additive commutative group and module `V` over a field `K` of infinite rank, the rank of `V`'s dual module equals its cardinality.
|
linearIndependent_iff_card_eq_finrank_span
theorem linearIndependent_iff_card_eq_finrank_span :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_2}
[inst_3 : Fintype ι] {b : ι → V}, LinearIndependent K b ↔ Fintype.card ι = Set.finrank K (Set.range b)
This theorem states that a finite family of vectors (denoted by `b` which is a function from some index set `ι` to the vector space `V` over a division ring `K`) is linearly independent if and only if the number of vectors in the family (which is the cardinality of the index set `ι`) equals the dimension of the span of these vectors. In other words, a finite set of vectors is linearly independent if and only if the dimension of the space they span is exactly the number of vectors in the set.
More concisely: A finite family of vectors is linearly independent if and only if the dimension of the span of these vectors equals their cardinality.
|
rank_add_rank_split
theorem rank_add_rank_split :
∀ {K : Type u} {V V₁ V₂ V₃ : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : AddCommGroup V₁] [inst_4 : Module K V₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module K V₂]
[inst_7 : AddCommGroup V₃] [inst_8 : Module K V₃] (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂)
(ce : V₁ →ₗ[K] V₃),
⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb →
LinearMap.ker cd = ⊥ →
db ∘ₗ cd = eb ∘ₗ ce →
(∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e) →
Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃
This theorem, `rank_add_rank_split`, is an auxiliary lemma primarily used in proving `Submodule.rank_sup_add_rank_inf_eq`. It states that for any division ring `K` and modules `V`, `V₁`, `V₂`, `V₃` over `K`, given four linear maps — `db` from `V₂` to `V`, `eb` from `V₃` to `V`, `cd` from `V₁` to `V₂`, and `ce` from `V₁` to `V₃` — if the following conditions are met:
1. the supremum of the ranges of `db` and `eb` is greater than or equal to the top element (`⊤`),
2. the kernel of `cd` is the bottom element (`⊥`),
3. the composition of `db` and `cd` is equal to the composition of `eb` and `ce`,
4. for every pair of elements `d` from `V₂` and `e` from `V₃`, if `db` of `d` equals `eb` of `e`, then there exists an element `c` from `V₁` such that `cd` of `c` equals `d` and `ce` of `c` equals `e`.
Then, the sum of the ranks of `V` and `V₁` is equal to the sum of the ranks of `V₂` and `V₃`.
More concisely: Given a division ring `K` and modules `V₁`, `V₂`, `V₃` over `K` with linear maps `db : V₂ → V`, `eb : V₃ → V`, `cd : V₁ → V₂`, and `ce : V₁ → V₃` such that the supremum of `db` and `eb` is greater than or equal to the top element, the kernel of `cd` is the bottom element, `db ∘ cd = eb ∘ ce`, and for every `d ∈ V₂` and `e ∈ V₃` with `db d = eb e`, there exists `c ∈ V₁` with `cd c = d` and `ce c = e`, then the ranks of `V` and `V₁` equal the sum of the ranks of `V₂` and `V₃`.
|
rank_submodule_le_one_iff
theorem rank_submodule_le_one_iff :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(s : Submodule K V), Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ Submodule.span K {v₀}
The theorem `rank_submodule_le_one_iff` states that for a given submodule `s` of a module `V` over a division ring `K`, the dimension of `s` is at most `1` if and only if there exists a single vector `v₀` in the submodule `s` such that `s` is contained in the span of `{v₀}`. Here, the span of a set `s` is understood to be the smallest submodule that contains `s`, and the 'dimension' of a submodule is the rank of the module. In other words, a submodule is one-dimensional if it can be generated by a single vector.
More concisely: A submodule of a module over a division ring has dimension at most 1 if and only if it is contained in the span of a single vector.
|
rank_submodule_le_one_iff'
theorem rank_submodule_le_one_iff' :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
(s : Submodule K V), Module.rank K ↥s ≤ 1 ↔ ∃ v₀, s ≤ Submodule.span K {v₀}
This theorem states that for any given submodule `s` of a module `V` over a division ring `K`, the dimension of the submodule (also known as its rank) is at most `1` if and only if there exists a single vector `v₀` (which does not necessarily have to be in the submodule itself) such that the submodule `s` is contained within the span of `v₀`. The span of a set, in this case `{v₀}`, is the smallest submodule of `V` that contains the set.
More concisely: The dimension of a submodule of a vector space is at most 1 if and only if it is contained in the span of a single vector.
|
rank_dual_eq_card_dual_of_aleph0_le_rank'
theorem rank_dual_eq_card_dual_of_aleph0_le_rank' :
∀ {K : Type u} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Cardinal.aleph0 ≤ Module.rank K V → Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = Cardinal.mk (V →ₗ[K] K)
This is the Erdős-Kaplansky Theorem, which states that for any infinite-dimensional vector space over a division ring, if the dimension of the vector space (also known as its rank) is at least as large as the smallest infinite cardinal number, also known as aleph-null (`ℵ₀`), then the dimension of the dual vector space (the space of all linear maps from the vector space to the division ring) is equal to the cardinality of the set of such linear maps.
More concisely: For an infinite-dimensional vector space over a division ring, if its dimension is greater than or equal to the first uncountable cardinal number, then the dimension of its dual space equals the cardinality of the space of all linear maps.
|
Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0
theorem Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0 :
∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Module.rank K V < Cardinal.aleph0 → (Basis.ofVectorSpaceIndex K V).Finite
This theorem states that if a vector space has a finite dimension, then the index set of its basis, as defined by the function `Basis.ofVectorSpace`, is also finite. Here, the dimension of the vector space is represented by `Module.rank K V`. The theorem specifies that if the rank of the module, i.e., the dimension of the vector space, is less than `Cardinal.aleph0` (the smallest infinite cardinal number, representing countable infinity), then the index set of the basis of the vector space is finite.
More concisely: A finite-dimensional vector space over a field has a finite basis.
|
max_aleph0_card_le_rank_fun_nat
theorem max_aleph0_card_le_rank_fun_nat :
∀ (K : Type u) [inst : DivisionRing K], max Cardinal.aleph0 (Cardinal.mk K) ≤ Module.rank K (ℕ → K)
This theorem is a key lemma towards the Erdős-Kaplansky theorem. It states that for any type `K` that forms a division ring, the maximum of the smallest infinite cardinal number (`ℵ₀`) and the cardinal number of `K` is less than or equal to the rank of the module of functions from natural numbers to `K`. In other words, the size of the set of all functions from natural numbers to any division ring is always greater than or equal to the maximum of the size of the set of natural numbers and the size of the set that forms the division ring.
More concisely: For any division ring `K`, the cardinality of `K` and `ℵ₀` is dominated by the cardinality of the set of functions from natural numbers to `K`.
|