English
If each N(i) is finitely generated, then for a Noetherian ring R and finite module M, the submodule F.submodule is finitely generated if and only if the filtration F is stable.
Русский
Если каждый N(i) конечнопорождён, то при Noetherian кольце R и конечном модуле M подмодуль F.submodule конечнопорождён тогда и только тогда, когда фильтрация F стабильна.
LaTeX
$$$(\\forall i, (F.N(i)).FG) \\rightarrow (F.submodule.FG \\iff F.Stable).$$$
Lean4
/-- If the components of a filtration are finitely generated, then the filtration is stable iff
its associated submodule of is finitely generated. -/
theorem submodule_fg_iff_stable (hF' : ∀ i, (F.N i).FG) : F.submodule.FG ↔ F.Stable := by
classical
delta Ideal.Filtration.Stable
simp_rw [← F.submodule_eq_span_le_iff_stable_ge]
constructor
· rintro H
refine H.stabilizes_of_iSup_eq ⟨fun n₀ => Submodule.span _ (⋃ (i : ℕ) (_ : i ≤ n₀), single R i '' ↑(F.N i)), ?_⟩ ?_
· intro n m e
rw [Submodule.span_le, Set.iUnion₂_subset_iff]
intro i hi
refine Set.Subset.trans ?_ Submodule.subset_span
refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_
exact hi.trans e
· dsimp
rw [← Submodule.span_iUnion, ← submodule_span_single]
congr 1
ext
simp only [Set.mem_iUnion, Set.mem_image, SetLike.mem_coe, exists_prop]
constructor
· rintro ⟨-, i, -, e⟩; exact ⟨i, e⟩
· rintro ⟨i, e⟩; exact ⟨i, i, le_refl i, e⟩
· rintro ⟨n, hn⟩
rw [hn]
simp_rw [Submodule.span_iUnion₂, ← Finset.mem_range_succ_iff, iSup_subtype']
apply Submodule.fg_iSup
rintro ⟨i, hi⟩
obtain ⟨s, hs⟩ := hF' i
have :
Submodule.span (reesAlgebra I) (s.image (lsingle R i) : Set (PolynomialModule R M)) =
Submodule.span _ (single R i '' (F.N i : Set M)) :=
by rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs]; rfl
rw [Subtype.coe_mk, ← this]
exact ⟨_, rfl⟩
