# 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: if P holds for ⊥ : Submodule R M and if P N follows from P N' for all N' that are of lower rank, then P holds on all submodules

• Submodule.exists_basis_of_pid: if R is a PID, then N : Submodule R M is free and finitely generated. This is the first part of the structure theorem for modules.

• Submodule.smithNormalForm: if R is a PID, then M has a basis bM and N has a basis bN such that bN i = a i • bM i. Equivalently, a linear map f : M →ₗ M with range f = N can be written as a matrix in Smith normal form, a diagonal matrix with the coefficients a i along the diagonal.

## Tags #

free module, finitely generated module, rank, structure theorem

theorem eq_bot_of_generator_maximal_map_eq_zero {R : Type u} {M : Type v} [Ring R] [] [Module R M] {ι : Type u_1} (b : Basis ι R M) {N : } {ϕ : M →ₗ[R] R} (hϕ : ∀ (ψ : M →ₗ[R] R), ¬ < ) [(Submodule.map ϕ N).IsPrincipal] (hgen : ) :
N =
theorem eq_bot_of_generator_maximal_submoduleImage_eq_zero {R : Type u} {M : Type v} [Ring R] [] [Module R M] {ι : Type u_1} {N : } {O : } (b : Basis ι R O) (hNO : N O) {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N) [(ϕ.submoduleImage N).IsPrincipal] (hgen : Submodule.IsPrincipal.generator (ϕ.submoduleImage N) = 0) :
N =
theorem dvd_generator_iff {R : Type u_2} [] [] {I : } {x : R} (hx : x I) :
theorem generator_maximal_submoduleImage_dvd {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] {N : } {O : } (hNO : N O) {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N) [(ϕ.submoduleImage N).IsPrincipal] (y : M) (yN : y N) (ϕy_eq : ϕ y, = Submodule.IsPrincipal.generator (ϕ.submoduleImage N)) (ψ : O →ₗ[R] R) :
Submodule.IsPrincipal.generator (ϕ.submoduleImage N) ψ y,
theorem Submodule.basis_of_pid_aux {ι : Type u_1} {R : Type u_2} [] [] [] {O : Type u_4} [] [Module R O] (M : ) (N : ) (b'M : Basis ι R M) (N_bot : N ) (N_le_M : N M) :
yM, ∃ (a : R), a y N M'M, N'N, N' M' (∀ (c : R), zM', c y + z = 0c = 0) (∀ (c : R), zN', c a y + z = 0c = 0) ∀ (n' : ) (bN' : Basis (Fin n') R N'), ∃ (bN : Basis (Fin (n' + 1)) R N), ∀ (m' : ) (hn'm' : n' m') (bM' : Basis (Fin m') R M'), ∃ (hnm : n' + 1 m' + 1) (bM : Basis (Fin (m' + 1)) R M), ∀ (as : Fin n'R), (∀ (i : Fin n'), (bN' i) = as i (bM' (Fin.castLE hn'm' i)))∃ (as' : Fin (n' + 1)R), ∀ (i : Fin (n' + 1)), (bN i) = as' i (bM (Fin.castLE hnm i))

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.

theorem Submodule.nonempty_basis_of_pid {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] {ι : Type u_4} [] (b : Basis ι R M) (N : ) :
∃ (n : ), Nonempty (Basis (Fin n) R N)

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.

noncomputable def Submodule.basisOfPid {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] {ι : Type u_4} [] (b : Basis ι R M) (N : ) :
(n : ) × Basis (Fin n) R N

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
• = .choose, .some
Instances For
theorem Submodule.basisOfPid_bot {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] {ι : Type u_4} [] (b : Basis ι R M) :
= 0,
noncomputable def Submodule.basisOfPidOfLE {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] {ι : Type u_4} [] {N : } {O : } (hNO : N O) (b : Basis ι R O) :
(n : ) × Basis (Fin n) R N

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
Instances For
noncomputable def Submodule.basisOfPidOfLESpan {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] {ι : Type u_4} [] {b : ιM} (hb : ) {N : } (le : N ) :
(n : ) × Basis (Fin n) R N

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
Instances For
noncomputable def Module.basisOfFiniteTypeTorsionFree {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] [] {s : ιM} (hs : = ) [] :
(n : ) × Basis (Fin n) R M

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
theorem Module.free_of_finite_type_torsion_free {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] [] {s : ιM} (hs : = ) [] :
noncomputable def Module.basisOfFiniteTypeTorsionFree' {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] [] [] :
(n : ) × Basis (Fin n) R M

A finite type torsion free module over a PID admits a basis.

Equations
• Module.basisOfFiniteTypeTorsionFree' =
Instances For
instance Module.free_of_finite_type_torsion_free' {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] [] [] :
Equations
• =
instance instFreeSubtypeMemIdealOfFiniteOfNoZeroSMulDivisors {R : Type u_2} [] [] {S : Type u_4} [] [Algebra R S] {I : } [hI₁ : ] [hI₂ : ] :
Equations
• =
theorem Module.free_iff_noZeroSMulDivisors {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] [] :
structure Basis.SmithNormalForm {R : Type u_2} [] {M : Type u_3} [] [Module R M] (N : ) (ι : Type u_4) (n : ) :
Type (max (max u_2 u_3) u_4)

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.

• bN : Basis (Fin n) R N

The basis of N.

• f : Fin n ι

The mapping between the vectors of the bases.

• a : Fin nR

The (diagonal) entries of the matrix.

• snf : ∀ (i : Fin n), (self.bN i) = self.a i self.bM (self.f i)

The SNF relation between the vectors of the bases.

Instances For
theorem Basis.SmithNormalForm.snf {R : Type u_2} [] {M : Type u_3} [] [Module R M] {N : } {ι : Type u_4} {n : } (self : ) (i : Fin n) :
(self.bN i) = self.a i self.bM (self.f i)

The SNF relation between the vectors of the bases.

theorem Basis.SmithNormalForm.repr_eq_zero_of_nmem_range {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] {n : } {N : } (snf : ) (m : N) {i : ι} (hi : iSet.range snf.f) :
(snf.bM.repr m) i = 0
theorem Basis.SmithNormalForm.le_ker_coord_of_nmem_range {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] {n : } {N : } (snf : ) {i : ι} (hi : iSet.range snf.f) :
N LinearMap.ker (snf.bM.coord i)
@[simp]
theorem Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] {n : } {N : } (snf : ) (m : N) {i : Fin n} :
(snf.bM.repr m) (snf.f i) = (snf.bN.repr (snf.a i m)) i
@[simp]
theorem Basis.SmithNormalForm.repr_comp_embedding_eq_smul {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] {n : } {N : } (snf : ) (m : N) :
(snf.bM.repr m) snf.f = snf.a (snf.bN.repr m)
@[simp]
theorem Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] {n : } {N : } (snf : ) {i : Fin n} :
snf.bM.coord (snf.f i) ∘ₗ N.subtype = snf.a i snf.bN.coord i
@[simp]
theorem Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] {n : } {N : } (snf : ) [] [] (f : M →ₗ[R] M) (hf : ∀ (x : M), f x N) (hf' : optParam (∀ xN, f x N) ) {i : Fin n} :
(LinearMap.toMatrix snf.bN snf.bN) (f.restrict hf') i i = (LinearMap.toMatrix snf.bM snf.bM) f (snf.f i) (snf.f i)

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.

theorem Submodule.exists_smith_normal_form_of_le {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] [] (b : Basis ι R M) (N : ) (O : ) (N_le_O : N O) :
∃ (n : ) (o : ) (hno : n o) (bO : Basis (Fin o) R O) (bN : Basis (Fin n) R N) (a : Fin nR), ∀ (i : Fin n), (bN i) = a i (bO (Fin.castLE hno i))

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.

noncomputable def Submodule.smithNormalFormOfLE {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] [] (b : Basis ι R M) (N : ) (O : ) (N_le_O : N O) :
(o : ) × (n : ) × Basis.SmithNormalForm (Submodule.comap O.subtype N) (Fin o) n

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
noncomputable def Submodule.smithNormalForm {ι : Type u_1} {R : Type u_2} [] {M : Type u_3} [] [Module R M] [] [] (b : Basis ι R M) (N : ) :
(n : ) ×

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
noncomputable def Ideal.smithNormalForm {ι : Type u_1} {R : Type u_2} [] [] {S : Type u_4} [] [] [Algebra R S] [] (b : Basis ι R S) (I : ) (hI : I ) :

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
theorem Ideal.exists_smith_normal_form {ι : Type u_1} {R : Type u_2} [] [] {S : Type u_4} [] [] [Algebra R S] [] (b : Basis ι R S) (I : ) (hI : I ) :
∃ (b' : Basis ι R S) (a : ιR) (ab' : Basis ι R I), ∀ (i : ι), (ab' i) = a i b' i

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.

noncomputable def Ideal.ringBasis {ι : Type u_1} {R : Type u_2} [] [] {S : Type u_4} [] [] [Algebra R S] [] (b : Basis ι R S) (I : ) (hI : I ) :
Basis ι R S

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
Instances For
noncomputable def Ideal.selfBasis {ι : Type u_1} {R : Type u_2} [] [] {S : Type u_4} [] [] [Algebra R S] [] (b : Basis ι R S) (I : ) (hI : I ) :
Basis ι R I

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
Instances For
noncomputable def Ideal.smithCoeffs {ι : Type u_1} {R : Type u_2} [] [] {S : Type u_4} [] [] [Algebra R S] [] (b : Basis ι R S) (I : ) (hI : I ) :
ιR

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
• = .choose
Instances For
@[simp]
theorem Ideal.selfBasis_def {ι : Type u_1} {R : Type u_2} [] [] {S : Type u_4} [] [] [Algebra R S] [] (b : Basis ι R S) (I : ) (hI : I ) (i : ι) :
((Ideal.selfBasis b I hI) i) = Ideal.smithCoeffs b I hI i (Ideal.ringBasis b I hI) i

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.

@[simp]
theorem Ideal.smithCoeffs_ne_zero {ι : Type u_1} {R : Type u_2} [] [] {S : Type u_4} [] [] [Algebra R S] [] (b : Basis ι R S) (I : ) (hI : I ) (i : ι) :
theorem LinearIndependent.restrict_scalars_algebras {R : Type u_1} {S : Type u_2} {M : Type u_3} {ι : Type u_4} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (hinj : Function.Injective (algebraMap R S)) {v : ιM} (li : ) :

A set of linearly independent vectors in a module M over a semiring S is also linearly independent over a subring R of K.