English
Existence of Smith normal form data satisfying rank-equality constraints and matching embeddings.
Русский
Существование данных SmithNormalForm, удовлетворяющих ограничениям по рангу и сопоставлениям вложений.
LaTeX
$$$smithNormalFormOfRankEq$ with rank equality constraints$$
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.smithNormalFormOfLE` for a version of this theorem that returns
a `Basis.SmithNormalForm`.
This is a strengthening of `Submodule.basisOfPidOfLE`.
-/
theorem exists_smith_normal_form_of_le [Finite ι] (b : Basis ι R M) (N O : Submodule R M) (N_le_O : N ≤ O) :
∃ (n o : ℕ) (hno : n ≤ o) (bO : Basis (Fin o) R O) (bN : Basis (Fin n) R N) (a : Fin n → R),
∀ i, (bN i : M) = a i • bO (Fin.castLE hno i) :=
by
cases nonempty_fintype ι
induction O using inductionOnRank b generalizing N with
| ih M0 ih =>
obtain ⟨m, b'M⟩ := M0.basisOfPid b
by_cases N_bot : N = ⊥
· subst N_bot
exact ⟨0, m, Nat.zero_le _, b'M, Basis.empty _, finZeroElim, finZeroElim⟩
obtain ⟨y, hy, a, _, M', M'_le_M, N', _, N'_le_M', y_ortho, _, h⟩ :=
Submodule.basis_of_pid_aux M0 N b'M N_bot N_le_O
obtain ⟨n', m', hn'm', bM', bN', as', has'⟩ := ih M' M'_le_M y hy y_ortho N' N'_le_M'
obtain ⟨bN, h'⟩ := h n' bN'
obtain ⟨hmn, bM, h''⟩ := h' m' hn'm' bM'
obtain ⟨as, has⟩ := h'' as' has'
exact ⟨_, _, hmn, bM, bN, as, has⟩
