English
If M is finite-free over a PID R, then for any submodule N of the same rank, there exists bases for M and N with the same index set such that the inclusion map is represented by a square diagonal matrix.
Русский
Если M конечномерно свободен над PID R, то для любой подмодуля N той же ранга существуют базы M и N с общим индексом, для которых включение представлено квадратной диагональной матрицей.
LaTeX
$$$\\text{smithNormalFormBotBasis}(b,h):\\;\\text{Basis } ι R N$ с равной ранговой записью и соответствующим свойством включения.$$
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; this is the basis for `N`. See:
* `Submodule.smithNormalFormTopBasis` for the basis on `M`,
* `Submodule.smithNormalFormCoeffs` for the entries of the diagonal matrix
* `Submodule.smithNormalFormBotBasis_def` for the proof that the inclusion map
forms a square diagonal matrix.
-/
noncomputable def smithNormalFormBotBasis (b : Basis ι R M) (h : Module.finrank R N = Module.finrank R M) :
Basis ι R N :=
(exists_smith_normal_form_of_rank_eq b h).choose_spec.choose_spec.choose
