Dimension of modules and vector spaces #
Main definitions #
-
The rank of a module is defined as
module.rank : cardinal
. This is defined as the supremum of the cardinalities of linearly independent subsets. -
The rank of a linear map is defined as the rank of its range.
Main statements #
linear_map.dim_le_of_injective
: the source of an injective linear map has dimension at most that of the target.linear_map.dim_le_of_surjective
: the target of a surjective linear map has dimension at most that of that source.basis_fintype_of_finite_spans
: the existence of a finite spanning set implies that any basis is finite.infinite_basis_le_maximal_linear_independent
: ifb
is an infinite basis for a moduleM
, ands
is a maximal linearly independent set, then the cardinality ofb
is bounded by the cardinality ofs
.
For modules over rings satisfying the rank condition
basis.le_span
: the cardinality of a basis is bounded by the cardinality of any spanning set
For modules over rings satisfying the strong rank condition
linear_independent_le_span
: For any linearly independent familyv : ι → M
and any finite spanning setw : set M
, the cardinality ofι
is bounded by the cardinality ofw
.linear_independent_le_basis
: Ifb
is a basis for a moduleM
, ands
is a linearly independent set, then the cardinality ofs
is bounded by the cardinality ofb
.
For modules over rings with invariant basis number (including all commutative rings and all noetherian rings)
mk_eq_mk_of_basis
: the dimension theorem, any two bases of the same vector space have the same cardinality.
For vector spaces (i.e. modules over a field), we have
dim_quotient_add_dim
: ifV₁
is a submodule ofV
, thenmodule.rank (V/V₁) + module.rank V₁ = module.rank V
.dim_range_add_dim_ker
: the rank-nullity theorem.
Implementation notes #
There is a naming discrepancy: most of the theorem names refer to dim
,
even though the definition is of module.rank
.
This reflects that module.rank
was originally called dim
, and only defined for vector spaces.
Many theorems in this file are not universe-generic when they relate dimensions
in different universes. They should be as general as they can be without
inserting lift
s. The types V
, V'
, ... all live in different universes,
and V₁
, V₂
, ... all live in the same universe.
The rank of a module, defined as a term of type cardinal
.
We define this as the supremum of the cardinalities of linearly independent subsets.
For a free module over any ring satisfying the strong rank condition (e.g. left-noetherian rings, commutative rings, and in particular division rings and fields), this is the same as the dimension of the space (i.e. the cardinality of any basis).
In particular this agrees with the usual notion of the dimension of a vector space.
The definition is marked as protected to avoid conflicts with _root_.rank
,
the rank of a linear map.
Equations
- module.rank K V = ⨆ (ι : {s // linear_independent K coe}), cardinal.mk ↥(ι.val)
Two linearly equivalent vector spaces have the same dimension, a version with different universes.
Two linearly equivalent vector spaces have the same dimension.
Pushforwards of submodules along a linear_equiv
have the same dimension.
A linearly-independent family of vectors in a module over a non-trivial ring must be finite if the module is Noetherian.
Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
Equations
Over any ring R
, if b
is a basis for a module M
,
and s
is a maximal linearly independent set,
then the union of the supports of x ∈ s
(when written out in the basis b
) is all of b
.
Over any ring R
, if b
is an infinite basis for a module M
,
and s
is a maximal linearly independent set,
then the cardinality of b
is bounded by the cardinality of s
.
Over any ring R
, if b
is an infinite basis for a module M
,
and s
is a maximal linearly independent set,
then the cardinality of b
is bounded by the cardinality of s
.
The dimension theorem: if v
and v'
are two bases, their index types
have the same cardinalities.
Given two bases indexed by ι
and ι'
of an R
-module, where R
satisfies the invariant
basis number property, an equiv ι ≃ ι'
.
Equations
- v.index_equiv v' = _.some
An auxiliary lemma for basis.le_span
.
If R
satisfies the rank condition,
then for any finite basis b : basis ι R M
,
and any finite spanning set w : set M
,
the cardinality of ι
is bounded by the cardinality of w
.
Another auxiliary lemma for basis.le_span
, which does not require assuming the basis is finite,
but still assumes we have a finite spanning set.
If R
satisfies the rank condition,
then the cardinality of any basis is bounded by the cardinality of any spanning set.
If R
satisfies the strong rank condition,
then any linearly independent family v : ι → M
contained in the span of some finite w : set M
,
is itself finite.
Equations
If R
satisfies the strong rank condition,
then for any linearly independent family v : ι → M
contained in the span of some finite w : set M
,
the cardinality of ι
is bounded by the cardinality of w
.
If R
satisfies the strong rank condition,
then for any linearly independent family v : ι → M
and any finite spanning set w : set M
,
the cardinality of ι
is bounded by the cardinality of w
.
An auxiliary lemma for linear_independent_le_basis
:
we handle the case where the basis b
is infinite.
Over any ring R
satisfying the strong rank condition,
if b
is a basis for a module M
,
and s
is a linearly independent set,
then the cardinality of s
is bounded by the cardinality of b
.
In an n
-dimensional space, the rank is at most m
.
Over any ring R
satisfying the strong rank condition,
if b
is an infinite basis for a module M
,
then every maximal linearly independent set has the same cardinality as b
.
This proof (along with some of the lemmas above) comes from Les familles libres maximales d'un module ont-elles le meme cardinal?
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 module has a finite dimension, all bases are indexed by a finite type.
If a module has a finite dimension, all bases are indexed by a finite type.
Equations
If a module has a finite dimension, all bases are indexed by a finite set.
If N
is a submodule in a free, finitely generated module,
do induction on adjoining a linear independent element to a submodule.
Equations
- submodule.induction_on_rank b P ih N = submodule.induction_on_rank_aux b P ih (fintype.card ι) N _
If S
a finite-dimensional ring extension of R
which is free as an R
-module,
then the rank of an ideal I
of S
over R
is the same as the rank of S
.
If a vector space has a finite dimension, the index set of basis.of_vector_space
is finite.
Two vector spaces are isomorphic if they have the same dimension.
Two vector spaces are isomorphic if they have the same dimension.
Two vector spaces are isomorphic if they have the same dimension.
Equations
- linear_equiv.of_lift_dim_eq V V' cond = classical.choice _
Two vector spaces are isomorphic if they have the same dimension.
Equations
- linear_equiv.of_dim_eq V V₁ cond = classical.choice _
Two vector spaces are isomorphic if and only if they have the same dimension.
Two vector spaces are isomorphic if and only if they have the same dimension.
rank-nullity theorem
This is mostly an auxiliary lemma for dim_sup_add_dim_inf_eq
.
rank f
is the rank of a linear_map f
, defined as the dimension of f.range
.
Equations
- rank f = module.rank K ↥(linear_map.range f)
The ι
indexed basis on V
, where ι
is an empty type and V
is zero-dimensional.
See also finite_dimensional.fin_basis
.
Equations
A vector space has dimension at most 1
if and only if there is a
single vector of which all vectors are multiples.
A submodule has dimension at most 1
if and only if there is a
single vector in the submodule such that the submodule is contained in
its span.
A submodule has dimension at most 1
if and only if there is a
single vector, not necessarily in the submodule, such that the
submodule is contained in its span.