English
For a finite rank submodule N ⊆ M over a PID, there is a canonical top basis for M (the Smith normal form top basis) arising from the Smith normal form decomposition, which, together with a corresponding bottom basis for N, yields a diagonal inclusion.
Русский
Для конечной ранговой пары N ⊆ M над PID существует каноническая вершина базиса M (верхняя основа Смита), которая возникает из разложения Смита, и вместе с соответствующей нижней базой для N даёт диагональное вложение.
LaTeX
$$$\exists b' : \mathrm{Basis}\ ι\ R\ M,\ \text{such that }\text{the pair }(b',\mathrm{smithNormalFormBotBasis}\, b'\, h)\text{ yields a diagonal inclusion.}$$$
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 `M`. See:
* `Submodule.smithNormalFormBotBasis` for the basis on `N`,
* `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 smithNormalFormTopBasis (b : Basis ι R M) (h : Module.finrank R N = Module.finrank R M) :
Basis ι R M :=
(exists_smith_normal_form_of_rank_eq b h).choose
