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

theorem dvd_generator_iff {R : Type u_1} [CommSemiring 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] {M : Type u_3} [AddCommGroup M] [Module R M] [IsPrincipalIdealRing R] {N O : Submodule R M} (hNO : N ≤ O) {ϕ : ↥O →ₗ[R] R} (hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N) [(ϕ.submoduleImage N).IsPrincipal] (y : M) (yN : y ∈ N) (ϕy_eq : ϕ ⟨y, ⋯⟩ = Submodule.IsPrincipal.generator (ϕ.submoduleImage N)) (ψ : ↥O →ₗ[R] R) : Submodule.IsPrincipal.generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩

theorem Submodule.basis_of_pid_aux {ι : Type u_1} {R : Type u_2} [CommRing R] [IsPrincipalIdealRing R] [IsDomain R] [Finite ι] {O : Type u_4} [AddCommGroup O] [Module R O] (M N : Submodule R O) (b'M : Module.Basis ι R ↥M) (N_bot : N ≠ ⊥) (N_le_M : N ≤ M) : ∃ y ∈ M, ∃ (a : R), a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Module.Basis (Fin n') R ↥N'), ∃ (bN : Module.Basis (Fin (n' + 1)) R ↥N), ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Module.Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1) (bM : Module.Basis (Fin (m' + 1)) R ↥M), ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ (as' : Fin (n' + 1) → R), ∀ (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] {M : Type u_3} [AddCommGroup M] [Module R M] [IsPrincipalIdealRing R] [IsDomain R] {ι : Type u_4} [Finite ι] (b : Module.Basis ι R M) (N : Submodule R M) : ∃ (n : ℕ), Nonempty (Module.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.basisOfPid.

See also the stronger version Submodule.smithNormalForm.

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

Equations

• Submodule.basisOfPid b N = ⟨⋯.choose, ⋯.some⟩

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

noncomputable def Submodule.basisOfPidOfLE {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsPrincipalIdealRing R] [IsDomain R] {ι : Type u_4} [Finite ι] {N O : Submodule R M} (hNO : N ≤ O) (b : Module.Basis ι R ↥O) : (n : ℕ) × Module.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.smithNormalFormOfLE.

Equations

• Submodule.basisOfPidOfLE hNO b = match Submodule.basisOfPid b (Submodule.comap O.subtype N) with | ⟨n, bN'⟩ => ⟨n, bN'.map (Submodule.comapSubtypeEquivOfLe hNO)⟩

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

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

noncomputable def Module.basisOfFiniteTypeTorsionFree' {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsPrincipalIdealRing R] [IsDomain R] [Module.Finite R M] [IsTorsionFree 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 ⋯

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

instance instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree {R : Type u_2} [CommRing R] [IsPrincipalIdealRing R] [IsDomain R] {S : Type u_4} [CommRing S] [Algebra R S] {I : Ideal S} [hI₁ : Module.Finite R ↥I] [hI₂ : Module.IsTorsionFree R ↥I] : Module.Free R ↥I

theorem Module.free_iff_isTorsionFree {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsPrincipalIdealRing R] [IsDomain R] [Module.Finite R M] : Free R M ↔ IsTorsionFree R M

structure Module.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)

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.

• bM : Basis ι R M

  The basis of M.

• bN : Basis (Fin n) R ↥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) : ↑(self.bN i) = self.a i • self.bM (self.f i)

  The SNF relation between the vectors of the bases.

theorem Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_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 : SmithNormalForm N ι n) (m : ↥N) {i : ι} (hi : i ∉ Set.range ⇑snf.f) : (snf.bM.repr ↑m) i = 0

theorem Module.Basis.SmithNormalForm.le_ker_coord_of_notMem_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 : SmithNormalForm N ι n) {i : ι} (hi : i ∉ Set.range ⇑snf.f) : N ≤ (snf.bM.coord i).ker

@[simp]

theorem Module.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 : SmithNormalForm N ι n) (m : ↥N) {i : Fin n} : (snf.bM.repr ↑m) (snf.f i) = (snf.bN.repr (snf.a i • m)) i

@[simp]

theorem Module.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 : SmithNormalForm N ι n) (m : ↥N) : ⇑(snf.bM.repr ↑m) ∘ ⇑snf.f = snf.a • ⇑(snf.bN.repr m)

@[simp]

theorem Module.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 : SmithNormalForm N ι n) {i : Fin n} : snf.bM.coord (snf.f i) ∘ₗ N.subtype = snf.a i • snf.bN.coord i

@[simp]

