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:
- it admits a finite basis.
- it is finitely generated.
- it is noetherian, i.e., every subspace is finitely generated.
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):
exists_is_basis_finitestates that a finite-dimensional vector space has a finite basisof_finite_basisstates that the existence of a finite basis implies finite-dimensionalityiff_fgstates that the space is finite-dimensional if and only if it is finitely generated
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
- submodules
- quotients (for the dimension of a quotient, see
findim_quotient_add_findim) - linear equivs, in
linear_equiv.finite_dimensionalandlinear_equiv.findim_eq - image under a linear map (the rank-nullity formula is in
findim_range_add_findim_ker)
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.
finite_dimensional vector spaces are defined to be noetherian modules.
Use finite_dimensional.iff_fg or finite_dimensional.of_finite_basis to prove finite dimension
from a conventional definition.
Equations
- finite_dimensional K V = is_noetherian K V
Instances
- finite_dimensional.finite_dimensional_submodule
- finite_dimensional.finite_dimensional_quotient
- finite_dimensional.finite_dimensional_fintype_fun
- finite_dimensional.finite_dimensional
- linear_map.finite_dimensional_range
- matrix.finite_dimensional
- euclidean_space.finite_dimensional
- finite_dimensional_direction_affine_span_of_fintype
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.
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.
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.
If a vector space has a finite basis, then it is finite-dimensional.
If a vector space has a finite basis, then it is finite-dimensional, finset style.
A subspace of a finite-dimensional space is also finite-dimensional.
Equations
- _ = _
A quotient of a finite-dimensional space is also finite-dimensional.
Equations
- _ = _
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
- finite_dimensional.findim K V = dite (vector_space.dim K V < cardinal.omega) (λ (h : vector_space.dim K V < cardinal.omega), classical.some _) (λ (h : ¬vector_space.dim K V < cardinal.omega), 0)
In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its findim.
If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the cardinality of the basis.
If a vector space has a finite basis, then its dimension is equal to the cardinality of the basis.
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.
A finite dimensional space has positive findim iff it has a nonzero element.
A finite dimensional space has positive findim iff it is nontrivial.
A nontrivial finite dimensional space has positive findim.
If a finset has cardinality larger than the dimension of the space, then there is a nontrivial linear relation amongst its elements.
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.
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.
A field is one-dimensional as a vector space over itself.
The vector space of functions on a fintype has finite dimension.
Equations
- _ = _
The vector space of functions on a fintype ι has findim equal to the cardinality of ι.
The vector space of functions on fin n has findim equal to n.
The submodule generated by a finite set is finite-dimensional.
The submodule generated by a single element is finite-dimensional.
Equations
- _ = _
A submodule is finitely generated if and only if it 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.
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
Finite dimensionality is preserved under linear equivalence.
The dimension of a finite dimensional space is preserved under linear equivalence.
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.
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.
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.
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.
The image under an onto linear map of a finite-dimensional space is also finite-dimensional.
The range of a linear map defined on a finite-dimensional space is also finite-dimensional.
Equations
- _ = _
rank-nullity theorem : the dimensions of the kernel and the range of a linear map add up to the dimension of the source space.
The linear equivalence corresponging to an injective endomorphism.
Equations
- linear_equiv.of_injective_endo f h_inj = (linear_equiv.of_injective f h_inj).trans (linear_equiv.of_top f.range _)
An integral domain that is module-finite as an algebra over a field is a field.
Equations
- field_of_finite_dimensional F K = {add := integral_domain.add _inst_7, add_assoc := _, zero := integral_domain.zero _inst_7, zero_add := _, add_zero := _, neg := integral_domain.neg _inst_7, add_left_neg := _, add_comm := _, mul := integral_domain.mul _inst_7, mul_assoc := _, one := integral_domain.one _inst_7, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := λ (x : K), dite (x = 0) (λ (H : x = 0), 0) (λ (H : ¬x = 0), classical.some _), exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}