# Documentation

Mathlib.LinearAlgebra.FreeModule.PID

# 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), ¬ < ) [] (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 { x // x O }) (hNO : N O) {ϕ : { x // x O } →ₗ[R] R} (hϕ : ∀ (ψ : { x // x O } →ₗ[R] R), ) (hgen : ) :
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) {ϕ : { x // x O } →ₗ[R] R} (hϕ : ∀ (ψ : { x // x O } →ₗ[R] R), ) (y : M) (yN : y N) (ϕy_eq : ϕ { val := y, property := hNO y yN } = ) (ψ : { x // x O } →ₗ[R] R) :
ψ { val := y, property := hNO y yN }
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 { x // x M }) (N_bot : N ) (N_le_M : N M) :
y, y M a x M', M' M N', N' N _N'_le_M' _y_ortho_M' _ay_ortho_N', ∀ (n' : ) (bN' : Basis (Fin n') R { x // x N' }), bN, ∀ (m' : ) (hn'm' : n' m') (bM' : Basis (Fin m') R { x // x M' }), hnm bM, ∀ (as : Fin n'R), (∀ (i : Fin n'), ↑(bN' i) = as i ↑(bM' (Fin.castLE hn'm' i))) → as', ∀ (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 { x // x 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 { x // x 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.

Instances For
theorem Submodule.basisOfPid_bot {R : Type u_2} [] [] {M : Type u_3} [] [Module R M] {ι : Type u_4} [] (b : Basis ι R M) :
= { fst := 0, snd := Basis.empty { x // x } }
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 { x // x O }) :
(n : ) × Basis (Fin n) R { x // x 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.

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 { x // x 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.

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.

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.

Instances For
theorem Module.free_of_finite_type_torsion_free' {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)
• bM : Basis ι R M

The basis of M.

• bN : Basis (Fin n) R { x // x 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), ↑(s.bN i) = s.bM (s.f i)

The SNF relation between the vectors of the bases.

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.

Instances For
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 : { x // x N }) {i : ι} (hi : ¬i Set.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 : ¬i Set.range snf.f) :
@[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 : { x // x N }) {i : Fin n} :
↑(snf.bM.repr m) (snf.f i) = ↑(snf.bN.repr ( 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 : { x // x 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} :
LinearMap.comp (Basis.coord snf.bM (snf.f i)) () = Basis.coord snf.bN 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 (∀ (x : M), x Nf x N) fun x x_1 => hf x) {i : Fin n} :
↑(LinearMap.toMatrix snf.bN snf.bN) () 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 bO bN a, ∀ (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 () (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.

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.

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.

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' a ab', ∀ (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.

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 { x // x 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.

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.

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 ↑()) {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.