English
For a finite-dimensional extension S over a principal ideal domain R, free as an R-module, and a nonzero ideal I of S, there exists a basis of S and a basis of I such that the inclusion I → S is represented by a diagonal matrix.
Русский
Для конечномерного расширения S над PID-R, свободного как R-модуль, и ненулевого идеала I ⊆ S существует база для S и база для I, при которых включение I ↪ S выражается диагональной матрицей.
LaTeX
$$$\\exists b' : \\text{Basis } ι R S,\\; \\exists a : ι \\to R,\\; \\exists ab' : \\text{Basis } ι R I,\\; \\forall i,\\; (ab' i : S) = a i \\cdot b' i$$$
Lean4
/-- 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`.
-/
noncomputable def smithNormalForm [Fintype ι] (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) :
Basis.SmithNormalForm (I.restrictScalars R) ι (Fintype.card ι) :=
Submodule.smithNormalFormOfRankEq b (finrank_eq_finrank b I hI)
