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 second point of view, i.e., as finite
. However, we prove
that all these points of view are equivalent, with the following lemmas
(in the namespace finite_dimensional
):
fintype_basis_index
states that a finite-dimensional vector space has a finite basisfinite_dimensional.fin_basis
andfinite_dimensional.fin_basis_of_finrank_eq
are bases for finite dimensional vector spaces, where the index type isfin
of_fintype_basis
states that the existence of a basis indexed by a finite type implies finite-dimensionalityof_finite_basis
states that the existence of a basis indexed by a finite set implies finite-dimensionalityis_noetherian.iff_fg
states that the space is finite-dimensional if and only if it is noetherian
Also defined is 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
.
Preservation of finite-dimensionality and formulas for the dimension are given for
- submodules
- quotients (for the dimension of a quotient, see
finrank_quotient_add_finrank
) - linear equivs, in
linear_equiv.finite_dimensional
andlinear_equiv.finrank_eq
- image under a linear map (the rank-nullity formula is in
finrank_range_add_finrank_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 linear_map.mul_eq_one_comm
and linear_map.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.
Much of this file could be generalised away from fields or division rings. You should not assume that there has been any effort to state lemmas as generally as possible.
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 finite modules.
Use finite_dimensional.of_fintype_basis
to prove finite dimension from another definition.
Equations
- finite_dimensional K V = module.finite K V
If the codomain of an injective linear map is finite dimensional, the domain must be as well.
If the domain of a surjective linear map is finite dimensional, the codomain must be as well.
A finite dimensional vector space over a finite field is finite
Equations
If a vector space has a finite basis, then it is finite-dimensional.
If a vector space is finite_dimensional
, all bases are indexed by a finite type
Equations
- finite_dimensional.fintype_basis_index b = let _inst : is_noetherian K V := finite_dimensional.fintype_basis_index._proof_1 in is_noetherian.fintype_basis_index b
If a vector space is finite_dimensional
, basis.of_vector_space
is indexed by
a finite type.
Equations
- finite_dimensional.basis.of_vector_space_index.fintype = let _inst : is_noetherian K V := finite_dimensional.basis.of_vector_space_index.fintype._proof_1 in is_noetherian.basis.of_vector_space_index.fintype
If a vector space has a basis indexed by elements of a finite set, then it is finite-dimensional.
A subspace of a finite-dimensional space is also finite-dimensional.
A quotient of a finite-dimensional space is also finite-dimensional.
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
In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its
finrank
.
We can infer finite_dimensional K V
in the presence of [fact (finrank K V = n + 1)]
. Declare
this as a local instance where needed.
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
finrank
.
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 vector space has a basis indexed by fin (finrank K V)
.
Equations
- finite_dimensional.fin_basis K V = have h : fintype.card ↥(is_noetherian.finset_basis_index K V) = finite_dimensional.finrank K V, from _, (is_noetherian.finset_basis K V).reindex (fintype.equiv_fin_of_card_eq h)
An n
-dimensional vector space has a basis indexed by fin n
.
Equations
A module with dimension 1 has a basis with one element.
Equations
A finite dimensional space has positive finrank
iff it has a nonzero element.
A finite dimensional space has positive finrank
iff it is nontrivial.
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 nontrivial finite dimensional space has positive finrank
.
A finite dimensional space has zero finrank
iff it is a subsingleton.
This is the finrank
version of dim_zero_iff
.
A finite dimensional space that is a subsingleton has zero finrank
.
If a submodule has maximal dimension in a finite dimensional space, then it is equal to the whole space.
A division_ring is one-dimensional as a vector space over itself.
The vector space of functions on a fintype ι has finrank equal to the cardinality of ι.
The vector space of functions on fin n
has finrank equal to n
.
The submodule generated by a finite set is finite-dimensional.
The submodule generated by a single element is finite-dimensional.
The submodule generated by a finset is finite-dimensional.
Pushforwards of finite-dimensional submodules are finite-dimensional.
Pushforwards of finite-dimensional submodules have a smaller finrank.
If p
is an independent family of subspaces of a finite-dimensional space V
, then the
number of nontrivial subspaces in the family p
is finite.
Equations
If p
is an independent family of subspaces of a finite-dimensional space V
, then the
number of nontrivial subspaces in the family p
is bounded above by the dimension of V
.
Note that the fintype
hypothesis required here can be provided by
complete_lattice.independent.fintype_ne_bot_of_finite_dimensional
.
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 finrank + 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.
In a vector space with dimension 1, each set {v} is a basis for v ≠ 0
.
Equations
- finite_dimensional.basis_singleton ι h v hv = let b : basis ι K V := finite_dimensional.basis_unique ι h, h_1 : ⇑(⇑(b.repr) v) inhabited.default ≠ 0 := _ in {repr := {to_fun := λ (w : V), finsupp.single inhabited.default (⇑(⇑(b.repr) w) inhabited.default / ⇑(⇑(b.repr) v) inhabited.default), map_add' := _, map_smul' := _, inv_fun := λ (f : ι →₀ K), ⇑f inhabited.default • v, left_inv := _, right_inv := _}}
A submodule is finitely generated if and only if it is finite-dimensional
A submodule contained in a finite-dimensional submodule is finite-dimensional.
The inf of two submodules, the first finite-dimensional, is finite-dimensional.
The inf of two submodules, the second finite-dimensional, is finite-dimensional.
The sup of two finite-dimensional submodules is finite-dimensional.
The submodule generated by a finite supremum of finite dimensional submodules is finite-dimensional.
Note that strictly this only needs ∀ i ∈ s, finite_dimensional K (S i)
, but that doesn't
work well with typeclass search.
The submodule generated by a supremum of finite dimensional submodules, indexed by a finite type is finite-dimensional.
The submodule generated by a supremum indexed by a proposition is finite-dimensional if the submodule is.
The dimension of a submodule is bounded by the dimension of the ambient space.
The dimension of a quotient is bounded by the dimension of the ambient space.
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 strict submodule is strictly 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.
Pushforwards of finite-dimensional submodules along a linear_equiv
have the same finrank.
Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.
Two finite-dimensional vector spaces are isomorphic if and only if they have the same (finite) dimension.
Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.
Equations
If a submodule is less than or equal to a finite-dimensional submodule with the same dimension, they are equal.
Given isomorphic subspaces p q
of vector spaces V
and V₁
respectively,
p.quotient
is isomorphic to q.quotient
.
Equations
- finite_dimensional.linear_equiv.quot_equiv_of_equiv f₁ f₂ = finite_dimensional.linear_equiv.of_finrank_eq (V ⧸ p) (V₂ ⧸ q) _
Given the subspaces p q
, if p.quotient ≃ₗ[K] q
, then q.quotient ≃ₗ[K] p
On a finite-dimensional space, an injective linear map is surjective.
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.
The dimensions of the domain and range of an injective linear map are equal.
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.
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_bijective f h_inj _
If ι
is an empty type and V
is zero-dimensional, there is a unique ι
-indexed basis.
Equations
Given a linear map f
between two vector spaces with the same dimension, if
ker f = ⊥
then linear_equiv_of_injective
is the induced isomorphism
between the two vector spaces.
Equations
- f.linear_equiv_of_injective hf hdim = linear_equiv.of_bijective f hf _
A domain that is module-finite as an algebra over a field is a division ring.
Equations
- division_ring_of_finite_dimensional F K = {add := ring.add _inst_2, add_assoc := _, zero := ring.zero _inst_2, zero_add := _, add_zero := _, nsmul := ring.nsmul _inst_2, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg _inst_2, sub := ring.sub _inst_2, sub_eq_add_neg := _, zsmul := ring.zsmul _inst_2, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast _inst_2, nat_cast := ring.nat_cast _inst_2, one := ring.one _inst_2, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul _inst_2, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow _inst_2, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := λ (x : K), dite (x = 0) (λ (H : x = 0), 0) (λ (H : ¬x = 0), classical.some _), div := div_inv_monoid.div._default ring.mul ring.mul_assoc ring.one ring.one_mul ring.mul_one ring.npow ring.npow_zero' ring.npow_succ' (λ (x : K), dite (x = 0) (λ (H : x = 0), 0) (λ (H : ¬x = 0), classical.some _)), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default ring.mul ring.mul_assoc ring.one ring.one_mul ring.mul_one ring.npow ring.npow_zero' ring.npow_succ' (λ (x : K), dite (x = 0) (λ (H : x = 0), 0) (λ (H : ¬x = 0), classical.some _)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := rat.cast_rec (div_inv_monoid.to_has_inv K), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec rat.cast_rec (distrib.to_has_mul K), qsmul_eq_mul' := _}
An integral domain that is module-finite as an algebra over a field is a field.
Equations
- field_of_finite_dimensional F K = {add := division_ring.add (division_ring_of_finite_dimensional F K), add_assoc := _, zero := division_ring.zero (division_ring_of_finite_dimensional F K), zero_add := _, add_zero := _, nsmul := division_ring.nsmul (division_ring_of_finite_dimensional F K), nsmul_zero' := _, nsmul_succ' := _, neg := division_ring.neg (division_ring_of_finite_dimensional F K), sub := division_ring.sub (division_ring_of_finite_dimensional F K), sub_eq_add_neg := _, zsmul := division_ring.zsmul (division_ring_of_finite_dimensional F K), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := division_ring.int_cast (division_ring_of_finite_dimensional F K), nat_cast := division_ring.nat_cast (division_ring_of_finite_dimensional F K), one := division_ring.one (division_ring_of_finite_dimensional F K), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := division_ring.mul (division_ring_of_finite_dimensional F K), mul_assoc := _, one_mul := _, mul_one := _, npow := division_ring.npow (division_ring_of_finite_dimensional F K), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv (division_ring_of_finite_dimensional F K), div := division_ring.div (division_ring_of_finite_dimensional F K), div_eq_mul_inv := _, zpow := division_ring.zpow (division_ring_of_finite_dimensional F K), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast (division_ring_of_finite_dimensional F K), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul (division_ring_of_finite_dimensional F K), qsmul_eq_mul' := _}
The rank of a set of vectors as a natural number.
Equations
- set.finrank K s = finite_dimensional.finrank K ↥(submodule.span K s)
A finite family of vectors is linearly independent if and only if its cardinality equals the dimension of its span.
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
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 _ _
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 _ _
A linear independent family of finrank K V
vectors forms a basis.
Equations
- basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq = basis.mk lin_ind _
A linear independent finset of finrank K V
vectors forms a basis.
Equations
- finset_basis_of_linear_independent_of_card_eq_finrank hs lin_ind card_eq = basis_of_linear_independent_of_card_eq_finrank lin_ind _
A linear independent set of finrank K V
vectors forms a basis.
Equations
- set_basis_of_linear_independent_of_card_eq_finrank lin_ind card_eq = basis_of_linear_independent_of_card_eq_finrank lin_ind _
We now give characterisations of finrank K V = 1
and 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.
If every vector is a multiple of some v : V
, then V
has dimension at most one.
A vector space with a nonzero vector v
has dimension 1 iff v
spans.
A module with a nonzero vector v
has dimension 1 iff every vector is a multiple of v
.
A module has dimension 1 iff there is some v : V
so {v}
is a basis.
A module has dimension 1 iff there is some nonzero v : V
so every vector is a multiple of v
.
A finite dimensional module has dimension at most 1 iff
there is some v : V
so every vector is a multiple of v
.