English
Let R be a ring, M an R-module, and b a basis of M. For a submodule N ⊆ M and a linear map φ: M → R, suppose N.map φ is a principal ideal with generator equal to 0, and suppose there is no other linear map ψ with N.map φ < N.map ψ (i.e., N.map φ is maximal among the submodule images). Then N must be the zero submodule.
Русский
Пусть R — кольцо, M — R-модуль, и пусть b — база M. Пусть N ⊆ M и линейное отображение φ: M → R так, что образ N через φ являетсяPrincipal-образующей идеал с порождающим 0, и при этом нет такого ψ, чтобы образ N через φ был строгим меньшим образом образа через ψ. Тогда N = {0}.
LaTeX
$$$\\forall R, M, b, N \\subseteq M, \\varphi: M \\to_R R,\\; [(N.map \\varphi) \\text{ principal}] \n\\; (generator (N.map \\varphi) = 0) \\Rightarrow N = \\{0\\}$ with the maximality condition $\\forall \\psi: M \\to_R R, \\; N.map \\varphi < N.map \\psi$ is false.$$
Lean4
theorem eq_bot_of_generator_maximal_map_eq_zero (b : Basis ι R M) {N : Submodule R M} {ϕ : M →ₗ[R] R}
(hϕ : ∀ ψ : M →ₗ[R] R, ¬N.map ϕ < N.map ψ) [(N.map ϕ).IsPrincipal] (hgen : generator (N.map ϕ) = (0 : R)) : N = ⊥ :=
by
rw [Submodule.eq_bot_iff]
intro x hx
refine b.ext_elem fun i ↦ ?_
rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ
rw [LinearEquiv.map_zero, Finsupp.zero_apply]
exact (Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _ ⟨x, hx, rfl⟩
