English
A proof-1 level equivalence for Smith normal form with rank constraints and embeddings.
Русский
Уровень доказательства 1 для SmithNormalForm с учётом ограничения по рангу и вложениям.
LaTeX
$$$smithNormalFormOfRankEq$-proof-1$$
Lean4
/-- If `M` is finite free over a PID `R`, then any submodule `N` is free
and we can find a basis for `M` and `N` such that the inclusion map is a diagonal matrix
in Smith normal form.
This is a strengthening of `Submodule.basisOfPid`.
See also `Ideal.smithNormalForm`, which moreover proves that the dimension of
an ideal is the same as the dimension of the whole ring.
-/
noncomputable def smithNormalForm [Finite ι] (b : Basis ι R M) (N : Submodule R M) :
Σ n : ℕ, Basis.SmithNormalForm N ι n :=
let ⟨m, n, bM, bN, f, a, snf⟩ := N.smithNormalFormOfLE b ⊤ le_top
let bM' := bM.map (LinearEquiv.ofTop _ rfl)
let e := bM'.indexEquiv b
⟨n, bM'.reindex e, bN.map (comapSubtypeEquivOfLe le_top), f.trans e.toEmbedding, a, fun i ↦ by
simp only [bM', snf, Basis.map_apply, LinearEquiv.ofTop_apply, Submodule.coe_smul_of_tower,
Submodule.comapSubtypeEquivOfLe_apply_coe, Basis.reindex_apply, Equiv.toEmbedding_apply,
Function.Embedding.trans_apply, Equiv.symm_apply_apply]⟩
