English
Let R be a principal ideal domain and M a finite free R‑module. If N is a submodule of M with the same rank as M, then there exist a basis b′ of M, a function a:ι→R, and a basis ab′ of N (with the same indexing set ι) such that every ab′ i equals a(i) times b′ i, i.e. ab′ i = a(i)·b′ i for all i.
Русский
Пусть R — кольцо главных идеалов (PID) и M — конечный свободный модуль над R. Пусть N — подмодуль M той же ранги. Тогда существуют база b′ модуля M, функция a:ι→R и база ab′ модуля N с тем же индексным множеством ι, такие что каждый элемент ab′ i равен a(i) умноженному на b′ i: ab′ i = a(i)·b′ i для всех i.
LaTeX
$$$\exists b' : \mathrm{Basis}\ ι\ R\ M,\ \exists a : ι \to R,\ \exists ab' : \mathrm{Basis}\ ι\ R\ N,\ \forall i,\ (ab'\ i : M) = a\ i \cdot b'\ i$$$
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 also `Submodule.smithNormalFormOfRankEq` for a version of this theorem that returns
a `Basis.SmithNormalForm`.
-/
theorem exists_smith_normal_form_of_rank_eq (b : Basis ι R M) (h : Module.finrank R N = Module.finrank R M) :
∃ (b' : Basis ι R M) (a : ι → R) (ab' : Basis ι R N), ∀ i, (ab' i : M) = a i • b' i :=
by
cases nonempty_fintype ι
let ⟨bM, bN, f, a, snf⟩ := N.smithNormalFormOfRankEq b h
let e : Fin (Fintype.card ι) ≃ ι :=
Equiv.ofBijective f ((Fintype.bijective_iff_injective_and_card f).mpr ⟨f.injective, Fintype.card_fin _⟩)
have fe : ∀ i, f (e.symm i) = i := e.apply_symm_apply
exact ⟨bM, a ∘ e.symm, bN.reindex e, fun i ↦ by simp only [snf, fe, Basis.coe_reindex, (· ∘ ·)]⟩
