Finite dimensional vector spaces #
This file defines finite dimensional vector spaces and shows our definition is equivalent to alternative definitions.
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
):
Module.finBasis
andModule.finBasisOfFinrankEq
are bases for finite dimensional vector spaces, where the index type isFin
(inMathlib.LinearAlgebra.Dimension.Free
)fintypeBasisIndex
states that a finite-dimensional vector space has a finite basisof_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-dimensionalityof_finrank_pos
states that a nonzero finrank (implying non-infinite dimension) 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
) - linear equivs, in
LinearEquiv.finiteDimensional
Implementation notes #
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.
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.
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.
This is a shortcut instance to simplify inference in the presence of [FiniteDimensional K V]
.
A quotient of a finite-dimensional space is also finite-dimensional.
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
.
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.
A submodule is finitely generated if and only if it is finite-dimensional
Finite dimensionality is preserved under linear equivalence.