Finite dimension of vector spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Definition of the rank of a module, or dimension of a vector space, as a natural number.
Main definitions #
Defined is finite_dimensional.finrank, the dimension of a finite dimensional space, returning a
nat, as opposed to module.rank, which returns a cardinal. When the space has infinite
dimension, its finrank is by convention set to 0.
The definition of finrank does not assume a finite_dimensional instance, but lemmas might.
Import linear_algebra.finite_dimensional to get access to these additional lemmas.
Formulas for the dimension are given for linear equivs, in linear_equiv.finrank_eq
Implementation notes #
Most results are deduced from the corresponding results for the general dimension (as a cardinal),
in dimension.lean. Not all results have been ported yet.
You should not assume that there has been any effort to state lemmas as generally as possible.
noncomputable
def
finite_dimensional.finrank
(R : Type u_1)
(V : Type u_2)
[semiring R]
[add_comm_group V]
[module R V] :
The rank of a module as a natural number.
Defined by convention to be 0 if the space has infinite rank.
For a vector space V over a field K, this is the same as the finite dimension
of V over K.
Equations
theorem
finite_dimensional.finrank_eq_of_rank_eq
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
{n : ℕ}
(h : module.rank K V = ↑n) :
finite_dimensional.finrank K V = n
theorem
finite_dimensional.finrank_le_of_rank_le
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
{n : ℕ}
(h : module.rank K V ≤ ↑n) :
finite_dimensional.finrank K V ≤ n
theorem
finite_dimensional.finrank_lt_of_rank_lt
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
{n : ℕ}
(h : module.rank K V < ↑n) :
finite_dimensional.finrank K V < n
theorem
finite_dimensional.rank_lt_of_finrank_lt
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
{n : ℕ}
(h : n < finite_dimensional.finrank K V) :
↑n < module.rank K V
theorem
finite_dimensional.finrank_le_finrank_of_rank_le_rank
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
(h : (module.rank K V).lift ≤ (module.rank K V₂).lift)
(h' : module.rank K V₂ < cardinal.aleph_0) :
theorem
finite_dimensional.nontrivial_of_finrank_pos
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
[nontrivial K]
[no_zero_smul_divisors K V]
(h : 0 < finite_dimensional.finrank K V) :
A finite dimensional space is nontrivial if it has positive finrank.
theorem
finite_dimensional.nontrivial_of_finrank_eq_succ
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
[nontrivial K]
[no_zero_smul_divisors K V]
{n : ℕ}
(hn : finite_dimensional.finrank K V = n.succ) :
A finite dimensional space is nontrivial if it has finrank equal to the successor of a
natural number.
theorem
finite_dimensional.finrank_zero_of_subsingleton
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
[nontrivial K]
[no_zero_smul_divisors K V]
[h : subsingleton V] :
finite_dimensional.finrank K V = 0
A (finite dimensional) space that is a subsingleton has zero finrank.
theorem
finite_dimensional.finrank_eq_card_basis
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
[strong_rank_condition K]
{ι : Type w}
[fintype ι]
(h : basis ι K V) :
If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the cardinality of the basis.
theorem
finite_dimensional.finrank_eq_card_finset_basis
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
[strong_rank_condition K]
{ι : Type w}
{b : finset ι}
(h : basis ↥b K V) :
finite_dimensional.finrank K V = b.card
If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the
cardinality of the basis. This lemma uses a finset instead of indexed types.
@[simp]
theorem
finite_dimensional.finrank_self
(K : Type u)
[ring K]
[strong_rank_condition K] :
finite_dimensional.finrank K K = 1
A ring satisfying strong_rank_condition (such as a division_ring) is one-dimensional as a
module over itself.
@[simp]
theorem
finite_dimensional.finrank_fintype_fun_eq_card
(K : Type u)
[ring K]
[strong_rank_condition K]
{ι : Type v}
[fintype ι] :
finite_dimensional.finrank K (ι → K) = fintype.card ι
The vector space of functions on a fintype ι has finrank equal to the cardinality of ι.
@[simp]
theorem
finite_dimensional.finrank_fin_fun
(K : Type u)
[ring K]
[strong_rank_condition K]
{n : ℕ} :
finite_dimensional.finrank K (fin n → K) = n
The vector space of functions on fin n has finrank equal to n.
theorem
finite_dimensional.basis.subset_extend
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{s : set V}
(hs : linear_independent K coe) :
theorem
finrank_eq_zero_of_basis_imp_not_finite
{K : Type u}
{V : Type v}
[ring K]
[strong_rank_condition K]
[add_comm_group V]
[module K V]
[module.free K V]
(h : ∀ (s : set V), basis ↥s K V → ¬s.finite) :
finite_dimensional.finrank K V = 0
theorem
finrank_eq_zero_of_basis_imp_false
{K : Type u}
{V : Type v}
[ring K]
[strong_rank_condition K]
[add_comm_group V]
[module K V]
[module.free K V]
(h : ∀ (s : finset V), basis ↥↑s K V → false) :
finite_dimensional.finrank K V = 0
theorem
finrank_eq_zero_of_not_exists_basis
{K : Type u}
{V : Type v}
[ring K]
[strong_rank_condition K]
[add_comm_group V]
[module K V]
[module.free K V]
(h : ¬∃ (s : finset V), nonempty (basis ↥↑s K V)) :
finite_dimensional.finrank K V = 0
theorem
finrank_eq_zero_of_not_exists_basis_finite
{K : Type u}
{V : Type v}
[ring K]
[strong_rank_condition K]
[add_comm_group V]
[module K V]
[module.free K V]
(h : ¬∃ (s : set V) (b : basis ↥s K V), s.finite) :
finite_dimensional.finrank K V = 0
theorem
finrank_eq_zero_of_not_exists_basis_finset
{K : Type u}
{V : Type v}
[ring K]
[strong_rank_condition K]
[add_comm_group V]
[module K V]
[module.free K V]
(h : ¬∃ (s : finset V), nonempty (basis ↥s K V)) :
finite_dimensional.finrank K V = 0
theorem
linear_equiv.finrank_eq
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M ≃ₗ[R] M₂) :
The dimension of a finite dimensional space is preserved under linear equivalence.
theorem
linear_equiv.finrank_map_eq
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M ≃ₗ[R] M₂)
(p : submodule R M) :
Pushforwards of finite-dimensional submodules along a linear_equiv have the same finrank.
theorem
linear_map.finrank_range_of_inj
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
{V₂ : Type v'}
[add_comm_group V₂]
[module K V₂]
{f : V →ₗ[K] V₂}
(hf : function.injective ⇑f) :
The dimensions of the domain and range of an injective linear map are equal.
@[simp]
theorem
finrank_bot
(K : Type u)
(V : Type v)
[ring K]
[add_comm_group V]
[module K V]
[nontrivial K] :
@[simp]
theorem
submodule.lt_of_le_of_finrank_lt_finrank
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
{s t : submodule K V}
(le : s ≤ t)
(lt : finite_dimensional.finrank K ↥s < finite_dimensional.finrank K ↥t) :
s < t
theorem
submodule.lt_top_of_finrank_lt_finrank
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
{s : submodule K V}
(lt : finite_dimensional.finrank K ↥s < finite_dimensional.finrank K V) :
@[protected]
noncomputable
def
set.finrank
(K : Type u)
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
(s : set V) :
The rank of a set of vectors as a natural number.
Equations
- set.finrank K s = finite_dimensional.finrank K ↥(submodule.span K s)
theorem
finrank_span_le_card
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
(s : set V)
[fintype ↥s] :
finite_dimensional.finrank K ↥(submodule.span K s) ≤ s.to_finset.card
theorem
finrank_span_finset_le_card
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
(s : finset V) :
set.finrank K ↑s ≤ s.card
theorem
finrank_range_le_card
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
{b : ι → V} :
set.finrank K (set.range b) ≤ fintype.card ι
theorem
finrank_span_eq_card
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
{b : ι → V}
(hb : linear_independent K b) :
finite_dimensional.finrank K ↥(submodule.span K (set.range b)) = fintype.card ι
theorem
finrank_span_set_eq_card
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
(s : set V)
[fintype ↥s]
(hs : linear_independent K coe) :
finite_dimensional.finrank K ↥(submodule.span K s) = s.to_finset.card
theorem
finrank_span_finset_eq_card
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
(s : finset V)
(hs : linear_independent K coe) :
finite_dimensional.finrank K ↥(submodule.span K ↑s) = s.card
theorem
span_lt_of_subset_of_card_lt_finrank
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{s : set V}
[fintype ↥s]
{t : submodule K V}
(subset : s ⊆ ↑t)
(card_lt : s.to_finset.card < finite_dimensional.finrank K ↥t) :
submodule.span K s < t
theorem
span_lt_top_of_card_lt_finrank
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{s : set V}
[fintype ↥s]
(card_lt : s.to_finset.card < finite_dimensional.finrank K V) :
submodule.span K s < ⊤
theorem
linear_independent_of_top_le_span_of_card_eq_finrank
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
{b : ι → V}
(spans : ⊤ ≤ submodule.span K (set.range b))
(card_eq : fintype.card ι = finite_dimensional.finrank K V) :
theorem
linear_independent_iff_card_eq_finrank_span
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
{b : ι → V} :
linear_independent 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
linear_independent_iff_card_le_finrank_span
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
{b : ι → V} :
linear_independent K b ↔ fintype.card ι ≤ set.finrank K (set.range b)
noncomputable
def
basis_of_top_le_span_of_card_eq_finrank
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
(b : ι → V)
(le_span : ⊤ ≤ submodule.span K (set.range b))
(card_eq : fintype.card ι = finite_dimensional.finrank K V) :
basis ι K V
A family of finrank K V vectors forms a basis if they span the whole space.
Equations
- basis_of_top_le_span_of_card_eq_finrank b le_span card_eq = basis.mk _ le_span
@[simp]
theorem
coe_basis_of_top_le_span_of_card_eq_finrank
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
[fintype ι]
(b : ι → V)
(le_span : ⊤ ≤ submodule.span K (set.range b))
(card_eq : fintype.card ι = finite_dimensional.finrank K V) :
⇑(basis_of_top_le_span_of_card_eq_finrank b le_span card_eq) = b
noncomputable
def
finset_basis_of_top_le_span_of_card_eq_finrank
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{s : finset V}
(le_span : ⊤ ≤ submodule.span K ↑s)
(card_eq : s.card = finite_dimensional.finrank K V) :
A finset of finrank K V vectors forms a basis if they span the whole space.
Equations
- finset_basis_of_top_le_span_of_card_eq_finrank le_span card_eq = basis_of_top_le_span_of_card_eq_finrank coe _ _
@[simp]
theorem
finset_basis_of_top_le_span_of_card_eq_finrank_repr_apply
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{s : finset V}
(le_span : ⊤ ≤ submodule.span K ↑s)
(card_eq : s.card = finite_dimensional.finrank K V)
(ᾰ : V) :
⇑((finset_basis_of_top_le_span_of_card_eq_finrank le_span card_eq).repr) ᾰ = ⇑(_.repr) (⇑(linear_map.cod_restrict (submodule.span K (set.range coe)) linear_map.id _) ᾰ)
@[simp]
theorem
set_basis_of_top_le_span_of_card_eq_finrank_repr_apply
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{s : set V}
[fintype ↥s]
(le_span : ⊤ ≤ submodule.span K s)
(card_eq : s.to_finset.card = finite_dimensional.finrank K V)
(ᾰ : V) :
⇑((set_basis_of_top_le_span_of_card_eq_finrank le_span card_eq).repr) ᾰ = ⇑(_.repr) (⇑(linear_map.cod_restrict (submodule.span K (set.range coe)) linear_map.id _) ᾰ)
noncomputable
def
set_basis_of_top_le_span_of_card_eq_finrank
{K : Type u}
{V : Type v}
[division_ring K]
[add_comm_group V]
[module K V]
{s : set V}
[fintype ↥s]
(le_span : ⊤ ≤ submodule.span K s)
(card_eq : s.to_finset.card = finite_dimensional.finrank K V) :
A set of finrank K V vectors forms a basis if they span the whole space.
Equations
- set_basis_of_top_le_span_of_card_eq_finrank le_span card_eq = basis_of_top_le_span_of_card_eq_finrank coe _ _
We now give characterisations of finrank K V = 1 and finrank K V ≤ 1.
theorem
finrank_eq_one
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
[no_zero_smul_divisors K V]
[strong_rank_condition K]
(v : V)
(n : v ≠ 0)
(h : ∀ (w : V), ∃ (c : K), c • v = w) :
finite_dimensional.finrank K V = 1
If there is a nonzero vector and every other vector is a multiple of it, then the module has dimension one.
theorem
finrank_le_one
{K : Type u}
{V : Type v}
[ring K]
[add_comm_group V]
[module K V]
[no_zero_smul_divisors K V]
[strong_rank_condition K]
(v : V)
(h : ∀ (w : V), ∃ (c : K), c • v = w) :
finite_dimensional.finrank K V ≤ 1
If every vector is a multiple of some v : V, then V has dimension at most one.
@[simp]
theorem
subalgebra.rank_to_submodule
{F : Type u_1}
{E : Type u_2}
[comm_ring F]
[ring E]
[algebra F E]
(S : subalgebra F E) :
module.rank F ↥(⇑subalgebra.to_submodule S) = module.rank F ↥S
@[simp]
theorem
subalgebra.finrank_to_submodule
{F : Type u_1}
{E : Type u_2}
[comm_ring F]
[ring E]
[algebra F E]
(S : subalgebra F E) :
theorem
subalgebra_top_rank_eq_submodule_top_rank
{F : Type u_1}
{E : Type u_2}
[comm_ring F]
[ring E]
[algebra F E] :
module.rank F ↥⊤ = module.rank F ↥⊤
theorem
subalgebra_top_finrank_eq_submodule_top_finrank
{F : Type u_1}
{E : Type u_2}
[comm_ring F]
[ring E]
[algebra F E] :
theorem
subalgebra.rank_top
{F : Type u_1}
{E : Type u_2}
[comm_ring F]
[ring E]
[algebra F E] :
module.rank F ↥⊤ = module.rank F E
@[simp]
theorem
subalgebra.rank_bot
{F : Type u_1}
{E : Type u_2}
[comm_ring F]
[ring E]
[algebra F E]
[strong_rank_condition F]
[no_zero_smul_divisors F E]
[nontrivial E] :
module.rank F ↥⊥ = 1
@[simp]
theorem
subalgebra.finrank_bot
{F : Type u_1}
{E : Type u_2}
[comm_ring F]
[ring E]
[algebra F E]
[strong_rank_condition F]
[no_zero_smul_divisors F E]
[nontrivial E] :