mathlib documentation

linear_algebra.finite_dimensional

Finite dimensional vector spaces

Definition and basic properties of finite dimensional vector spaces, of their dimensions, and of linear maps on such spaces.

Main definitions

Assume V is a vector space over a field K. There are (at least) three equivalent definitions of finite-dimensionality of V:

We introduce a typeclass finite_dimensional K V capturing this property. For ease of transfer of proof, it is defined using the third point of view, i.e., as is_noetherian. However, we prove that all these points of view are equivalent, with the following lemmas (in the namespace finite_dimensional):

Also defined is findim, the dimension of a finite dimensional space, returning a nat, as opposed to dim, which returns a cardinal. When the space has infinite dimension, its findim is by convention set to 0.

Preservation of finite-dimensionality and formulas for the dimension are given for

Basic properties of linear maps of a finite-dimensional vector space are given. Notably, the equivalence of injectivity and surjectivity is proved in linear_map.injective_iff_surjective, and the equivalence between left-inverse and right-inverse in mul_eq_one_comm and comp_eq_id_comm.

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.

One of the characterizations of finite-dimensionality is in terms of finite generation. This property is currently defined only for submodules, so we express it through the fact that the maximal submodule (which, as a set, coincides with the whole space) is finitely generated. This is not very convenient to use, although there are some helper functions. However, this becomes very convenient when speaking of submodules which are finite-dimensional, as this notion coincides with the fact that the submodule is finitely generated (as a submodule of the whole space). This equivalence is proved in submodule.fg_iff_finite_dimensional.

A vector space is finite-dimensional if and only if its dimension (as a cardinal) is strictly less than the first infinite cardinal omega.

The dimension of a finite-dimensional vector space, as a cardinal, is strictly less than the first infinite cardinal omega.

theorem finite_dimensional.exists_is_basis_finite (K : Type u) (V : Type v) [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] :
∃ (s : set V), is_basis K coe s.finite

theorem finite_dimensional.exists_is_basis_finset (K : Type u) (V : Type v) [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] :
∃ (b : finset V), is_basis K coe

In a finite dimensional space, there exists a finite basis. Provides the basis as a finset. This is in contrast to exists_is_basis_finite, which provides a set and a set.finite.

def finite_dimensional.fintype_of_fintype (K : Type u) (V : Type v) [field K] [add_comm_group V] [vector_space K V] [fintype K] [finite_dimensional K V] :

A finite dimensional vector space over a finite field is finite

Equations
theorem finite_dimensional.iff_fg {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] :

A vector space is finite-dimensional if and only if it is finitely generated. As the finitely-generated property is a property of submodules, we formulate this in terms of the maximal submodule, equal to the whole space as a set by definition.

theorem finite_dimensional.of_fintype_basis {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type w} [fintype ι] {b : ι → V} :

If a vector space has a finite basis, then it is finite-dimensional.

theorem finite_dimensional.of_finite_basis {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type u_1} {s : set ι} {b : s → V} :

If a vector space has a basis indexed by elements of a finite set, then it is finite-dimensional.

theorem finite_dimensional.of_finset_basis {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type u_1} {s : finset ι} {b : s → V} :

If a vector space has a finite basis, then it is finite-dimensional, finset style.

@[instance]

A subspace of a finite-dimensional space is also finite-dimensional.

@[instance]

A quotient of a finite-dimensional space is also finite-dimensional.

def finite_dimensional.findim (K : Type u_1) (V : Type v) [field K] [add_comm_group V] [vector_space K V] :

The dimension of a finite-dimensional vector space as a natural number. Defined by convention to be 0 if the space is infinite-dimensional.

Equations

In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its findim.

theorem finite_dimensional.dim_eq_card_basis {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type w} [fintype ι] {b : ι → V} :

If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the cardinality of the basis.

theorem finite_dimensional.findim_eq_card_basis {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type w} [fintype ι] {b : ι → V} :

If a vector space has a finite basis, then its dimension is equal to the cardinality of the basis.

theorem finite_dimensional.findim_eq_card_basis' {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {ι : Type w} {b : ι → V} :

If a vector space is finite-dimensional, then the cardinality of any basis is equal to its findim.

