Dimension of vector spaces

In this file we provide results about Module.rank and FiniteDimensional.finrank of vector spaces over division rings.

Main statements

For vector spaces (i.e. modules over a field), we have

• rank_quotient_add_rank: if V₁ is a submodule of V, then Module.rank (V/V₁) + Module.rank V₁ = Module.rank V.
• rank_range_add_rank_ker: the rank-nullity theorem.
• rank_dual_eq_card_dual_of_aleph0_le_rank: The Erdős-Kaplansky Theorem which says that the dimension of an infinite-dimensional dual space over a division ring has dimension equal to its cardinality.

theorem Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0 {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : Module.rank K V < Cardinal.aleph0) : Set.Finite (Basis.ofVectorSpaceIndex K V)

If a vector space has a finite dimension, the index set of Basis.ofVectorSpace is finite.

theorem rank_quotient_add_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (p : Submodule K V) : Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

theorem rank_range_add_rank_ker {K : Type u} {V : Type v} {V₁ : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₁] [Module K V₁] (f : V →ₗ[K] V₁) : Module.rank K ↥(LinearMap.range f) + Module.rank K ↥(LinearMap.ker f) = Module.rank K V

The rank-nullity theorem

theorem rank_eq_of_surjective {K : Type u} {V : Type v} {V₁ : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₁] [Module K V₁] (f : V →ₗ[K] V₁) (h : Function.Surjective ⇑f) : Module.rank K V = Module.rank K V₁ + Module.rank K ↥(LinearMap.ker f)

theorem exists_linearIndependent_cons_of_lt_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {v : Fin n → V} (hv : LinearIndependent K v) (h : ↑n < Module.rank K V) : ∃ (x : V), LinearIndependent K (Fin.cons x v)

Given a family of n linearly independent vectors in a space of dimension > n, one may extend the family by another vector while retaining linear independence.

theorem exists_linearIndependent_snoc_of_lt_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {v : Fin n → V} (hv : LinearIndependent K v) (h : ↑n < Module.rank K V) : ∃ (x : V), LinearIndependent K (Fin.snoc v x)

Given a family of n linearly independent vectors in a space of dimension > n, one may extend the family by another vector while retaining linear independence.

theorem exists_linearIndependent_pair_of_one_lt_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : 1 < Module.rank K V) {x : V} (hx : x ≠ 0) : ∃ (y : V), LinearIndependent K ![x, y]

Given a nonzero vector in a space of dimension > 1, one may find another vector linearly independent of the first one.

theorem rank_add_rank_split {K : Type u} {V : Type v} {V₁ : Type v} {V₂ : Type v} {V₃ : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [AddCommGroup V₁] [Module K V₁] [AddCommGroup V₂] [Module K V₂] [AddCommGroup V₃] [Module K V₃] (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd : V₁ →ₗ[K] V₂) (ce : V₁ →ₗ[K] V₃) (hde : ⊤ ≤ LinearMap.range db ⊔ LinearMap.range eb) (hgd : LinearMap.ker cd = ⊥) (eq : db ∘ₗ cd = eb ∘ₗ ce) (eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ (c : V₁), cd c = d ∧ ce c = e) : Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

This is mostly an auxiliary lemma for Submodule.rank_sup_add_rank_inf_eq.

theorem Submodule.rank_sup_add_rank_inf_eq {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) (t : Submodule K V) : Module.rank K ↥(s ⊔ t) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t

theorem Submodule.rank_add_le_rank_add_rank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) (t : Submodule K V) : Module.rank K ↥(s ⊔ t) ≤ Module.rank K ↥s + Module.rank K ↥t

