Finite dimensional vector spaces #
Basic properties of finite dimensional vector spaces, of their dimensions, and of linear maps on such spaces.
Main definitions #
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
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 #
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
.
If a submodule has maximal dimension in a finite dimensional space, then it is equal to the whole space.
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
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, FiniteDimensional 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 sort is finite-dimensional.
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.
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 (x : ℚ≥0) => HMul.hMul ↑x) ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯
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 forward direction of Subalgebra.finiteDimensional_toSubmodule
.
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.