mathlib3documentation

linear_algebra.finrank

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] [ 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] [ V] {n : } (h : V = n) :
theorem finite_dimensional.finrank_le_of_rank_le {K : Type u} {V : Type v} [ring K] [ V] {n : } (h : V n) :
theorem finite_dimensional.finrank_lt_of_rank_lt {K : Type u} {V : Type v} [ring K] [ V] {n : } (h : V < n) :
theorem finite_dimensional.rank_lt_of_finrank_lt {K : Type u} {V : Type v} [ring K] [ V] {n : } (h : n < ) :
n < V
theorem finite_dimensional.finrank_le_finrank_of_rank_le_rank {K : Type u} {V : Type v} [ring K] [ V] {V₂ : Type v'} [add_comm_group V₂] [ V₂] (h : V).lift V₂).lift) (h' : V₂ < cardinal.aleph_0) :
theorem finite_dimensional.nontrivial_of_finrank_pos {K : Type u} {V : Type v} [ring K] [ V] [nontrivial K] (h : 0 < ) :

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] [ V] [nontrivial K] {n : } (hn : = 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] [ V] [nontrivial K] [h : subsingleton V] :

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] [ V] {ι : Type w} [fintype ι] (h : 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] [ V] {ι : Type w} {b : finset ι} (h : 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. This lemma uses a finset instead of indexed types.

@[simp]
theorem finite_dimensional.finrank_self (K : Type u) [ring K]  :

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] {ι : Type v} [fintype ι] :
K) =

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] {n : } :
(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} [ V] {s : set V} (hs : coe) :
s hs.extend _
theorem finrank_eq_zero_of_basis_imp_not_finite {K : Type u} {V : Type v} [ring K] [ V] [ V] (h : (s : set V), K V ¬s.finite) :
theorem finrank_eq_zero_of_basis_imp_false {K : Type u} {V : Type v} [ring K] [ V] [ V] (h : (s : finset V), K V false) :
theorem finrank_eq_zero_of_not_exists_basis {K : Type u} {V : Type v} [ring K] [ V] [ V] (h : ¬ (s : finset V), nonempty (basis s K V)) :
theorem finrank_eq_zero_of_not_exists_basis_finite {K : Type u} {V : Type v} [ring K] [ V] [ V] (h : ¬ (s : set V) (b : K V), s.finite) :
theorem finrank_eq_zero_of_not_exists_basis_finset {K : Type u} {V : Type v} [ring K] [ V] [ V] (h : ¬ (s : finset V), nonempty (basis s K V)) :
theorem linear_equiv.finrank_eq {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [ring R] [add_comm_group M₂] [ M] [ 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₂] [ M] [ M₂] (f : M ≃ₗ[R] M₂) (p : 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] [ V] {V₂ : Type v'} [add_comm_group V₂] [ 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] [ V] [nontrivial K] :
@[simp]
theorem finrank_top (K : Type u) (V : Type v) [ring K] [ V] :
theorem submodule.lt_of_le_of_finrank_lt_finrank {K : Type u} {V : Type v} [ring K] [ V] {s t : V} (le : s t) (lt : < ) :
s < t
theorem submodule.lt_top_of_finrank_lt_finrank {K : Type u} {V : Type v} [ring K] [ V] {s : V} (lt : < ) :
s <
@[protected]
noncomputable def set.finrank (K : Type u) {V : Type v} [ V] (s : set V) :

The rank of a set of vectors as a natural number.

Equations
theorem finrank_span_le_card {K : Type u} {V : Type v} [ V] (s : set V) [fintype s] :
theorem finrank_span_finset_le_card {K : Type u} {V : Type v} [ V] (s : finset V) :
theorem finrank_range_le_card {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] {b : ι V} :
theorem finrank_span_eq_card {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] {b : ι V} (hb : b) :
theorem finrank_span_set_eq_card {K : Type u} {V : Type v} [ V] (s : set V) [fintype s] (hs : coe) :
theorem finrank_span_finset_eq_card {K : Type u} {V : Type v} [ V] (s : finset V) (hs : coe) :
theorem span_lt_of_subset_of_card_lt_finrank {K : Type u} {V : Type v} [ V] {s : set V} [fintype s] {t : V} (subset : s t) (card_lt : s.to_finset.card < ) :
< t
theorem span_lt_top_of_card_lt_finrank {K : Type u} {V : Type v} [ V] {s : set V} [fintype s] (card_lt : s.to_finset.card < ) :
theorem linear_independent_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] {b : ι V} (spans : (set.range b)) (card_eq : = ) :
theorem linear_independent_iff_card_eq_finrank_span {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] {b : ι V} :

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} [ V] {ι : Type u_1} [fintype ι] {b : ι V} :
noncomputable def basis_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] (b : ι V) (le_span : (set.range b)) (card_eq : = ) :
K V

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

Equations
• card_eq = le_span
@[simp]
theorem coe_basis_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {ι : Type u_1} [fintype ι] (b : ι V) (le_span : (set.range b)) (card_eq : = ) :
le_span card_eq) = b
noncomputable def finset_basis_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {s : finset V} (le_span : ) (card_eq : s.card = ) :
K V

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

Equations
@[simp]
theorem finset_basis_of_top_le_span_of_card_eq_finrank_repr_apply {K : Type u} {V : Type v} [ V] {s : finset V} (le_span : ) (card_eq : s.card = ) (ᾰ : V) :
card_eq).repr) = (_.repr) ᾰ)
@[simp]
theorem set_basis_of_top_le_span_of_card_eq_finrank_repr_apply {K : Type u} {V : Type v} [ V] {s : set V} [fintype s] (le_span : ) (card_eq : s.to_finset.card = ) (ᾰ : V) :
card_eq).repr) = (_.repr) ᾰ)
noncomputable def set_basis_of_top_le_span_of_card_eq_finrank {K : Type u} {V : Type v} [ V] {s : set V} [fintype s] (le_span : ) (card_eq : s.to_finset.card = ) :
K V

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

Equations

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] [ V] (v : V) (n : v 0) (h : (w : V), (c : K), c v = w) :

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] [ V] (v : V) (h : (w : V), (c : K), c v = w) :

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] [ E] (S : E) :
@[simp]
theorem subalgebra.finrank_to_submodule {F : Type u_1} {E : Type u_2} [comm_ring F] [ring E] [ E] (S : E) :
theorem subalgebra_top_rank_eq_submodule_top_rank {F : Type u_1} {E : Type u_2} [comm_ring F] [ring E] [ E] :
theorem subalgebra_top_finrank_eq_submodule_top_finrank {F : Type u_1} {E : Type u_2} [comm_ring F] [ring E] [ E] :
theorem subalgebra.rank_top {F : Type u_1} {E : Type u_2} [comm_ring F] [ring E] [ E] :
= E
@[simp]
theorem subalgebra.rank_bot {F : Type u_1} {E : Type u_2} [comm_ring F] [ring E] [ E] [nontrivial E] :
= 1
@[simp]
theorem subalgebra.finrank_bot {F : Type u_1} {E : Type u_2} [comm_ring F] [ring E] [ E] [nontrivial E] :