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 division ring 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 FiniteDimensional K V
capturing this property. For ease of transfer of
proof, it is defined using the second point of view, i.e., as Module.Finite
. However, we prove
that all these points of view are equivalent, with the following lemmas
(in the namespace FiniteDimensional
):
fintypeBasisIndex
states that a finite-dimensional vector space has a finite basisModule.finBasis
andModule.finBasisOfFinrankEq
are bases for finite dimensional vector spaces, where the index type isFin
(inMathlib.LinearAlgebra.Dimension.Free
)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-dimensionalityIsNoetherian.iff_fg
states that the space is finite-dimensional if and only if it is noetherian (inMathlib.FieldTheory.Finiteness
)
We make use of 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
. finrank
is not defined using FiniteDimensional
.
For basic results that do not need the FiniteDimensional
class, import
Mathlib.LinearAlgebra.Finrank
.
Preservation of finite-dimensionality and formulas for the dimension are given for
- submodules (
FiniteDimensional.finiteDimensional_submodule
) - quotients (for the dimension of a quotient, see
Submodule.finrank_quotient_add_finrank
inMathlib.LinearAlgebra.FiniteDimensional
) - linear equivs, in
LinearEquiv.finiteDimensional
- image under a linear map (the rank-nullity formula is in
LinearMap.finrank_range_add_finrank_ker
inMathlib.LinearAlgebra.FiniteDimensional
)
Basic properties of linear maps of a finite-dimensional vector space are given. Notably, the
equivalence of injectivity and surjectivity is proved in LinearMap.injective_iff_surjective
,
and the equivalence between left-inverse and right-inverse in LinearMap.mul_eq_one_comm
and LinearMap.comp_eq_id_comm
.
Implementation notes #
Most results are deduced from the corresponding results for the general dimension (as a cardinal),
in Mathlib.LinearAlgebra.Dimension
. Not all results have been ported yet.
You should not assume that there has been any effort to state lemmas as generally as possible.
Plenty of the results hold for general fg modules or notherian modules, and they can be found in
Mathlib.LinearAlgebra.FreeModule.Finite.Rank
and Mathlib.RingTheory.Noetherian
.
FiniteDimensional
vector spaces are defined to be finite modules.
Use FiniteDimensional.of_fintype_basis
to prove finite dimension from another definition.
Equations
- FiniteDimensional K V = Module.Finite K V
Instances For
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.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A finite dimensional vector space over a finite field is finite
Equations
Instances For
If a vector space has a finite basis, then it is finite-dimensional.
If a vector space is FiniteDimensional
, all bases are indexed by a finite type
Equations
Instances For
If a vector space is FiniteDimensional
, Basis.ofVectorSpace
is indexed by
a finite type.
Equations
- FiniteDimensional.instFintypeElemOfVectorSpaceIndex = inferInstance
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.
Equations
- ⋯ = ⋯
A quotient of a finite-dimensional space is also finite-dimensional.
Equations
- ⋯ = ⋯
We can infer FiniteDimensional K V
in the presence of [Fact (finrank K V = n + 1)]
. Declare
this as a local instance where needed.
In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its
finrank
. This is a copy of finrank_eq_rank _ _
which creates easier typeclass searches.
If a vector space is finite-dimensional, then the cardinality of any basis is equal to its
finrank
.
If a submodule has maximal dimension in a finite dimensional space, then it is equal to the whole space.
Equations
- ⋯ = ⋯
The submodule generated by a finite set is finite-dimensional.
The submodule generated by a single element is finite-dimensional.
Equations
- ⋯ = ⋯
The submodule generated by a finset is finite-dimensional.
Equations
- ⋯ = ⋯
Pushforwards of finite-dimensional submodules are finite-dimensional.
Equations
- ⋯ = ⋯
A slight strengthening of exists_nontrivial_relation_sum_zero_of_rank_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
- One or more equations did not get rendered due to their size.
Instances For
Alias of FiniteDimensional.of_rank_eq_nat
.
Alias of FiniteDimensional.of_rank_eq_zero
.
Alias of FiniteDimensional.of_rank_eq_one
.
Equations
- ⋯ = ⋯
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.
Equations
- ⋯ = ⋯
The inf of two submodules, the second finite-dimensional, is finite-dimensional.
Equations
- ⋯ = ⋯
The sup of two finite-dimensional submodules is finite-dimensional.
Equations
- ⋯ = ⋯
The submodule generated by a finite supremum of finite dimensional submodules is finite-dimensional.
Note that strictly this only needs ∀ i ∈ s, FiniteDimensional K (S i)
, but that doesn't
work well with typeclass search.
Equations
- ⋯ = ⋯
The submodule generated by a supremum of finite dimensional submodules, indexed by a finite sort is finite-dimensional.
Equations
- ⋯ = ⋯
Finite dimensionality is preserved under linear equivalence.
Equations
- ⋯ = ⋯
If a submodule is contained in a finite-dimensional submodule with the same or smaller dimension, they are equal.
If a submodule is contained in a finite-dimensional submodule with the same dimension, they are equal.
If a subalgebra is contained in a finite-dimensional subalgebra with the same or smaller dimension, they are equal.
If a subalgebra is contained in a finite-dimensional subalgebra with the same dimension, they are equal.
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.
Equations
- ⋯ = ⋯
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 linear equivalence corresponding to an injective endomorphism.
Equations
- LinearEquiv.ofInjectiveEndo f h_inj = LinearEquiv.ofBijective f ⋯
Instances For
If ι
is an empty type and V
is zero-dimensional, there is a unique ι
-indexed basis.
Equations
Instances For
A domain that is module-finite as an algebra over a field is a division ring.
Equations
- divisionRingOfFiniteDimensional F K = DivisionRing.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (q : ℚ≥0) => HMul.hMul ↑q) ⋯ ⋯ (fun (q : ℚ) => HMul.hMul ↑q) ⋯
Instances For
An integral domain that is module-finite as an algebra over a field is a field.
Equations
- fieldOfFiniteDimensional F K = Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ DivisionRing.qsmul ⋯
Instances For
In a one-dimensional space, any vector is a multiple of any nonzero vector
We now give characterisations of finrank K V = 1
and finrank K V ≤ 1
.
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 Subalgebra
is FiniteDimensional
iff it is FiniteDimensional
as a submodule.
Alias of the reverse direction of Subalgebra.finiteDimensional_toSubmodule
.
A Subalgebra
is FiniteDimensional
iff it is FiniteDimensional
as a submodule.
Alias of the forward direction of Subalgebra.finiteDimensional_toSubmodule
.
A Subalgebra
is FiniteDimensional
iff it is FiniteDimensional
as a submodule.
Equations
- ⋯ = ⋯