English
For a finite module M over R, there exists a nontrivial quotient by an ideal I of R such that there exists a surjective linear map M → R/I.
Русский
Для конечного модуля M существует ненулевой частный/фактор по идеалу I такого, что существует сюрьективный линейный отображение M → R/I.
LaTeX
$$$\exists I \neq R,\; \exists f: M \to R/I \text{ surjective}$$$
Lean4
theorem exists_surjective_quotient_of_finite : ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I), I ≠ ⊤ ∧ Function.Surjective f :=
by
obtain ⟨N, hN, ⟨x, hx⟩⟩ := Module.exists_isPrincipal_quotient_of_finite R M
let f :=
(LinearMap.toSpanSingleton R _ x).quotKerEquivOfSurjective
(by rw [← LinearMap.range_eq_top, ← LinearMap.span_singleton_eq_range, hx])
refine ⟨_, f.symm.toLinearMap.comp N.mkQ, fun e ↦ ?_, f.symm.surjective.comp N.mkQ_surjective⟩
obtain rfl : x = 0 := by simpa using LinearMap.congr_fun (LinearMap.ker_eq_top.mp e) 1
rw [ne_eq, ← Submodule.subsingleton_quotient_iff_eq_top, ← not_nontrivial_iff_subsingleton, not_not] at hN
simp at hx