If a vector space has a finite basis, then its dimension is equal to the cardinality of the basis. This lemma uses a finset instead of indexed types.

theorem finite_dimensional.equiv_fin {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type u_1} [finite_dimensional K V] {v : ι → V} :
is_basis K v(∃ (g : fin (finite_dimensional.findim K V) ι), is_basis K (v g))

theorem finite_dimensional.fin_basis (K : Type u) (V : Type v) [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] :
∃ (v : fin (finite_dimensional.findim K V) → V), is_basis K v

theorem finite_dimensional.cardinal_mk_le_findim_of_linear_independent {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {ι : Type w} {b : ι → V} :

theorem finite_dimensional.lt_omega_of_linear_independent {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type w} [finite_dimensional K V] {v : ι → V} :

theorem finite_dimensional.not_linear_independent_of_infinite {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type w} [inf : infinite ι] [finite_dimensional K V] (v : ι → V) :

theorem finite_dimensional.findim_pos_iff_exists_ne_zero {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] :
0 < finite_dimensional.findim K V ∃ (x : V), x 0

A finite dimensional space has positive findim iff it has a nonzero element.

A finite dimensional space has positive findim iff it is nontrivial.

theorem finite_dimensional.findim_pos {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] [h : nontrivial V] :

A nontrivial finite dimensional space has positive findim.

theorem finite_dimensional.exists_nontrivial_relation_of_dim_lt_card {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {t : finset V} :
finite_dimensional.findim K V < t.card(∃ (f : V → K), ∑ (e : V) in t, f e e = 0 ∃ (x : V) (H : x t), f x 0)

If a finset has cardinality larger than the dimension of the space, then there is a nontrivial linear relation amongst its elements.

theorem finite_dimensional.exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {t : finset V} :
finite_dimensional.findim K V + 1 < t.card(∃ (f : V → K), ∑ (e : V) in t, f e e = 0 ∑ (e : V) in t, f e = 0 ∃ (x : V) (H : x t), f x 0)

If a finset has cardinality larger than findim + 1, then there is a nontrivial linear relation amongst its elements, such that the coefficients of the relation sum to zero.

theorem finite_dimensional.exists_relation_sum_zero_pos_coefficient_of_dim_succ_lt_card {L : Type u_1} [linear_ordered_field L] {W : Type v} [add_comm_group W] [vector_space L W] [finite_dimensional L W] {t : finset W} :
finite_dimensional.findim L W + 1 < t.card(∃ (f : W → L), ∑ (e : W) in t, f e e = 0 ∑ (e : W) in t, f e = 0 ∃ (x : W) (H : x t), 0 < f x)

A slight strengthening of exists_nontrivial_relation_sum_zero_of_dim_succ_lt_card available when working over an ordered field: we can ensure a positive coefficient, not just a nonzero coefficient.

If a submodule has maximal dimension in a finite dimensional space, then it is equal to the whole space.

@[simp]

A field is one-dimensional as a vector space over itself.

@[instance]
def finite_dimensional.finite_dimensional_fintype_fun (K : Type u) [field K] {ι : Type u_1} [fintype ι] :
finite_dimensional K (ι → K)

The vector space of functions on a fintype has finite dimension.

@[simp]
theorem finite_dimensional.findim_fintype_fun_eq_card (K : Type u) [field K] {ι : Type v} [fintype ι] :

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

@[simp]
theorem finite_dimensional.findim_fin_fun (K : Type u) [field K] {n : } :

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

theorem finite_dimensional.span_of_finite (K : Type u) {V : Type v} [field K] [add_comm_group V] [vector_space K V] {A : set V} :

The submodule generated by a finite set is finite-dimensional.

@[instance]
def finite_dimensional.finite_dimensional (K : Type u) {V : Type v} [field K] [add_comm_group V] [vector_space K V] (x : V) :

The submodule generated by a single element is finite-dimensional.

theorem finite_dimensional_of_dim_eq_zero {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] :

theorem finite_dimensional_of_dim_eq_one {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] :

theorem finite_dimensional_bot (K : Type u) (V : Type v) [field K] [add_comm_group V] [vector_space K V] :

@[simp]
theorem findim_bot (K : Type u) (V : Type v) [field K] [add_comm_group V] [vector_space K V] :

theorem bot_eq_top_of_dim_eq_zero {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] :

@[simp]
theorem dim_eq_zero {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {S : submodule K V} :

@[simp]
theorem findim_eq_zero {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {S : submodule K V} [finite_dimensional K S] :

theorem submodule.fg_iff_finite_dimensional {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (s : submodule K V) :

A submodule is finitely generated if and only if it is finite-dimensional

theorem submodule.finite_dimensional_of_le {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {S₁ S₂ : submodule K V} [finite_dimensional K S₂] :
S₁ S₂finite_dimensional K S₁

A submodule contained in a finite-dimensional submodule is finite-dimensional.

@[instance]
def submodule.finite_dimensional_inf_left {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (S₁ S₂ : submodule K V) [finite_dimensional K S₁] :

The inf of two submodules, the first finite-dimensional, is finite-dimensional.

@[instance]
def submodule.finite_dimensional_inf_right {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (S₁ S₂ : submodule K V) [finite_dimensional K S₂] :

The inf of two submodules, the second finite-dimensional, is finite-dimensional.

@[instance]
def submodule.finite_dimensional_sup {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (S₁ S₂ : submodule K V) [h₁ : finite_dimensional K S₁] [h₂ : finite_dimensional K S₂] :

The sup of two finite-dimensional submodules is finite-dimensional.

In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding quotient add up to the dimension of the space.

The dimension of a submodule is bounded by the dimension of the ambient space.

theorem submodule.findim_lt {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {s : submodule K V} :

The dimension of a strict submodule is strictly bounded by the dimension of the ambient space.

The dimension of a quotient is bounded by the dimension of the ambient space.

The sum of the dimensions of s + t and s ∩ t is the sum of the dimensions of s and t

theorem linear_equiv.finite_dimensional {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {V₂ : Type v'} [add_comm_group V₂] [vector_space K V₂] (f : V ≃ₗ[K] V₂) [finite_dimensional K V] :

Finite dimensionality is preserved under linear equivalence.

theorem linear_equiv.findim_eq {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {V₂ : Type v'} [add_comm_group V₂] [vector_space K V₂] (f : V ≃ₗ[K] V₂) [finite_dimensional K V] :

The dimension of a finite dimensional space is preserved under linear equivalence.

theorem finite_dimensional.eq_of_le_of_findim_eq {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {S₁ S₂ : submodule K V} [finite_dimensional K S₂] :
S₁ S₂finite_dimensional.findim K S₁ = finite_dimensional.findim K S₂S₁ = S₂

If a submodule is less than or equal to a finite-dimensional submodule with the same dimension, they are equal.

On a finite-dimensional space, an injective linear map is surjective.

On a finite-dimensional space, a linear map is injective if and only if it is surjective.

theorem linear_map.ker_eq_bot_iff_range_eq_top {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {f : V →ₗ[K] V} :

theorem linear_map.mul_eq_one_of_mul_eq_one {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {f g : V →ₗ[K] V} :
f * g = 1g * f = 1

In a finite-dimensional space, if linear maps are inverse to each other on one side then they are also inverse to each other on the other side.

theorem linear_map.mul_eq_one_comm {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {f g : V →ₗ[K] V} :
f * g = 1 g * f = 1

In a finite-dimensional space, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.

theorem linear_map.comp_eq_id_comm {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] {f g : V →ₗ[K] V} :

In a finite-dimensional space, linear maps are inverse to each other on one side if and only if they are inverse to each other on the other side.

theorem linear_map.finite_dimensional_of_surjective {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {V₂ : Type v'} [add_comm_group V₂] [vector_space K V₂] [h : finite_dimensional K V] (f : V →ₗ[K] V₂) :

The image under an onto linear map of a finite-dimensional space is also finite-dimensional.

@[instance]
def linear_map.finite_dimensional_range {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {V₂ : Type v'} [add_comm_group V₂] [vector_space K V₂] [h : finite_dimensional K V] (f : V →ₗ[K] V₂) :

The range of a linear map defined on a finite-dimensional space is also finite-dimensional.

rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to the dimension of the source space.

def linear_equiv.of_injective_endo {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] (f : V →ₗ[K] V) :
f.ker = (V ≃ₗ[K] V)

The linear equivalence corresponging to an injective endomorphism.

Equations
theorem linear_equiv.of_injective_endo_to_fun {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] (f : V →ₗ[K] V) (h_inj : f.ker = ) :

theorem linear_equiv.of_injective_endo_right_inv {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] (f : V →ₗ[K] V) (h_inj : f.ker = ) :

theorem linear_equiv.of_injective_endo_left_inv {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] (f : V →ₗ[K] V) (h_inj : f.ker = ) :

theorem linear_map.is_unit_iff {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] (f : V →ₗ[K] V) :

@[simp]
theorem findim_top {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] :

theorem alg_hom.bijective {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] [finite_dimensional F E] (ϕ : E →ₐ[F] E) :

def alg_equiv_equiv_alg_hom (F : Type u) [field F] (E : Type v) [field E] [algebra F E] [finite_dimensional F E] :
(E ≃ₐ[F] E) (E →ₐ[F] E)

Biijection between algebra equivalences and algebra homomorphisms

Equations
def field_of_finite_dimensional (F : Type u_1) (K : Type u_2) [field F] [integral_domain K] [algebra F K] [finite_dimensional F K] :

An integral domain that is module-finite as an algebra over a field is a field.

Equations
theorem submodule.findim_mono {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] [finite_dimensional K V] :

theorem submodule.lt_of_le_of_findim_lt_findim {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {s t : submodule K V} :

theorem findim_span_le_card {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (s : set V) [fin : fintype s] :

theorem findim_span_eq_card {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type u_1} [fintype ι] {b : ι → V} :

theorem findim_span_set_eq_card {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] (s : set V) [fin : fintype s] :

theorem span_lt_of_subset_of_card_lt_findim {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {s : set V} [fintype s] {t : submodule K V} :

theorem span_lt_top_of_card_lt_findim {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {s : set V} [fintype s] :

theorem linear_independent_of_span_eq_top_of_card_eq_findim {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type u_1} [fintype ι] {b : ι → V} :

theorem linear_independent_iff_card_eq_findim_span {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K 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 is_basis_of_span_eq_top_of_card_eq_findim {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type u_1} [fintype ι] {b : ι → V} :

theorem set_is_basis_of_span_eq_top_of_card_eq_findim {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {s : set V} [fintype s] :

theorem span_eq_top_of_linear_independent_of_card_eq_findim {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type u_1} [hι : nonempty ι] [fintype ι] {b : ι → V} :

theorem is_basis_of_linear_independent_of_card_eq_findim {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {ι : Type u_1} [nonempty ι] [fintype ι] {b : ι → V} :

theorem subalgebra.dim_eq_one_of_eq_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] {S : subalgebra F E} :

@[simp]
theorem subalgebra.dim_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] :

theorem subalgebra.dim_top {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] :

theorem subalgebra.finite_dimensional_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] :

@[simp]
theorem subalgebra.findim_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] :

theorem subalgebra.findim_eq_one_of_eq_bot {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] {S : subalgebra F E} :

theorem subalgebra.eq_bot_of_findim_one {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] {S : subalgebra F E} :

theorem subalgebra.eq_bot_of_dim_one {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] {S : subalgebra F E} :

@[simp]
theorem subalgebra.bot_eq_top_of_dim_eq_one {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] :

@[simp]
theorem subalgebra.bot_eq_top_of_findim_eq_one {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] :

@[simp]
theorem subalgebra.dim_eq_one_iff {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] {S : subalgebra F E} :

@[simp]
theorem subalgebra.findim_eq_one_iff {F : Type u_1} {E : Type u_2} [field F] [field E] [algebra F E] {S : subalgebra F E} :

theorem module.End.ker_pow_constant {K : Type u} {V : Type v} [field K] [add_comm_group V] [vector_space K V] {f : module.End K V} {k : } (h : linear_map.ker (f ^ k) = linear_map.ker (f ^ k.succ)) (m : ) :