English
In a finite-rank setting for M, N with a rank-equal condition and bases b, there exist ι-indexed coefficients smithNormalFormCoeffs b h that describe the diagonal entries of the inclusion map in the Smith normal form.
Русский
При равной ранге и базах b существует набор коэффициентов smithNormalFormCoeffs b h, индексируемых ι, которые описывают диагональные элементы включения в форме Смитa.
LaTeX
$$$\\text{smithNormalFormCoeffs } b h : ι → R$$$
Lean4
/-- If `M` is finite free over a PID `R`, then for any submodule `N` of the same rank,
we can find basis for `M` and `N` with the same indexing such that the inclusion map
is a square diagonal matrix; these are the entries of the diagonal matrix. See:
* `Submodule.smithNormalFormTopBasis` for the basis on `M`,
* `Submodule.smithNormalFormBotBasis` for the basis on `N`,
* `Submodule.smithNormalFormBotBasis_def` for the proof that the inclusion map
forms a square diagonal matrix.
-/
noncomputable def smithNormalFormCoeffs (b : Basis ι R M) (h : Module.finrank R N = Module.finrank R M) : ι → R :=
(exists_smith_normal_form_of_rank_eq b h).choose_spec.choose
