English
Further explicit formulation of a Smith normal form by matching B-bases under embeddings with respect to rank constraints.
Русский
Дополнительная явная формулировка SmithNormalForm при сопоставлении баз B через вложения с учётом рангов.
LaTeX
$$$smithNormalFormOfRankEq$-proof-6$$
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.
See `Submodule.exists_smith_normal_form_of_le` for a version of this theorem that doesn't
need to map `N` into a submodule of `O`.
This is a strengthening of `Submodule.basisOfPidOfLe`.
-/
noncomputable def smithNormalFormOfLE [Finite ι] (b : Basis ι R M) (N O : Submodule R M) (N_le_O : N ≤ O) :
Σ o n : ℕ, Basis.SmithNormalForm (N.comap O.subtype) (Fin o) n :=
by
choose n o hno bO bN a snf using N.exists_smith_normal_form_of_le b O N_le_O
refine ⟨o, n, bO, bN.map (comapSubtypeEquivOfLe N_le_O).symm, (Fin.castLEEmb hno), a, fun i ↦ ?_⟩
ext
simp only [snf, Basis.map_apply, Submodule.comapSubtypeEquivOfLe_symm_apply, Submodule.coe_smul_of_tower,
Fin.castLEEmb_apply]
