Dimension of vector spaces

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

Main statements

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

• rank_quotient_add_rank_of_divisionRing: 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.

See also Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean for the Erdős-Kaplansky theorem.

theorem Module.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) : (ofVectorSpaceIndex K V).Finite

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

theorem rank_quotient_add_rank_of_divisionRing {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

Also see rank_quotient_add_rank.

instance DivisionRing.hasRankNullity {K : Type u} [DivisionRing K] : HasRankNullity.{u₀, u} K

theorem rank_add_rank_split {K : Type u} {V V₁ 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 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 ι = Module.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 ι = Module.finrank K V) : Module.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 = Module.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 ι = Module.finrank K V) : ⇑(basisOfTopLeSpanOfCardEqFinrank b le_span card_eq) = b

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 = Module.finrank K V) : Module.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 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 = Module.finrank K V) (a✝ : V) : (finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a✝ = ⋯.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 : s.toFinset.card = Module.finrank K V) : Module.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 ⋯ ⋯

@[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 : s.toFinset.card = Module.finrank K V) (a✝ : V) : (setBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr a✝ = ⋯.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) a✝)