English
For any ideal I with h : M ≤ nonZeroDivisors R, the image coeSubmodule(S,I) is principal iff I is principal.
Русский
Для любого идеала I с условием h, образ coeSubmodule(S,I) является главной порождающей, тогда и только тогда, когда I является главной порождающей.
LaTeX
$$coeSubmodule_isPrincipal : {I : Ideal R} (h : M ≤ nonZeroDivisors R) : (coeSubmodule S I).IsPrincipal ↔ I.IsPrincipal$$
Lean4
theorem coeSubmodule_isPrincipal {I : Ideal R} (h : M ≤ nonZeroDivisors R) :
(coeSubmodule S I).IsPrincipal ↔ I.IsPrincipal :=
by
constructor <;> rintro ⟨⟨x, hx⟩⟩
· have x_mem : x ∈ coeSubmodule S I := hx.symm ▸ Submodule.mem_span_singleton_self x
obtain ⟨x, _, rfl⟩ := (mem_coeSubmodule _ _).mp x_mem
refine ⟨⟨x, coeSubmodule_injective S h ?_⟩⟩
rw [Ideal.submodule_span_eq, hx, coeSubmodule_span_singleton]
· refine ⟨⟨algebraMap R S x, ?_⟩⟩
rw [hx, Ideal.submodule_span_eq, coeSubmodule_span_singleton]
