English
There is a basis for I as an R-submodule of S that corresponds to the Smith-normal-form decomposition of I inside S.
Русский
Существует база для I как подмодуля I над R внутри S, соответствующая разложениям Смита-Нормальной формы.
LaTeX
$$$\\text{selfBasis}(b, I, hI) : \\text{Basis } ι R 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; 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.
-/
noncomputable def selfBasis (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) : Basis ι R I :=
(Ideal.exists_smith_normal_form b I hI).choose_spec.choose_spec.choose
