linear_algebra.free_module.pid

source

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 ψ N) [(submodule.map ϕ N).is_principal] (hgen : submodule.is_principal.generator (submodule.map ϕ N) = 0) :

N = ⊥

source

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).is_principal] (hgen : submodule.is_principal.generator (ϕ.submodule_image N) = 0) :

N = ⊥

source

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) :

x ∣ submodule.is_principal.generator I ↔ I = ideal.span {x}

source

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).is_principal] (y : M) (yN : y ∈ N) (ϕy_eq : ⇑ϕ ⟨y, _⟩ = submodule.is_principal.generator (ϕ.submodule_image N)) (ψ : ↥O →ₗ[R] R) :

submodule.is_principal.generator (ϕ.submodule_image N) ∣ ⇑ψ ⟨y, _⟩

source

theorem submodule.basis_of_pid_aux {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] [finite ι] {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 = 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.

source

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} [finite ι] (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.

source

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} [finite ι] (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

submodule.basis_of_pid b N = ⟨_.some, nonempty.some _⟩

source

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} [finite ι] (b : basis ι R M) :

submodule.basis_of_pid b ⊥ = ⟨0, basis.empty ↥⊥ fin.is_empty⟩

source

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} [finite ι] {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

submodule.basis_of_pid_of_le hNO b = submodule.basis_of_pid_of_le._match_1 hNO (submodule.basis_of_pid b (submodule.comap O.subtype N))
submodule.basis_of_pid_of_le._match_1 hNO ⟨n, bN'⟩ = ⟨n, bN'.map (submodule.comap_subtype_equiv_of_le hNO)⟩

source

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} [finite ι] {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

submodule.basis_of_pid_of_le_span hb le = submodule.basis_of_pid_of_le le (basis.span hb)

source

noncomputable def module.basis_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 admits a basis.

Equations

module.basis_of_finite_type_torsion_free hs = let I : set ι := module.basis_of_finite_type_torsion_free._proof_1.some in and.dcases_on module.basis_of_finite_type_torsion_free._proof_3 (λ (indepI : linear_independent R (λ (x : ↥(module.basis_of_finite_type_torsion_free._proof_2.some)), s ↑x)) (hI : ∀ (i : ι), i ∉ module.basis_of_finite_type_torsion_free._proof_2.some → (∃ (a : R), a ≠ 0 ∧ a • s i ∈ submodule.span R (s '' module.basis_of_finite_type_torsion_free._proof_2.some))), id (λ (indepI : linear_independent R (s ∘ coe)), id (λ (hI : ∀ (i : ι), i ∉ I → (∃ (a : R), a ≠ 0 ∧ a • s i ∈ submodule.span R (s '' I))), let N : submodule R M := submodule.span R (set.range (s ∘ coe)), sI : ↥I → ↥N := λ (i : ↥I), ⟨s i.val, _⟩, sI_basis : basis ↥I R ↥N := basis.span indepI in (λ (_x : ∀ (i : ι), (λ (i : ι), classical.some _) i ≠ 0 ∧ (λ (i : ι), classical.some _) i • s i ∈ N), let A : R := finset.univ.prod (λ (i : ι), (λ (i : ι), classical.some _) i), φ : M →ₗ[R] M := ⇑(linear_map.lsmul R M) A, ψ : M ≃ₗ[R] ↥(linear_map.range φ) := linear_equiv.of_injective φ _ in (submodule.basis_of_pid_of_le _ sI_basis).cases_on (λ (n : ℕ) (b : basis (fin n) R ↥(linear_map.range φ)), ⟨n, b.map ψ.symm⟩)) _) hI) indepI)

source

theorem 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] [finite ι] {s : ι → M} (hs : submodule.span R (set.range s) = ⊤) [no_zero_smul_divisors R M] :

module.free R M

source

noncomputable def module.basis_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 admits a basis.

Equations

module.basis_of_finite_type_torsion_free' = module.basis_of_finite_type_torsion_free module.basis_of_finite_type_torsion_free'._proof_3

source

theorem 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] :

module.free R M

source

@[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)

bM : basis ι R M
bN : basis (fin n) R ↥N
f : fin n ↪ ι
a : fin n → R
snf : ∀ (i : fin n), ↑(⇑(self.bN) i) = self.a i • ⇑(self.bM) (⇑(self.f) i)

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

source

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] [finite ι] (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.

source

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] [finite ι] (b : basis ι R M) (N O : submodule R M) (N_le_O : N ≤ O) :

