Skip to content

Smith normal form

2 fully proved

Submodule

TheoremSmith normal form with a divisibility chain#✓fully proved

Let \(R\) be a principal ideal domain, let \(M\) be a finitely generated free \(R\)-module and let \(N\) be a submodule of \(M\). Then there are natural numbers \(n \le m\), a basis \(e_0, \dots, e_{m-1}\) of \(M\), a basis \(f_0, \dots, f_{n-1}\) of \(N\) and nonzero elements \(a_0, \dots, a_{n-1}\) of \(R\) such that \(f_i = a_i e_i\) in \(M\) for every \(i < n\) and \(a_i \mid a_{i+1}\) whenever \(i + 1 < n\).

theorem exists_smith_normal_form_dvd_chain
    {R M : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
    [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M]
    (N : Submodule R M) :
    ∃ (n m : ℕ) (hnm : n ≤ m) (bM : Module.Basis (Fin m) R M)
      (bN : Module.Basis (Fin n) R N) (a : Fin n → R),
      (∀ i, (bN i : M) = a i • bM (Fin.castLE hnm i)) ∧
      (∀ i, a i ≠ 0) ∧
      (∀ (i : ℕ) (hi1 : i < n) (hi2 : i + 1 < n), a ⟨i, hi1⟩ ∣ a ⟨i + 1, hi2⟩)
Used by 2
Used byFundamental theorem of finitely generated abelian groups, invariant factor form · Smith normal form

Smith normal form

TheoremSmith normal form#✓fully proved

Let \(R\) be a principal ideal domain, let \(M\) be a finitely generated free \(R\)-module and let \(N\) be a submodule of \(M\). Then there are natural numbers \(n \le m\), a basis \(e_0, \dots, e_{m-1}\) of \(M\), a basis \(f_0, \dots, f_{n-1}\) of \(N\) and nonzero elements \(a_0, \dots, a_{n-1}\) of \(R\) such that \(f_i = a_i e_i\) in \(M\) for every \(i < n\) and \(a_i \mid a_{i+1}\) whenever \(i + 1 < n\).

theorem smithNormalForm
    {R M : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
    [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M]
    (N : Submodule R M) :
    ∃ (n m : ℕ) (hnm : n ≤ m) (bM : Module.Basis (Fin m) R M)
      (bN : Module.Basis (Fin n) R N) (a : Fin n → R),
      (∀ i, (bN i : M) = a i • bM (Fin.castLE hnm i)) ∧
      (∀ i, a i ≠ 0) ∧
      (∀ (i : ℕ) (hi1 : i < n) (hi2 : i + 1 < n), a ⟨i, hi1⟩ ∣ a ⟨i + 1, hi2⟩)
Sources
  • H. J. S. Smith, Phil. Trans. R. Soc. Lond. 151 (1861), 293-326, DOI 10.1098/RSTL.1861.0016. It is Submodule.exists_smith_normal_form_dvd_chain, kept under the source's name.
Uses 1
Proof usesSmith normal form with a divisibility chain

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.