theorem Module.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 : SmithNormalForm N ι n) [Fintype ι] [DecidableEq ι] (f : M →ₗ[R] M) (hf : ∀ (x : M), f x ∈ N) (hf' : ∀ x ∈ N, f x ∈ N := ⋯) {i : Fin n} : (LinearMap.toMatrix snf.bN snf.bN) (f.restrict 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] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] [Finite ι] (b : Module.Basis ι R M) (N O : Submodule R M) (N_le_O : N ≤ O) : ∃ (n : ℕ) (o : ℕ) (hno : n ≤ o) (bO : Module.Basis (Fin o) R ↥O) (bN : Module.Basis (Fin n) R ↥N) (a : Fin n → R), ∀ (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] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] [Finite ι] (b : Module.Basis ι R M) (N O : Submodule R M) (N_le_O : N ≤ O) : (o : ℕ) × (n : ℕ) × Module.Basis.SmithNormalForm (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.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] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] [Finite ι] (b : Module.Basis ι R M) (N : Submodule R M) : (n : ℕ) × Module.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 Submodule.smithNormalFormOfRankEq {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] {N : Submodule R M} [Fintype ι] (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) : Module.Basis.SmithNormalForm N ι (Fintype.card ι)

If M is finite free over a PID R, then for any submodule N of the same rank, we can find basis for M and N with the same indexing such that the inclusion map is a square diagonal matrix.

See Submodule.exists_smith_normal_form_of_rank_eq for a version that states the existence of the basis.

Equations

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

theorem Submodule.exists_smith_normal_form_of_rank_eq {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] {N : Submodule R M} [Finite ι] (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) : ∃ (b' : Module.Basis ι R M) (a : ι → R) (ab' : Module.Basis ι R ↥N), ∀ (i : ι), ↑(ab' i) = a i • b' i

If M is finite free over a PID R, then for any submodule N of the same rank, we can find basis for M and N with the same indexing such that the inclusion map is a square diagonal matrix.

See also Submodule.smithNormalFormOfRankEq for a version of this theorem that returns a Basis.SmithNormalForm.

noncomputable def Submodule.smithNormalFormTopBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] {N : Submodule R M} [Finite ι] (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) : Module.Basis ι R M

If M is finite free over a PID R, then for any submodule N of the same rank, we can find basis for M and N with the same indexing such that the inclusion map is a square diagonal matrix; this is the basis for M. See:

• Submodule.smithNormalFormBotBasis for the basis on N,
• Submodule.smithNormalFormCoeffs for the entries of the diagonal matrix
• Submodule.smithNormalFormBotBasis_def for the proof that the inclusion map forms a square diagonal matrix.

Equations

• Submodule.smithNormalFormTopBasis b h = ⋯.choose

noncomputable def Submodule.smithNormalFormBotBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] {N : Submodule R M} [Finite ι] (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) : Module.Basis ι R ↥N

If M is finite free over a PID R, then for any submodule N of the same rank, we can find basis for M and N with the same indexing such that the inclusion map is a square diagonal matrix; this is the basis for N. See:

• Submodule.smithNormalFormTopBasis for the basis on M,
• Submodule.smithNormalFormCoeffs for the entries of the diagonal matrix
• Submodule.smithNormalFormBotBasis_def for the proof that the inclusion map forms a square diagonal matrix.

Equations

• Submodule.smithNormalFormBotBasis b h = ⋯.choose

noncomputable def Submodule.smithNormalFormCoeffs {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] {N : Submodule R M} [Finite ι] (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) : ι → R

If M is finite free over a PID R, then for any submodule N of the same rank, we can find basis for M and N with the same indexing such that the inclusion map is a square diagonal matrix; these are the entries of the diagonal matrix. See:

• Submodule.smithNormalFormTopBasis for the basis on M,
• Submodule.smithNormalFormBotBasis for the basis on N,
• Submodule.smithNormalFormBotBasis_def for the proof that the inclusion map forms a square diagonal matrix.

Equations

• Submodule.smithNormalFormCoeffs b h = ⋯.choose

@[simp]

theorem Submodule.smithNormalFormBotBasis_def {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] {N : Submodule R M} [Finite ι] (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) (i : ι) : ↑((smithNormalFormBotBasis b h) i) = smithNormalFormCoeffs b h i • (smithNormalFormTopBasis b h) i

@[simp]

theorem Submodule.smithNormalFormCoeffs_ne_zero {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] [IsDomain R] [IsPrincipalIdealRing R] {N : Submodule R M} [Finite ι] (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) (i : ι) : smithNormalFormCoeffs b h i ≠ 0

theorem Ideal.finrank_eq_finrank {ι : 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 : Module.Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) : Module.finrank R ↥(Submodule.restrictScalars R I) = Module.finrank R S

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 : Module.Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) : Module.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

• Ideal.smithNormalForm b I hI = Submodule.smithNormalFormOfRankEq b ⋯

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 : Module.Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) : ∃ (b' : Module.Basis ι R S) (a : ι → R) (ab' : Module.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.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 : Module.Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) : Module.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,
• Ideal.smithCoeffs for the entries of the diagonal matrix
• Ideal.selfBasis_def for the proof that the inclusion map forms a square diagonal matrix.

Equations

• Ideal.ringBasis b I hI = ⋯.choose

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 : Module.Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) : Module.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.ringBasis for the basis on S,
• Ideal.smithCoeffs for the entries of the diagonal matrix
• Ideal.selfBasis_def for the proof that the inclusion map forms a square diagonal matrix.

Equations

• Ideal.selfBasis b I hI = ⋯.choose

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 : Module.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,
• Ideal.selfBasis for the basis on I,
• Ideal.selfBasis_def for the proof that the inclusion map forms a square diagonal matrix.

Equations

• Ideal.smithCoeffs b I hI = ⋯.choose

@[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 : Module.Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) (i : ι) : ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (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 : Module.Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) (i : ι) : smithCoeffs b I hI i ≠ 0