Σ (o n : ℕ), basis.smith_normal_form (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.basis_of_pid_of_le.

Equations

submodule.smith_normal_form_of_le b N O N_le_O = (λ (_x : ∃ (o : ℕ) (hno : classical.some _ ≤ o) (bO : basis (fin o) R ↥O) (bN : basis (fin (classical.some _)) R ↥N) (a : fin (classical.some _) → R), ∀ (i : fin (classical.some _)), ↑(⇑bN i) = a i • ↑(⇑bO (⇑(fin.cast_le hno) i))), (λ (_x_1 : ∃ (hno : classical.some _ ≤ classical.some _x) (bO : basis (fin (classical.some _x)) R ↥O) (bN : basis (fin (classical.some _)) R ↥N) (a : fin (classical.some _) → R), ∀ (i : fin (classical.some _)), ↑(⇑bN i) = a i • ↑(⇑bO (⇑(fin.cast_le hno) i))), (λ (_x_2 : ∃ (bO : basis (fin (classical.some _x)) R ↥O) (bN : basis (fin (classical.some _)) R ↥N) (a : fin (classical.some _) → R), ∀ (i : fin (classical.some _)), ↑(⇑bN i) = a i • ↑(⇑bO (⇑(fin.cast_le _) i))), (λ (_x_1_1 : ∃ (bN : basis (fin (classical.some _)) R ↥N) (a : fin (classical.some _) → R), ∀ (i : fin (classical.some _)), ↑(⇑bN i) = a i • ↑(⇑(classical.some _x_2) (⇑(fin.cast_le _) i))), (λ (_x_3 : ∃ (a : fin (classical.some _) → R), ∀ (i : fin (classical.some _)), ↑(⇑(classical.some _x_1_1) i) = a i • ↑(⇑(classical.some _x_2) (⇑(fin.cast_le _) i))), (λ (_x_1_2 : ∀ (i : fin (classical.some _)), ↑(⇑(classical.some _x_1_1) i) = classical.some _x_3 i • ↑(⇑(classical.some _x_2) (⇑(fin.cast_le _) i))), ⟨classical.some _x, ⟨classical.some _, {bM := classical.some _x_2, bN := (classical.some _x_1_1).map (submodule.comap_subtype_equiv_of_le N_le_O).symm, f := (fin.cast_le _).to_embedding, a := classical.some _x_3, snf := _}⟩⟩) _) _) _) _) _) _

source

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] [finite ι] (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

submodule.smith_normal_form b N = submodule.smith_normal_form._match_1 b N (submodule.smith_normal_form_of_le 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 (linear_equiv.of_top ⊤ submodule.smith_normal_form._match_1._proof_1), e : fin m ≃ ι := bM'.index_equiv b in ⟨n, {bM := bM'.reindex e, bN := bN.map (submodule.comap_subtype_equiv_of_le _), f := f.trans e.to_embedding, a := a, snf := _}⟩

source

noncomputable def ideal.smith_normal_form {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {S : Type u_4} [comm_ring S] [is_domain S] [algebra R S] [fintype ι] (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) :

basis.smith_normal_form (submodule.restrict_scalars 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.basis_of_pid.

Equations

ideal.smith_normal_form b I hI = ideal.smith_normal_form._match_1 I hI (submodule.smith_normal_form b (submodule.restrict_scalars R I))
ideal.smith_normal_form._match_1 I hI ⟨n, {bM := bS, bN := bI, f := f, a := a, snf := snf}⟩ = have eq : fintype.card (fin n) = fintype.card ι, from _, let e : fin n ≃ fin (fintype.card ι) := fintype.equiv_of_card_eq _ in {bM := bS, bN := bI.reindex e, f := e.symm.to_embedding.trans f, a := a ∘ ⇑(e.symm), snf := _}

source

theorem ideal.exists_smith_normal_form {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {S : Type u_4} [comm_ring S] [is_domain S] [algebra R S] [finite ι] (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.

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

source

noncomputable def ideal.ring_basis {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {S : Type u_4} [comm_ring S] [is_domain 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.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

ideal.ring_basis b I hI = _.some

source

noncomputable def ideal.self_basis {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {S : Type u_4} [comm_ring S] [is_domain S] [algebra R S] [finite ι] (b : basis ι R S) (I : ideal S) (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.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

ideal.self_basis b I hI = Exists.some _

source

noncomputable def ideal.smith_coeffs {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {S : Type u_4} [comm_ring S] [is_domain 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.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

ideal.smith_coeffs b I hI = Exists.some _

source

@[simp]

theorem ideal.self_basis_def {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {S : Type u_4} [comm_ring S] [is_domain S] [algebra R S] [finite ι] (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) (i : ι) :

↑(⇑(ideal.self_basis b I hI) i) = ideal.smith_coeffs b I hI i • ⇑(ideal.ring_basis 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.

source

@[simp]

theorem ideal.smith_coeffs_ne_zero {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {S : Type u_4} [comm_ring S] [is_domain S] [algebra R S] [finite ι] (b : basis ι R S) (I : ideal S) (hI : I ≠ ⊥) (i : ι) :

ideal.smith_coeffs b I hI i ≠ 0

source

@[protected, instance]

def has_quotient.quotient.module {ι : Type u_1} {R : Type u_2} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] {S : Type u_4} [comm_ring S] [is_domain S] [algebra R S] [finite ι] (F : Type u) [comm_ring F] [algebra F R] (b : basis ι R S) {I : ideal S} (hI : I ≠ ⊥) (i : ι) :

module F (R ⧸ ideal.span {ideal.smith_coeffs b I hI i})

Equations

has_quotient.quotient.module F b hI i = submodule.quotient.module' (ideal.span {ideal.smith_coeffs b I hI i})

source

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) :

linear_independent 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.

mathlib3 documentation

Free modules over PID #

Main results #

Tags #