# mathlib3documentation

linear_algebra.free_module.pid

# Free modules over PID #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 [is_domain R] [is_principal_ideal_ring 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.induction_on_rank: 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.smith_normal_form: 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] [ M] {ι : Type u_1} (b : R M) {N : M} {ϕ : M →ₗ[R] R} (hϕ : (ψ : M →ₗ[R] R), ¬ < ) [ N).is_principal] (hgen : = 0) :
N =
theorem eq_bot_of_generator_maximal_submodule_image_eq_zero {R : Type u} {M : Type v} [ring R] [ M] {ι : Type u_1} {N O : M} (b : R O) (hNO : N O) {ϕ : O →ₗ[R] R} (hϕ : (ψ : O →ₗ[R] R), ¬ < ) [(ϕ.submodule_image N).is_principal] (hgen : = 0) :
N =
theorem dvd_generator_iff {R : Type u_2} [comm_ring R] [is_domain R] {I : ideal R} {x : R} (hx : x I) :
theorem generator_maximal_submodule_image_dvd {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] {N O : M} (hNO : N O) {ϕ : O →ₗ[R] R} (hϕ : (ψ : O →ₗ[R] R), ¬ < ) [(ϕ.submodule_image N).is_principal] (y : M) (yN : y N) (ϕy_eq : ϕ y, _⟩ = ) (ψ : O →ₗ[R] R) :
ψ y, _⟩
theorem submodule.basis_of_pid_aux {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [finite ι] {O : Type u_3} [ O] (M N : O) (b'M : R M) (N_bot : N ) (N_le_M : N M) :
(y : O) (H : y M) (a : R) (hay : a y N) (M' : O) (H : M' M) (N' : O) (H : N' N) (N'_le_M' : N' M') (y_ortho_M' : (c : R) (z : O), z M' c y + z = 0 c = 0) (ay_ortho_N' : (c : R) (z : O), z N' c a y + z = 0 c = 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.cast_le hn'm') i))) ( (as' : fin (n' + 1) R), (i : fin (n' + 1)), (bN i) = as' i (bM ((fin.cast_le hnm) i)))

The induction hypothesis of submodule.basis_of_pid and submodule.smith_normal_form.

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} [comm_ring R] [is_domain R] {M : Type u_3} [ M] {ι : Type u_1} [finite ι] (b : R M) (N : M) :
(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.basis_of_pid.

See also the stronger version submodule.smith_normal_form.

noncomputable def submodule.basis_of_pid {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] {ι : Type u_1} [finite ι] (b : R M) (N : M) :
Σ (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.smith_normal_form.

Equations
theorem submodule.basis_of_pid_bot {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] {ι : Type u_1} [finite ι] (b : R M) :
noncomputable def submodule.basis_of_pid_of_le {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] {ι : Type u_1} [finite ι] {N O : M} (hNO : N O) (b : 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.smith_normal_form_of_le.

Equations
• = submodule.basis_of_pid_of_le._match_1 hNO N))
• submodule.basis_of_pid_of_le._match_1 hNO n, bN'⟩ = n, bN'.map
noncomputable def submodule.basis_of_pid_of_le_span {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] {ι : Type u_1} [finite ι] {b : ι M} (hb : b) {N : M} (le : N (set.range b)) :
Σ (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
noncomputable def module.basis_of_finite_type_torsion_free {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] [fintype ι] {s : ι M} (hs : (set.range s) = )  :
Σ (n : ), basis (fin n) R M

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

Equations
theorem module.free_of_finite_type_torsion_free {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] [finite ι] {s : ι M} (hs : (set.range s) = )  :
M
noncomputable def module.basis_of_finite_type_torsion_free' {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] [ M]  :
Σ (n : ), basis (fin n) R M

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

Equations
theorem module.free_of_finite_type_torsion_free' {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] [ M]  :
M
@[nolint]
structure basis.smith_normal_form {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] (N : M) (ι : Type u_4) (n : ) :
Type (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.

Instances for basis.smith_normal_form
• basis.smith_normal_form.has_sizeof_inst
theorem submodule.exists_smith_normal_form_of_le {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] [finite ι] (b : R M) (N O : M) (N_le_O : N O) :
(n o : ) (hno : n o) (bO : basis (fin o) R O) (bN : basis (fin n) R N) (a : fin n R), (i : fin n), (bN i) = a i (bO ((fin.cast_le 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.smith_normal_form_of_le for a version of this theorem that returns a basis.smith_normal_form.

This is a strengthening of submodule.basis_of_pid_of_le.

noncomputable def submodule.smith_normal_form_of_le {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] [finite ι] (b : R M) (N O : M) (N_le_O : N O) :
Σ (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.basis_of_pid_of_le.

Equations
noncomputable def submodule.smith_normal_form {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {M : Type u_3} [ M] [finite ι] (b : R M) (N : M) :
Σ (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.basis_of_pid.

See also ideal.smith_normal_form, which moreover proves that the dimension of an ideal is the same as the dimension of the whole ring.

Equations
• = submodule.smith_normal_form._match_1 b N
• submodule.smith_normal_form._match_1 b N m, n, {bM := bM, bN := bN, f := f, a := a, snf := snf} = let bM' : basis (fin m) R M := bM.map submodule.smith_normal_form._match_1._proof_1), e : fin m ι := bM'.index_equiv b in n, {bM := bM'.reindex e, bN := , f := , a := a, snf := _}
noncomputable def ideal.smith_normal_form {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {S : Type u_4} [comm_ring S] [is_domain S] [ S] [fintype ι] (b : R S) (I : ideal S) (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.basis_of_pid.

Equations
theorem ideal.exists_smith_normal_form {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {S : Type u_4} [comm_ring S] [is_domain S] [ S] [finite ι] (b : R S) (I : ideal S) (hI : I ) :
(b' : R S) (a : ι R) (ab' : 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.smith_normal_form for a version of this theorem that returns a basis.smith_normal_form.

The definitions ideal.ring_basis, ideal.self_basis, ideal.smith_coeffs are (noncomputable) choices of values for this existential quantifier.

noncomputable def ideal.ring_basis {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {S : Type u_4} [comm_ring S] [is_domain S] [ S] [finite ι] (b : R S) (I : ideal S) (hI : I ) :
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.self_basis for the basis on I, see ideal.smith_coeffs for the entries of the diagonal matrix and ideal.self_basis_def for the proof that the inclusion map forms a square diagonal matrix.

Equations
noncomputable def ideal.self_basis {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {S : Type u_4} [comm_ring S] [is_domain S] [ S] [finite ι] (b : R S) (I : ideal S) (hI : I ) :
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.ring_basis for the basis on S, see ideal.smith_coeffs for the entries of the diagonal matrix and ideal.self_basis_def for the proof that the inclusion map forms a square diagonal matrix.

Equations
• hI =
noncomputable def ideal.smith_coeffs {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {S : Type u_4} [comm_ring S] [is_domain S] [ S] [finite ι] (b : 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.ring_basis for the basis on S, see ideal.self_basis for the basis on I, and ideal.self_basis_def for the proof that the inclusion map forms a square diagonal matrix.

Equations
• hI =
@[simp]
theorem ideal.self_basis_def {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {S : Type u_4} [comm_ring S] [is_domain S] [ S] [finite ι] (b : R S) (I : ideal S) (hI : I ) (i : ι) :
( I hI) i) = hI i 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.smith_coeffs_ne_zero {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {S : Type u_4} [comm_ring S] [is_domain S] [ S] [finite ι] (b : R S) (I : ideal S) (hI : I ) (i : ι) :
hI i 0
@[protected, instance]
def has_quotient.quotient.module {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] {S : Type u_4} [comm_ring S] [is_domain S] [ S] [finite ι] (F : Type u) [comm_ring F] [ R] (b : R S) {I : ideal S} (hI : I ) (i : ι) :
(R ideal.span hI i})
Equations
theorem linear_independent.restrict_scalars_algebras {R : Type u_1} {S : Type u_2} {M : Type u_3} {ι : Type u_4} [semiring S] [ S] [ M] [ M] [ M] (hinj : function.injective S)) {v : ι M} (li : 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.