English
There exists a Smith normal form for the S-submodule I (viewed via restriction of scalars to R) inside S, giving bases b' for S, a for R-coefficients, and ab' for I such that (ab' i) = a_i b'_i for all i.
Русский
Существуют базы для 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 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.
-/
theorem exists_smith_normal_form (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) :
∃ (b' : Basis ι R S) (a : ι → R) (ab' : Basis ι R I), ∀ i, (ab' i : S) = a i • b' i :=
Submodule.exists_smith_normal_form_of_rank_eq b (finrank_eq_finrank b I hI)
