mathlib3 documentation

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] [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

A finite dimensional space is nontrivial if it has positive finrank.

A finite dimensional space is nontrivial if it has finrank equal to the successor of a natural number.

A (finite dimensional) space that is a subsingleton has zero finrank.

If a vector space (or module) has a finite basis, then its dimension (or rank) is equal to the cardinality of the basis.

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]

A ring satisfying strong_rank_condition (such as a division_ring) is one-dimensional as a module over itself.

@[simp]

The vector space of functions on a fintype ι has finrank equal to the cardinality of ι.

@[simp]

The vector space of functions on fin n has finrank equal to n.

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.

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] :
@[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
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} :
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) :

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

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
@[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) :
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
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) :
basis s 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] [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) :

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

If every vector is a multiple of some v : V, then V has dimension at most one.

@[simp]
theorem subalgebra.rank_top {F : Type u_1} {E : Type u_2} [comm_ring F] [ring E] [algebra F E] :
@[simp]