mathlib documentation

linear_algebra.free_module.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 [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.

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] [add_comm_group 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 ψ Nsubmodule.map ψ N = submodule.map ϕ N) [(submodule.map ϕ N).is_principal] (hgen : submodule.is_principal.generator (submodule.map ϕ N) = 0) :
N =
theorem eq_bot_of_generator_maximal_submodule_image_eq_zero {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {N O : submodule R M} (b : basis ι R O) (hNO : N O) {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ϕ.submodule_image N ψ.submodule_image Nψ.submodule_image N = ϕ.submodule_image N) [(ϕ.submodule_image N).is_principal] (hgen : submodule.is_principal.generator (ϕ.submodule_image N) = 0) :
N =
theorem dvd_generator_iff {R : Type u_2} [comm_ring R] [is_domain R] {I : ideal R} [submodule.is_principal I] {x : R} (hx : x I) :
theorem generator_maximal_submodule_image_dvd {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] {N O : submodule R M} (hNO : N O) {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ϕ.submodule_image N ψ.submodule_image Nψ.submodule_image N = ϕ.submodule_image N) [(ϕ.submodule_image N).is_principal] (y : M) (yN : y N) (ϕy_eq : ϕ y, _⟩ = submodule.is_principal.generator (ϕ.submodule_image N)) (ψ : O →ₗ[R] R) :
theorem submodule.basis_of_pid_aux {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] [fintype ι] {O : Type u_3} [add_comm_group O] [module R O] (M N : submodule R O) (b'M : basis ι R M) (N_bot : N ) (N_le_M : N M) :
∃ (y : O) (H : y M) (a : R) (hay : a y N) (M' : submodule R O) (H : M' M) (N' : submodule R O) (H : N' N) (N'_le_M' : N' M') (y_ortho_M' : ∀ (c : R) (z : O), z M'c y + z = 0c = 0) (ay_ortho_N' : ∀ (c : R) (z : O), z N'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.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] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] (b : basis ι R M) (N : submodule R 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] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] (b : basis ι R M) (N : submodule R 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] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] (b : basis ι R M) :
noncomputable def submodule.basis_of_pid_of_le {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] {N O : submodule R M} (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.smith_normal_form_of_le.

Equations
noncomputable def submodule.basis_of_pid_of_le_span {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] {ι : Type u_1} [fintype ι] {b : ι → M} (hb : linear_independent R b) {N : submodule R M} (le : N submodule.span R (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.free_of_finite_type_torsion_free {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] [fintype ι] {s : ι → M} (hs : submodule.span R (set.range s) = ) [no_zero_smul_divisors R M] :
Σ (n : ), basis (fin n) R M

A finite type torsion free module over a PID is free.

Equations
noncomputable def module.free_of_finite_type_torsion_free' {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] [module.finite R M] [no_zero_smul_divisors R M] :
Σ (n : ), basis (fin n) R M

A finite type torsion free module over a PID is free.

Equations
@[nolint]
structure basis.smith_normal_form {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] (N : submodule R 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.

theorem submodule.exists_smith_normal_form_of_le {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] [fintype ι] (b : basis ι R M) (N O : submodule R 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] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] [fintype ι] (b : basis ι R M) (N O : submodule R M) (N_le_O : N O) :

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] [is_principal_ideal_ring R] {M : Type u_3} [add_comm_group M] [module R M] [fintype ι] (b : basis ι R M) (N : submodule R M) :
Σ (n : ), basis.smith_normal_form 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.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
noncomputable def ideal.smith_normal_form {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] [fintype ι] {S : Type u_3} [comm_ring S] [is_domain S] [algebra R S] (b : basis ι 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] [is_principal_ideal_ring R] [fintype ι] {S : Type u_3} [comm_ring S] [is_domain S] [algebra R S] (b : basis ι R S) (I : ideal S) (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.smith_normal_form for a version of this theorem that returns a basis.smith_normal_form.

theorem linear_independent.restrict_scalars_algebras {R : Type u_1} {S : Type u_2} {M : Type u_3} {ι : Type u_4} [comm_semiring R] [semiring S] [add_comm_monoid M] [algebra R S] [module R M] [module S M] [is_scalar_tower R S M] (hinj : function.injective (algebra_map R S)) {v : ι → M} (li : linear_independent S 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.