English
There is a canonical Smith basis for the ambient ring S relative to a nonzero ideal I, arising from the Smith normal form data: ringBasis is a basis of S, and selfBasis is a basis for I compatibly with the diagonal inclusion.
Русский
Существует канонический базис Смита для окружения S по отношению к ненулевому идеалу I, получаемый из данных нормальной формы Смита: ringBasis — база S, selfBasis — база I совместимая с диагональным включением.
LaTeX
$$$\\text{ringBasis}(b, I, hI) : \\text{Basis } ι R S$$$
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; 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.
-/
noncomputable def ringBasis (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) : Basis ι R S :=
(Ideal.exists_smith_normal_form b I hI).choose
