English
For a PID and a submodule N of a free module M, there exists a finite basis for N (as a submodule of M).
Русский
Если R — PID и N — подмодуль свободного модуля M, то для N существует конечная база как подмодуля M.
LaTeX
$$$\\exists n, \\text{Basis} (Fin n) R N$$$
Lean4
/-- A submodule of a free `R`-module of finite rank is also a free `R`-module of finite rank,
if `R` is a principal ideal domain.
This is a `lemma` to make the induction a bit easier. To actually access the basis,
see `Submodule.basisOfPid`.
See also the stronger version `Submodule.smithNormalForm`.
-/
theorem nonempty_basis_of_pid {ι : Type*} [Finite ι] (b : Basis ι R M) (N : Submodule R M) :
∃ n : ℕ, Nonempty (Basis (Fin n) R N) := by
haveI := Classical.decEq M
cases nonempty_fintype ι
induction N using inductionOnRank b with
| ih N ih =>
let b' := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop _ rfl).symm
by_cases N_bot : N = ⊥
· subst N_bot
exact ⟨0, ⟨Basis.empty _⟩⟩
obtain ⟨y, -, a, hay, M', -, N', N'_le_N, -, -, ay_ortho, h'⟩ := Submodule.basis_of_pid_aux ⊤ N b' N_bot le_top
obtain ⟨n', ⟨bN'⟩⟩ := ih N' N'_le_N _ hay ay_ortho
obtain ⟨bN, _hbN⟩ := h' n' bN'
exact ⟨n' + 1, ⟨bN⟩⟩
