English
For a finitely generated module M over R with M nontrivial, there exists a submodule N ⊊ M such that ⊤/(N) is a principal module.
Русский
Для ненулевого модуля M над R существует подмодуль N ⊊ M, для которого общеобразовательный фактор-модуль ⊤/N является главной (principal).
LaTeX
$$$\exists N \le M, N \neq M,\; \top/M \text{ is principal}$$$
Lean4
theorem exists_isPrincipal_quotient_of_finite :
∃ N : Submodule R M, N ≠ ⊤ ∧ Submodule.IsPrincipal (⊤ : Submodule R (M ⧸ N)) :=
by
obtain ⟨n, f, hf⟩ := @Module.Finite.exists_fin R M _ _ _ _
let s := {m : ℕ | Submodule.span R (f '' (Fin.val ⁻¹' (Set.Iio m))) ≠ ⊤}
have hns : ∀ x ∈ s, x < n := by
refine fun x hx ↦ lt_iff_not_ge.mpr fun e ↦ ?_
have : (Fin.val ⁻¹' Set.Iio x : Set (Fin n)) = Set.univ := by ext y; simpa using y.2.trans_le e
simp [s, this, hf] at hx
have hs₁ : s.Nonempty := ⟨0, by simp [s]⟩
have hs₂ : BddAbove s := ⟨n, fun x hx ↦ (hns x hx).le⟩
have hs := Nat.sSup_mem hs₁ hs₂
refine ⟨_, hs, ⟨⟨Submodule.mkQ _ (f ⟨_, hns _ hs⟩), ?_⟩⟩⟩
have := not_not.mp (notMem_of_csSup_lt (Order.lt_succ _) hs₂)
rw [← Set.image_singleton, ← Submodule.map_span, ←
(Submodule.comap_injective_of_surjective (Submodule.mkQ_surjective _)).eq_iff, Submodule.comap_map_eq,
Submodule.ker_mkQ, Submodule.comap_top, ← this, ← Submodule.span_union, Order.Iio_succ_eq_insert (sSup s), ←
Set.union_singleton, Set.preimage_union, Set.image_union, ← @Set.image_singleton _ _ f, Set.union_comm]
congr!
ext
simp [Fin.ext_iff]
