Free modules over PID #
A free R
-module M
is a module with a basis over R
,
equivalently it is an R
-module linearly equivalent to ι →₀ R
for some ι
.
This file proves a submodule of a free R
-module of finite rank is also
a free R
-module of finite rank, if R
is a principal ideal domain (PID),
i.e. we have instances [IsDomain R] [IsPrincipalIdealRing R]
.
We express "free R
-module of finite rank" as a module M
which has a basis
b : ι → R
, where ι
is a Fintype
.
We call the cardinality of ι
the rank of M
in this file;
it would be equal to finrank R M
if R
is a field and M
is a vector space.
Main results #
In this section, M
is a free and finitely generated R
-module, and
N
is a submodule of M
.
Submodule.inductionOnRank
: ifP
holds for⊥ : Submodule R M
and ifP N
follows fromP N'
for allN'
that are of lower rank, thenP
holds on all submodulesSubmodule.exists_basis_of_pid
: ifR
is a PID, thenN : Submodule R M
is free and finitely generated. This is the first part of the structure theorem for modules.Submodule.smithNormalForm
: ifR
is a PID, thenM
has a basisbM
andN
has a basisbN
such thatbN i = a i • bM i
. Equivalently, a linear mapf : M →ₗ M
withrange f = N
can be written as a matrix in Smith normal form, a diagonal matrix with the coefficientsa i
along the diagonal.
Tags #
free module, finitely generated module, rank, structure theorem
The induction hypothesis of Submodule.basisOfPid
and Submodule.smithNormalForm
.
Basically, it says: let N ≤ M
be a pair of submodules, then we can find a pair of
submodules N' ≤ M'
of strictly smaller rank, whose basis we can extend to get a basis
of N
and M
. Moreover, if the basis for M'
is up to scalars a basis for N'
,
then the basis we find for M
is up to scalars a basis for N
.
For basis_of_pid
we only need the first half and can fix M = ⊤
,
for smith_normal_form
we need the full statement,
but must also feed in a basis for M
using basis_of_pid
to keep the induction going.
A submodule of a free R
-module of finite rank is also a free R
-module of finite rank,
if R
is a principal ideal domain.
This is a lemma
to make the induction a bit easier. To actually access the basis,
see Submodule.basisOfPid
.
See also the stronger version Submodule.smithNormalForm
.
A submodule of a free R
-module of finite rank is also a free R
-module of finite rank,
if R
is a principal ideal domain.
See also the stronger version Submodule.smithNormalForm
.
Equations
- Submodule.basisOfPid b N = ⟨⋯.choose, ⋯.some⟩
Instances For
A submodule inside a free R
-submodule of finite rank is also a free R
-module of finite rank,
if R
is a principal ideal domain.
See also the stronger version Submodule.smithNormalFormOfLE
.
Equations
- Submodule.basisOfPidOfLE hNO b = match Submodule.basisOfPid b (Submodule.comap O.subtype N) with | ⟨n, bN'⟩ => ⟨n, bN'.map (Submodule.comapSubtypeEquivOfLe hNO)⟩
Instances For
A submodule inside the span of a linear independent family is a free R
-module of finite rank,
if R
is a principal ideal domain.
Equations
- Submodule.basisOfPidOfLESpan hb le = Submodule.basisOfPidOfLE le (Basis.span hb)
Instances For
A finite type torsion free module over a PID admits a basis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A finite type torsion free module over a PID admits a basis.
Equations
- Module.basisOfFiniteTypeTorsionFree' = Module.basisOfFiniteTypeTorsionFree ⋯
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A Smith normal form basis for a submodule N
of a module M
consists of
bases for M
and N
such that the inclusion map N → M
can be written as a
(rectangular) matrix with a
along the diagonal: in Smith normal form.
- bM : Basis ι R M
The basis of M.
The basis of N.
The mapping between the vectors of the bases.
- a : Fin n → R
The (diagonal) entries of the matrix.
The SNF relation between the vectors of the bases.
Instances For
The SNF relation between the vectors of the bases.
Given a Smith-normal-form pair of bases for N ⊆ M
, and a linear endomorphism f
of M
that preserves N
, the diagonal of the matrix of the restriction f
to N
does not depend on
which of the two bases for N
is used.
If M
is finite free over a PID R
, then any submodule N
is free
and we can find a basis for M
and N
such that the inclusion map is a diagonal matrix
in Smith normal form.
See Submodule.smithNormalFormOfLE
for a version of this theorem that returns
a Basis.SmithNormalForm
.
This is a strengthening of Submodule.basisOfPidOfLE
.
If M
is finite free over a PID R
, then any submodule N
is free
and we can find a basis for M
and N
such that the inclusion map is a diagonal matrix
in Smith normal form.
See Submodule.exists_smith_normal_form_of_le
for a version of this theorem that doesn't
need to map N
into a submodule of O
.
This is a strengthening of Submodule.basisOfPidOfLe
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If M
is finite free over a PID R
, then any submodule N
is free
and we can find a basis for M
and N
such that the inclusion map is a diagonal matrix
in Smith normal form.
This is a strengthening of Submodule.basisOfPid
.
See also Ideal.smithNormalForm
, which moreover proves that the dimension of
an ideal is the same as the dimension of the whole ring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If S
a finite-dimensional ring extension of a PID R
which is free as an R
-module,
then any nonzero S
-ideal I
is free as an R
-submodule of S
, and we can
find a basis for S
and I
such that the inclusion map is a square diagonal
matrix.
See Ideal.exists_smith_normal_form
for a version of this theorem that doesn't
need to map I
into a submodule of R
.
This is a strengthening of Submodule.basisOfPid
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If S
a finite-dimensional ring extension of a PID R
which is free as an R
-module,
then any nonzero S
-ideal I
is free as an R
-submodule of S
, and we can
find a basis for S
and I
such that the inclusion map is a square diagonal
matrix.
See also Ideal.smithNormalForm
for a version of this theorem that returns
a Basis.SmithNormalForm
.
The definitions Ideal.ringBasis
, Ideal.selfBasis
, Ideal.smithCoeffs
are (noncomputable)
choices of values for this existential quantifier.
If S
a finite-dimensional ring extension of a PID R
which is free as an R
-module,
then any nonzero S
-ideal I
is free as an R
-submodule of S
, and we can
find a basis for S
and I
such that the inclusion map is a square diagonal
matrix; this is the basis for S
.
See Ideal.selfBasis
for the basis on I
,
see Ideal.smithCoeffs
for the entries of the diagonal matrix
and Ideal.selfBasis_def
for the proof that the inclusion map forms a square diagonal matrix.
Equations
- Ideal.ringBasis b I hI = ⋯.choose
Instances For
If S
a finite-dimensional ring extension of a PID R
which is free as an R
-module,
then any nonzero S
-ideal I
is free as an R
-submodule of S
, and we can
find a basis for S
and I
such that the inclusion map is a square diagonal
matrix; this is the basis for I
.
See Ideal.ringBasis
for the basis on S
,
see Ideal.smithCoeffs
for the entries of the diagonal matrix
and Ideal.selfBasis_def
for the proof that the inclusion map forms a square diagonal matrix.
Equations
- Ideal.selfBasis b I hI = ⋯.choose
Instances For
If S
a finite-dimensional ring extension of a PID R
which is free as an R
-module,
then any nonzero S
-ideal I
is free as an R
-submodule of S
, and we can
find a basis for S
and I
such that the inclusion map is a square diagonal
matrix; these are the entries of the diagonal matrix.
See Ideal.ringBasis
for the basis on S
,
see Ideal.selfBasis
for the basis on I
,
and Ideal.selfBasis_def
for the proof that the inclusion map forms a square diagonal matrix.
Equations
- Ideal.smithCoeffs b I hI = ⋯.choose
Instances For
If S
a finite-dimensional ring extension of a PID R
which is free as an R
-module,
then any nonzero S
-ideal I
is free as an R
-submodule of S
, and we can
find a basis for S
and I
such that the inclusion map is a square diagonal
matrix.
A set of linearly independent vectors in a module M
over a semiring S
is also linearly
independent over a subring R
of K
.