def Basis.ofRankEqZero {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [IsEmpty ι] (hV : Module.rank K V = 0) : Basis ι K V

The ι indexed basis on V, where ι is an empty type and V is zero-dimensional.

See also FiniteDimensional.finBasis.

Equations

• Basis.ofRankEqZero hV = Basis.empty V

@[simp]

theorem Basis.ofRankEqZero_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [IsEmpty ι] (hV : Module.rank K V = 0) (i : ι) : (Basis.ofRankEqZero hV) i = 0

theorem le_rank_iff_exists_linearIndependent {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {c : Cardinal.{v}} : c ≤ Module.rank K V ↔ ∃ (s : Set V), Cardinal.mk ↑s = c ∧ LinearIndependent (ι := { x : V // x ∈ s }) K Subtype.val

theorem le_rank_iff_exists_linearIndependent_finset {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} : ↑n ≤ Module.rank K V ↔ ∃ (s : Finset V), s.card = n ∧ LinearIndependent (ι := { x : V // x ∈ ↑s }) K Subtype.val

theorem rank_le_one_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] : Module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v

A vector space has dimension at most 1 if and only if there is a single vector of which all vectors are multiples.

theorem rank_submodule_le_one_iff {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) : Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ Submodule.span K {v₀}

A submodule has dimension at most 1 if and only if there is a single vector in the submodule such that the submodule is contained in its span.

theorem rank_submodule_le_one_iff' {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (s : Submodule K V) : Module.rank K ↥s ≤ 1 ↔ ∃ (v₀ : V), s ≤ Submodule.span K {v₀}

A submodule has dimension at most 1 if and only if there is a single vector, not necessarily in the submodule, such that the submodule is contained in its span.

theorem Submodule.rank_le_one_iff_isPrincipal {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (W : Submodule K V) : Module.rank K ↥W ≤ 1 ↔ Submodule.IsPrincipal W

theorem Module.rank_le_one_iff_top_isPrincipal {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] : Module.rank K V ≤ 1 ↔ Submodule.IsPrincipal ⊤

theorem exists_linearIndependent_snoc_of_lt_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {v : Fin n → V} (hv : LinearIndependent K v) (h : n < FiniteDimensional.finrank K V) : ∃ (x : V), LinearIndependent K (Fin.snoc v x)

Given a family of n linearly independent vectors in a finite-dimensional space of dimension > n, one may extend the family by another vector while retaining linear independence.

theorem exists_linearIndependent_cons_of_lt_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {n : ℕ} {v : Fin n → V} (hv : LinearIndependent K v) (h : n < FiniteDimensional.finrank K V) : ∃ (x : V), LinearIndependent K (Fin.cons x v)

Given a family of n linearly independent vectors in a finite-dimensional space of dimension > n, one may extend the family by another vector while retaining linear independence.

theorem exists_linearIndependent_pair_of_one_lt_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] (h : 1 < FiniteDimensional.finrank K V) {x : V} (hx : x ≠ 0) : ∃ (y : V), LinearIndependent K ![x, y]

Given a nonzero vector in a finite-dimensional space of dimension > 1, one may find another vector linearly independent of the first one.

theorem linearIndependent_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [Fintype ι] {b : ι → V} (spans : ⊤ ≤ Submodule.span K (Set.range b)) (card_eq : Fintype.card ι = FiniteDimensional.finrank K V) : LinearIndependent K b

theorem linearIndependent_iff_card_eq_finrank_span {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [Fintype ι] {b : ι → V} : LinearIndependent K b ↔ Fintype.card ι = Set.finrank K (Set.range b)

A finite family of vectors is linearly independent if and only if its cardinality equals the dimension of its span.

theorem linearIndependent_iff_card_le_finrank_span {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [Fintype ι] {b : ι → V} : LinearIndependent K b ↔ Fintype.card ι ≤ Set.finrank K (Set.range b)

noncomputable def basisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [Fintype ι] (b : ι → V) (le_span : ⊤ ≤ Submodule.span K (Set.range b)) (card_eq : Fintype.card ι = FiniteDimensional.finrank K V) : Basis ι K V

A family of finrank K V vectors forms a basis if they span the whole space.

Equations

• basisOfTopLeSpanOfCardEqFinrank b le_span card_eq = Basis.mk ⋯ le_span

@[simp]

theorem coe_basisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {ι : Type u_2} [Fintype ι] (b : ι → V) (le_span : ⊤ ≤ Submodule.span K (Set.range b)) (card_eq : Fintype.card ι = FiniteDimensional.finrank K V) : ⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b

@[simp]

theorem finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (le_span : ⊤ ≤ Submodule.span K ↑s) (card_eq : s.card = FiniteDimensional.finrank K V) : ∀ (a : V), (finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = (LinearIndependent.repr ⋯) ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a)

noncomputable def finsetBasisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Finset V} (le_span : ⊤ ≤ Submodule.span K ↑s) (card_eq : s.card = FiniteDimensional.finrank K V) : Basis { x : V // x ∈ s } K V

A finset of finrank K V vectors forms a basis if they span the whole space.

Equations

• finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq = basisOfTopLeSpanOfCardEqFinrank Subtype.val ⋯ ⋯

@[simp]

theorem setBasisOfTopLeSpanOfCardEqFinrank_repr_apply {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Fintype ↑s] (le_span : ⊤ ≤ Submodule.span K s) (card_eq : (Set.toFinset s).card = FiniteDimensional.finrank K V) : ∀ (a : V), (setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a = (LinearIndependent.repr ⋯) ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a)

noncomputable def setBasisOfTopLeSpanOfCardEqFinrank {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} [Fintype ↑s] (le_span : ⊤ ≤ Submodule.span K s) (card_eq : (Set.toFinset s).card = FiniteDimensional.finrank K V) : Basis (↑s) K V

A set of finrank K V vectors forms a basis if they span the whole space.

Equations

• setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq = basisOfTopLeSpanOfCardEqFinrank Subtype.val ⋯ ⋯

theorem max_aleph0_card_le_rank_fun_nat (K : Type u) [DivisionRing K] : max Cardinal.aleph0 (Cardinal.mk K) ≤ Module.rank K (ℕ → K)

Key lemma towards the Erdős-Kaplansky theorem from https://mathoverflow.net/a/168624

theorem rank_fun_infinite {K : Type u} [DivisionRing K] {ι : Type v} [hι : Infinite ι] : Module.rank K (ι → K) = Cardinal.mk (ι → K)

theorem rank_dual_eq_card_dual_of_aleph0_le_rank' {K : Type u} [DivisionRing K] {V : Type u_2} [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) : Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = Cardinal.mk (V →ₗ[K] K)

The Erdős-Kaplansky Theorem: the dual of an infinite-dimensional vector space over a division ring has dimension equal to its cardinality.

theorem rank_dual_eq_card_dual_of_aleph0_le_rank {K : Type u_2} {V : Type u_3} [Field K] [AddCommGroup V] [Module K V] (h : 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.

theorem lift_rank_lt_rank_dual' {K : Type u} [DivisionRing K] {V : Type v} [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) : Cardinal.lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

theorem lift_rank_lt_rank_dual {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) : Cardinal.lift.{u, v} (Module.rank K V) < Module.rank K (V →ₗ[K] K)

theorem rank_lt_rank_dual' {K : Type u} [DivisionRing K] {V : Type u} [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) : Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

theorem rank_lt_rank_dual {K : Type u} {V : Type u} [Field K] [AddCommGroup V] [Module K V] (h : Cardinal.aleph0 ≤ Module.rank K V) : Module.rank K V < Module.rank K (V →ₗ[K] K)