English
If M is a finite free module over a PID, any submodule N is free, and there is a Smith normal form for the inclusion N ↪ M.
Русский
Если M — конечный свободный модуль над PID, то любой подмодуль N свободен, и существует SmithNormalForm для включения N ↪ M.
LaTeX
$$$\\text{Submodule}.smithNormalForm\\; (N\\subset M)$ exists and yields a diagonal form$$
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.
See `Submodule.exists_smith_normal_form_of_rank_eq` for a version that states the
existence of the basis.
-/
noncomputable def smithNormalFormOfRankEq [Fintype ι] (b : Basis ι R M) (h : Module.finrank R N = Module.finrank R M) :
Basis.SmithNormalForm N ι (Fintype.card ι) :=
let ⟨n, bM, bN, f, a, snf⟩ := N.smithNormalForm b
let e : Fin n ≃ Fin (Fintype.card ι) :=
Fintype.equivOfCardEq
(by simp only [Fintype.card_fin, ← Module.finrank_eq_card_basis bM, ← h, Module.finrank_eq_card_basis bN])
⟨bM, bN.reindex e, e.symm.toEmbedding.trans f, a ∘ e.symm, fun i ↦ by
simp only [snf, Basis.coe_reindex, Function.Embedding.trans_apply, Equiv.toEmbedding_apply, (· ∘ ·)]⟩
