English
A Noetherian property for a submodule can be equivalently stated by intersections with other submodules.
Русский
Свойство Ноетеровости подмодуля может формулироваться эквивалентно через пересечения с другими подмодулями.
LaTeX
$$$IsNoetherian(R,N) \iff ∀ s, (N \cap s).FG$$$
Lean4
theorem isNoetherian_submodule {N : Submodule R M} : IsNoetherian R N ↔ ∀ s : Submodule R M, s ≤ N → s.FG :=
by
refine
⟨fun ⟨hn⟩ => fun s hs =>
have : s ≤ LinearMap.range N.subtype := N.range_subtype.symm ▸ hs
Submodule.map_comap_eq_self this ▸ (hn _).map _,
fun h => ⟨fun s => ?_⟩⟩
have f := (Submodule.equivMapOfInjective N.subtype Subtype.val_injective s).symm
have h₁ := h (s.map N.subtype) (Submodule.map_subtype_le N s)
have h₂ : (⊤ : Submodule R (s.map N.subtype)).map f = ⊤ := by simp
have h₃ := ((Submodule.fg_top _).2 h₁).map (↑f : _ →ₗ[R] s)
exact (Submodule.fg_top _).1 (h₂ ▸ h₃)
