Documentation

Mathlib.LinearAlgebra.Dimension.DivisionRing

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

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

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) :

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) :
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} :

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

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) :
Basis ι K V

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

Equations
Instances For
    @[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
    @[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 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) :
    Basis { x : V // x s } K V

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

    Equations
    Instances For
      @[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)
      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) :
      Basis (↑s) K V

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

      Equations
      Instances For

        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)

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

        The Erdős-Kaplansky Theorem over a field.