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] [AddCommGroup M] [Module R M] {ι : Type u_1} (b : Basis ι R M) {N : Submodule R M} {ϕ : M →ₗ[R] R} (hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N) [Submodule.IsPrincipal (Submodule.map ϕ N)] (hgen : Submodule.IsPrincipal.generator (Submodule.map ϕ N) = 0) : N = ⊥

theorem eq_bot_of_generator_maximal_submoduleImage_eq_zero {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_1} {N : Submodule R M} {O : Submodule R M} (b : Basis ι R { x // x ∈ O }) (hNO : N ≤ O) {ϕ : { x // x ∈ O } →ₗ[R] R} (hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N) [Submodule.IsPrincipal (LinearMap.submoduleImage ϕ N)] (hgen : Submodule.IsPrincipal.generator (LinearMap.submoduleImage ϕ N) = 0) : N = ⊥

theorem dvd_generator_iff {R : Type u_2} [CommRing R] [IsDomain R] {I : Ideal R} [Submodule.IsPrincipal I] {x : R} (hx : x ∈ I) : x ∣ Submodule.IsPrincipal.generator I ↔ I = Ideal.span {x}

theorem generator_maximal_submoduleImage_dvd {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {N : Submodule R M} {O : Submodule R M} (hNO : N ≤ O) {ϕ : { x // x ∈ O } →ₗ[R] R} (hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N) [Submodule.IsPrincipal (LinearMap.submoduleImage ϕ N)] (y : M) (yN : y ∈ N) (ϕy_eq : ↑ϕ { val := y, property := hNO y yN } = Submodule.IsPrincipal.generator (LinearMap.submoduleImage ϕ N)) (ψ : { x // x ∈ O } →ₗ[R] R) : Submodule.IsPrincipal.generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := hNO y yN }

theorem Submodule.basis_of_pid_aux {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [Finite ι] {O : Type u_4} [AddCommGroup O] [Module R O] (M : Submodule R O) (N : Submodule R O) (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} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] (b : Basis ι R M) (N : Submodule R M) : ∃ 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} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] (b : Basis ι R M) (N : Submodule R M) : (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.

Equations

• One or more equations did not get rendered due to their size.

theorem Submodule.basisOfPid_bot {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] (b : Basis ι R M) : Submodule.basisOfPid b ⊥ = { fst := 0, snd := Basis.empty { x // x ∈ ⊥ } }

noncomputable def Submodule.basisOfPidOfLE {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] {N : Submodule R M} {O : Submodule R M} (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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Submodule.basisOfPidOfLESpan {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {ι : Type u_4} [Finite ι] {b : ι → M} (hb : LinearIndependent R b) {N : Submodule R M} (le : N ≤ Submodule.span R (Set.range b)) : (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.

Equations

• Submodule.basisOfPidOfLESpan hb le = Submodule.basisOfPidOfLE le (Basis.span hb)

noncomputable def Module.basisOfFiniteTypeTorsionFree {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Fintype ι] {s : ι → M} (hs : Submodule.span R (Set.range s) = ⊤) [NoZeroSMulDivisors R M] : (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.

theorem Module.free_of_finite_type_torsion_free {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Finite ι] {s : ι → M} (hs : Submodule.span R (Set.range s) = ⊤) [NoZeroSMulDivisors R M] : Module.Free R M

noncomputable def Module.basisOfFiniteTypeTorsionFree' {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Module.Finite R M] [NoZeroSMulDivisors R M] : (n : ℕ) × Basis (Fin n) R M

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

Equations

• Module.basisOfFiniteTypeTorsionFree' = Module.basisOfFiniteTypeTorsionFree (_ : Submodule.span R (Set.range (Exists.choose (_ : ∃ s, Submodule.span R (Set.range s) = ⊤))) = ⊤)

theorem Module.free_of_finite_type_torsion_free' {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Module.Finite R M] [NoZeroSMulDivisors R M] : Module.Free R M

structure Basis.SmithNormalForm {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (N : Submodule R M) (ι : 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 n → R

  The (diagonal) entries of the matrix.

• snf : ∀ (i : Fin n), ↑(↑s.bN i) = Basis.SmithNormalForm.a s 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.

theorem Basis.SmithNormalForm.repr_eq_zero_of_nmem_range {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) (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} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) {i : ι} (hi : ¬i ∈ Set.range ↑snf.f) : N ≤ LinearMap.ker (Basis.coord snf.bM i)

@[simp]

theorem Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) (m : { x // x ∈ N }) {i : Fin n} : ↑(↑snf.bM.repr ↑m) (↑snf.f i) = ↑(↑snf.bN.repr (Basis.SmithNormalForm.a snf i • m)) i

@[simp]

theorem Basis.SmithNormalForm.repr_comp_embedding_eq_smul {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) (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} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) {i : Fin n} : LinearMap.comp (Basis.coord snf.bM (↑snf.f i)) (Submodule.subtype N) = Basis.SmithNormalForm.a snf i • Basis.coord snf.bN i

@[simp]

theorem Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {n : ℕ} {N : Submodule R M} (snf : Basis.SmithNormalForm N ι n) [Fintype ι] [DecidableEq ι] (f : M →ₗ[R] M) (hf : ∀ (x : M), ↑f x ∈ N) (hf' : optParam (∀ (x : M), x ∈ N → ↑f x ∈ N) fun x x_1 => hf x) {i : Fin n} : ↑(LinearMap.toMatrix snf.bN snf.bN) (LinearMap.restrict f 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} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Finite ι] (b : Basis ι R M) (N : Submodule R M) (O : Submodule R M) (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} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [Finite ι] (b : Basis ι R M) (N : Submodule R M) (O : Submodule R M) (N_le_O : N ≤ O) : (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (Submodule.comap (Submodule.subtype O) 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.

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

noncomputable def Ideal.smithNormalForm {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Fintype ι] (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) : Basis.SmithNormalForm (Submodule.restrictScalars R I) ι (Fintype.card ι)

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.

theorem Ideal.exists_smith_normal_form {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (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} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (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

• Ideal.ringBasis b I hI = Exists.choose (_ : ∃ b' a ab', ∀ (i : ι), ↑(↑ab' i) = a i • ↑b' i)

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

Equations

• One or more equations did not get rendered due to their size.

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

• Ideal.smithCoeffs b I hI = Exists.choose (_ : ∃ a ab', ∀ (i : ι), ↑(↑ab' i) = a i • ↑(Exists.choose (_ : ∃ b' a ab', ∀ (i : ι), ↑(↑ab' i) = a i • ↑b' i)) i)

@[simp]

theorem Ideal.selfBasis_def {ι : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (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} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4} [CommRing S] [IsDomain S] [Algebra R S] [Finite ι] (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) (i : ι) : Ideal.smithCoeffs b I hI i ≠ 0

theorem LinearIndependent.restrict_scalars_algebras {R : Type u_1} {S : Type u_2} {M : Type u_3} {ι : Type u_4} [CommSemiring R] [Semiring S] [AddCommMonoid M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (hinj : Function.Injective ↑(algebraMap R S)) {v : ι → M} (li : LinearIndependent S v) : LinearIndependent R v

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