English
For submodules N ⊆ M ⊆ O and a linear map ϕ: O → R, if the generator of the submodule image ϕ.submoduleImage N is zero, then N must be the bottom submodule.
Русский
Для подсубмодулей N ⊆ M ⊆ O и линейного отображения ϕ: O → R, если порождающая подмодуля-образа ϕ.submoduleImage N равна нулю, то N = ⊥.
LaTeX
$$$\\forall N \\le M \\le O,\\; ϕ: O \\to_R R,\\; [(ϕ.submoduleImage N).IsPrincipal] \\land (generator (ϕ.submoduleImage N) = 0) \\Rightarrow N = \\bot$.$$
Lean4
theorem eq_bot_of_generator_maximal_submoduleImage_eq_zero {N O : Submodule R M} (b : Basis ι R O) (hNO : N ≤ O)
{ϕ : O →ₗ[R] R} (hϕ : ∀ ψ : O →ₗ[R] R, ¬ϕ.submoduleImage N < ψ.submoduleImage N) [(ϕ.submoduleImage N).IsPrincipal]
(hgen : generator (ϕ.submoduleImage N) = 0) : N = ⊥ :=
by
rw [Submodule.eq_bot_iff]
intro x hx
refine (mk_eq_zero _ _).mp (show (⟨x, hNO hx⟩ : O) = 0 from b.ext_elem fun i ↦ ?_)
rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ
rw [LinearEquiv.map_zero, Finsupp.zero_apply]
refine (Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _ ?_
exact (LinearMap.mem_submoduleImage_of_le hNO).mpr ⟨x, hx, rfl⟩
