feat: power series over a noetherian ring is noetherian (#31149)

We add that the power series ring over a noetherian ring is noetherian.

Author: riccardobrasca

Mathlib.lean

@@ -6030,6 +6030,7 @@ public import Mathlib.RingTheory.PowerSeries.CoeffMulMem
 public import Mathlib.RingTheory.PowerSeries.Derivative
 public import Mathlib.RingTheory.PowerSeries.Evaluation
 public import Mathlib.RingTheory.PowerSeries.GaussNorm
+public import Mathlib.RingTheory.PowerSeries.Ideal
 public import Mathlib.RingTheory.PowerSeries.Inverse
 public import Mathlib.RingTheory.PowerSeries.NoZeroDivisors
 public import Mathlib.RingTheory.PowerSeries.Order

Mathlib/Algebra/Module/SpanRank.lean

@@ -5,11 +5,9 @@ Authors: Wanyi He, Jiedong Jiang, Xuchun Li, Christian Merten, Jingting Wang, An
 -/
 module
 
-public import Mathlib.Data.Set.Card
 public import Mathlib.Data.ENat.Lattice
-public import Mathlib.RingTheory.Finiteness.Defs
-public import Mathlib.LinearAlgebra.FreeModule.Basic
 public import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
+public import Mathlib.RingTheory.Finiteness.Ideal
 
 /-!
 # Minimum Cardinality of generating set of a submodule
@@ -118,6 +116,12 @@ lemma spanRank_finite_iff_fg {p : Submodule R M} : p.spanRank < aleph0 ↔ p.FG
   · rintro ⟨s, hs₁, hs₂⟩
     exact (ciInf_le' _ ⟨s, hs₂⟩).trans_lt (by simpa)
 
+lemma spanFinrank_of_not_fg {p : Submodule R M} (hp : ¬p.FG) : p.spanFinrank = 0 := by
+  refine toNat_eq_zero.2 ?_
+  right
+  by_contra! h
+  exact hp (spanRank_finite_iff_fg.1 h)
+
 /-- A submodule is finitely generated if and only if its `spanRank` is equal to its `spanFinrank`.
 -/
 lemma fg_iff_spanRank_eq_spanFinrank {p : Submodule R M} : p.spanRank = p.spanFinrank ↔ p.FG := by
@@ -247,15 +251,58 @@ lemma spanFinrank_singleton {m : M} (hm : m ≠ 0) : (span R {m}).spanFinrank =
     simp [Submodule.spanFinrank_eq_zero_iff_eq_bot (fg_span_singleton m), hm] at this
 
 end Defs
+
 end Submodule
 
+section map
+
+universe u
+section Submodule
+
+variable {R : Type*} {M N : Type u} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N]
+  [Module R N] (f : M →ₗ[R] N) (p : Submodule R M)
+
+lemma Submodule.spanRank_map_le : (p.map f).spanRank ≤ p.spanRank := by
+  rw [← generators_card p, FG.spanRank_le_iff_exists_span_set_card_le]
+  exact ⟨f '' p.generators, Cardinal.mk_image_le, le_antisymm (span_le.2 (fun n ⟨m, hm, h⟩ ↦
+    ⟨m, span_generators p ▸ subset_span hm, h⟩)) (by simp [span_generators])⟩
+
+variable {p} in
+lemma Submodule.spanFinrank_map_le_of_fg (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank :=
+  (Cardinal.toNat_le_iff_le_of_lt_aleph0 (spanRank_finite_iff_fg.mpr (FG.map f hp))
+    (spanRank_finite_iff_fg.mpr hp)).2 (p.spanRank_map_le f)
+
+end Submodule
+
+section Ideal
+
+variable {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (I : Ideal R)
+
+open Submodule in
+lemma Ideal.spanRank_map_le : (I.map f).spanRank ≤ I.spanRank := by
+  rw [← generators_card I, FG.spanRank_le_iff_exists_span_set_card_le]
+  refine ⟨f '' I.generators, Cardinal.mk_image_le, le_antisymm (span_le.2 (fun s ⟨r, hr, hfr⟩ ↦
+    hfr ▸ mem_map_of_mem _ <| span_generators I ▸ subset_span hr)) ?_⟩
+  refine map_le_of_le_comap (fun r hr ↦ ?_)
+  simp only [submodule_span_eq, mem_comap]
+  rw [← map_span, ← submodule_span_eq, span_generators]
+  exact mem_map_of_mem f hr
+
+open Submodule in
+variable {I} in
+lemma Ideal.spanFinrank_map_le_of_fg (hI : I.FG) : (I.map f).spanFinrank ≤ I.spanFinrank :=
+  (Cardinal.toNat_le_iff_le_of_lt_aleph0 (spanRank_finite_iff_fg.mpr (Ideal.FG.map hI f))
+    ((spanRank_finite_iff_fg.mpr hI))).2 (spanRank_map_le f I)
+
+end Ideal
+
+end map
+
 section rank
 
 open Cardinal Module Submodule
 
-universe u v w
-
-variable {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M]
+variable {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
 
 lemma Module.Basis.mk_eq_spanRank [RankCondition R] {ι : Type*} (v : Basis ι R M) :
     #(Set.range v) = (⊤ : Submodule R M).spanRank := by

Mathlib/RingTheory/PowerSeries/Ideal.lean

@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2025 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca, Anthony Fernandes, Marc Robin
+-/
+module
+
+public import Mathlib.RingTheory.PowerSeries.Inverse
+public import Mathlib.RingTheory.PowerSeries.Trunc
+public import Mathlib.RingTheory.Finiteness.Ideal
+public import Mathlib.RingTheory.Noetherian.OfPrime
+public import Mathlib.Algebra.Module.SpanRank
+
+/-!
+# Ideals in power series.
+
+We gather miscellaneous results about prime ideals in `R⟦X⟧`. More precisely, we prove that, given
+a prime ideal `I` of `R⟦X⟧`, if the ideal generated by the constant coefficients of the `f ∈ I` is
+generated by `n` elements, then `I` is generated by at most `n + 1` elements (actually it is
+generated by `n` elements if `X ∉ I` and `n + 1` elements otherwise). This implies immediately that
+`R⟦X⟧` is noetherian if `R` is. The proof of `eq_of_le_of_X_notMem_of_fg_of_isPrime` is inspired by
+[zbMATH05171613].
+
+
+## Main results
+
+* `PowerSeries.eq_span_insert_X_of_X_mem_of_span_eq` : given an ideal `I` of `R⟦X⟧` such that
+  `X ∈ I`, if `I.map constantCoeff` is generated by `S : Set T`, then `I` is generated by
+  `insert X (C '' S)`.
+* `PowerSeries.exist_eq_span_eq_ncard_of_X_notMem` : given a prime ideal `I` of `R⟦X⟧` such
+  that `X ∉ I`, if `I.map constantCoeff` is generated by a finite set `S : Set T`, then there exists
+  `T : Set R`, of the same cardinality as `S`, that generates `I`.
+* `PowerSeries.fg_iff_of_isPrime` : a prime ideal `P` of `R⟦X⟧` is finitely generated if and only
+  if `P.map constantCoeff` is finitely generated.
+
+
+## Implementation details
+
+There is a simpler proof of `IsNoetherianRing R → IsNoetherianRing R⟦X⟧`, similar to that for
+polynomials. On the other hand our proof has the advantage of giving explicitly the number of
+generators, and it will be used to prove that, for a domain `R`, we have
+`IsPrincipalIdealRing R → UniqueFactorizationMonoid R⟦X⟧`.
+
+## TODO
+Prove noetherianity of `MvPowerSeries` in finitely many variables.
+
+-/
+
+variable {R : Type*}
+
+open Ideal Set Finset
+
+namespace PowerSeries
+variable [CommRing R] {I : Ideal R⟦X⟧} {S : Set R}
+
+section X_mem
+
+theorem map_constantCoeff_le_self_of_X_mem (hXI : X ∈ I) :
+    I.map (C.comp constantCoeff) ≤ I := by
+  suffices ∀ x ∈ I, C (constantCoeff x) ∈ I by simpa [Ideal.map_le_iff_le_comap]
+  intro f hf
+  rw [← sub_eq_iff_eq_add'.mpr f.eq_X_mul_shift_add_const]
+  exact sub_mem hf (I.mul_mem_right _ hXI)
+
+/-- Given an ideal `I` of `R⟦X⟧` such that `X ∈ I`, if `I.map constantCoeff` is generated by
+`S : Set T`, then `I` is generated by `insert X (C '' S)`. -/
+theorem eq_span_insert_X_of_X_mem_of_span_eq (hXI : X ∈ I) (hSI : span S = I.map constantCoeff) :
+    I = span (insert X (C '' S)) := by
+  rw [Ideal.span_insert, ← Ideal.map_span, hSI, Ideal.map_map]
+  refine le_antisymm ?_ (by simp [Ideal.span_le, hXI, map_constantCoeff_le_self_of_X_mem])
+  exact fun f hf ↦ mem_span_singleton_sup.mpr
+    ⟨_, _, mem_map_of_mem _ hf, f.eq_shift_mul_X_add_const.symm⟩
+
+open Submodule in
+theorem spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem (hI : X ∈ I) :
+    spanFinrank I ≤ spanFinrank (I.map constantCoeff) + 1 := by
+  by_cases hfg : I.FG
+  swap; · exact spanFinrank_of_not_fg hfg ▸ Nat.zero_le _
+  replace hfg : (Ideal.map constantCoeff I).FG := by
+    have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
+    exact map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg
+  nth_rw 1 [eq_span_insert_X_of_X_mem_of_span_eq hI (I.map constantCoeff).span_generators]
+  refine le_trans (spanFinrank_span_le_ncard_of_finite ?_) (le_trans (Set.ncard_insert_le _ _) ?_)
+  · simpa using Set.Finite.map _ (FG.finite_generators hfg)
+  · simp only [add_le_add_iff_right]
+    refine le_trans (Set.ncard_image_le (FG.finite_generators hfg)) ?_
+    rw [FG.generators_ncard hfg]
+
+end X_mem
+
+section X_notMem
+
+variable (hXI : X ∉ I) [I.IsPrime]
+
+theorem eq_of_le_of_X_notMem_of_fg_of_isPrime {J : Ideal R⟦X⟧} (hJI : J ≤ I) (hXI : X ∉ I)
+    (hJ : J.FG) (h' : I.map constantCoeff ≤ J.map constantCoeff) : I = J := by
+  refine hJI.antisymm' ?_
+  replace h' := h'.antisymm (Ideal.map_mono hJI)
+  obtain ⟨n, F, rfl⟩ := Submodule.fg_iff_exists_fin_generating_family.mp hJ
+  rw [submodule_span_eq, map_span, ← Set.range_comp] at h'
+  choose! T hT using fun g (hg : g ∈ I) ↦
+    mem_span_range_iff_exists_fun.mp (h'.le (Ideal.mem_map_of_mem _ hg))
+  dsimp at hT
+  intro g hg
+  let G : ℕ → R⟦X⟧ :=
+    Nat.rec g fun _ G' ↦ mk fun p ↦ coeff (p + 1) G' - ∑ i, T G' i * coeff (p + 1) (F i)
+  have hG' (n : ℕ) (H : G n ∈ I) : G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1) := by
+    simpa [hT _ H] using sub_const_eq_X_mul_shift (G n - ∑ i, C (T (G n) i) * F i)
+  have hG : ∀ n, G n ∈ I := Nat.rec hg fun n IH ↦
+    (‹I.IsPrime›.mul_mem_iff_mem_or_mem.mp (hG' n IH ▸ I.sub_mem IH (I.sum_mem fun i _ ↦
+      I.mul_mem_left _ (hJI (subset_span (Set.mem_range_self _)))))).resolve_left hXI
+  replace hG' := fun n ↦ hG' n (hG n)
+  let H (i : Fin n) : R⟦X⟧ := mk fun n ↦ T (G n) i
+  have h₁ (n : ℕ) : g - ∑ i, trunc n (H i) * F i = X ^ n * G n := by
+    induction n with
+    | zero => simp [G]
+    | succ n IH =>
+      simp [trunc_succ, add_mul, sum_add_distrib, ← sub_sub, IH, pow_succ, mul_assoc, ← hG',
+        mul_sub, H, mul_sum, monomial_eq_C_mul_X_pow, mul_left_comm (C _)]
+  have h₂ : g = ∑ i, H i * F i := by
+    ext n; simpa [coeff_trunc, sub_eq_zero] using congr(($(h₁ (n + 1)).trunc (n + 1)).coeff n)
+  rw [h₂]
+  exact Ideal.sum_mem _ fun i _ ↦ Ideal.mul_mem_left _ _ (subset_span (Set.mem_range_self _))
+
+/-- Given a prime ideal `I` of `R⟦X⟧` such that `X ∉ I`, if `I.map constantCoeff` is generated by a
+finite set `S : Set T`, then there exists `T : Set R`, of the same cardinality as `S`, that
+generates `I`. -/
+theorem exist_eq_span_eq_ncard_of_X_notMem (hI : X ∉ I) {S : Set R}
+    (hSI : span S = I.map constantCoeff) (hS : S.Finite) :
+      ∃ T, I = span T ∧ T.Finite ∧ T.ncard = S.ncard := by
+  have : SurjOn constantCoeff I S := by
+    intro r hr
+    simpa [mem_map_iff_of_surjective _ constantCoeff_surj, hSI] using subset_span hr
+  obtain ⟨T, hTI, hinj, hT⟩ := this.exists_subset_injOn_image_eq
+  refine ⟨T, eq_of_le_of_X_notMem_of_fg_of_isPrime (span_le.2  hTI) hI (Submodule.fg_def.2
+    ⟨T, (hT ▸ hS).of_finite_image hinj, rfl⟩) ?_, Finite.of_injOn
+    (fun f hf ↦ hT ▸ Set.mem_image_of_mem _ hf) hinj hS, hT ▸ (ncard_image_of_injOn hinj).symm⟩
+  rw [map_le_iff_le_comap]
+  intro f hf
+  rw [mem_comap, mem_map_iff_of_surjective _ constantCoeff_surj]
+  replace hf : constantCoeff f ∈ span S := hSI ▸ Ideal.mem_map_of_mem constantCoeff hf
+  refine Submodule.span_induction (fun s hs ↦ ?_) ⟨0, zero_mem _, by simp⟩ ?_ ?_ hf
+  · obtain ⟨t, htmem, ht⟩ := hT ▸ hs
+    exact ⟨t, subset_span htmem, ht⟩
+  · intro r₁ r₂ hr₁ hr₂ ⟨s₁, hs₁mem, hs₁⟩ ⟨s₂, hs₂mem, hs₂⟩
+    exact ⟨s₁ + s₂, Ideal.add_mem _ hs₁mem hs₂mem, by simp [hs₁, hs₂]⟩
+  · intro r₁ r₂ hr₁ ⟨f, hfmem, hf⟩
+    exact ⟨r₁ • f, Submodule.smul_of_tower_mem _ _ hfmem, by simp [hf]⟩
+
+open Submodule in
+theorem spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime (hI : X ∉ I)
+    (hfg : I.FG) : spanFinrank I = spanFinrank (I.map constantCoeff) := by
+  refine le_antisymm ?_ ?_
+  swap; · exact Ideal.spanFinrank_map_le_of_fg constantCoeff hfg
+  have : RingHomSurjective (constantCoeff (R := R)) := ⟨constantCoeff_surj⟩
+  obtain ⟨S, rfl, hS, hScard⟩ := exist_eq_span_eq_ncard_of_X_notMem hI
+    (I.map constantCoeff).span_generators
+    (FG.finite_generators <| map_eq_submodule_map constantCoeff I ▸ Submodule.FG.map _ hfg)
+  refine le_trans (spanFinrank_span_le_ncard_of_finite hS) ?_
+  rw [hScard, FG.generators_ncard]
+  exact map_eq_submodule_map constantCoeff (Ideal.span S) ▸ Submodule.FG.map _ hfg
+
+end X_notMem
+
+variable {P : Ideal R⟦X⟧} [P.IsPrime]
+
+open Submodule in
+theorem spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime :
+    spanFinrank P ≤ spanFinrank (P.map constantCoeff) + 1 := by
+  by_cases hfg : P.FG
+  swap; · exact spanFinrank_of_not_fg hfg ▸ Nat.zero_le _
+  by_cases hP : X ∈ P
+  · exact spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem hP
+  · exact le_trans (spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime
+      hP hfg).le (Nat.le_succ _)
+
+/-- A prime ideal `P` of `R⟦X⟧` is finitely generated if and only if `P.map constantCoeff` is
+finitely generated. -/
+lemma fg_iff_of_isPrime : P.FG ↔ (P.map constantCoeff).FG := by
+  constructor
+  · exact (FG.map · _)
+  · intro ⟨S, hS⟩
+    by_cases hX : X ∈ P
+    · have H := eq_span_insert_X_of_X_mem_of_span_eq hX hS
+      have : (insert X <| (C (R := R)) '' S).Finite :=
+        Finite.insert X <| Finite.image _ S.finite_toSet
+      lift insert X <| (C (R := R)) '' S to Finset R⟦X⟧ using this with T hT
+      exact ⟨T, hT ▸ H.symm⟩
+    · obtain ⟨T, hT, hT₂, _⟩ := exist_eq_span_eq_ncard_of_X_notMem hX hS S.finite_toSet
+      lift T to Finset R⟦X⟧ using hT₂
+      exact ⟨T, hT.symm⟩
+
+/-- If `R` is noetherian then so is `R⟦X⟧`. -/
+instance [IsNoetherianRing R] : IsNoetherianRing R⟦X⟧ :=
+  IsNoetherianRing.of_prime fun P _ ↦
+    fg_iff_of_isPrime.2 <| (isNoetherianRing_iff_ideal_fg R).1 inferInstance (P.map constantCoeff)
+
+end PowerSeries

Mathlib/RingTheory/PowerSeries/Trunc.lean

@@ -37,19 +37,29 @@ section Trunc
 variable [Semiring R]
 open Finset Nat
 
-/-- The `n`th truncation of a formal power series to a polynomial -/
-def trunc (n : ℕ) (φ : R⟦X⟧) : R[X] :=
+private def trunc_aux (n : ℕ) (φ : R⟦X⟧) : R[X] :=
   ∑ m ∈ Ico 0 n, Polynomial.monomial m (coeff m φ)
 
+private theorem coeff_trunc_aux (m) (n) (φ : R⟦X⟧) :
+    (trunc_aux n φ).coeff m = if m < n then coeff m φ else 0 := by
+  simp [trunc_aux, Polynomial.coeff_monomial]
+
+/-- The `n`th truncation of a formal power series to a polynomial. -/
+def trunc (n : ℕ) : R⟦X⟧ →ₗ[R] R[X] where
+  toFun := trunc_aux n
+  map_add' φ ψ := Polynomial.ext fun m => by
+    simp only [coeff_trunc_aux, Polynomial.coeff_add]
+    split_ifs with H
+    · rfl
+    · rw [zero_add]
+  map_smul' t φ := by ext; simp [trunc_aux, Polynomial.coeff_monomial]
+
+lemma trunc_apply (n : ℕ) (φ : R⟦X⟧) :
+  trunc n φ = ∑ m ∈ Ico 0 n, Polynomial.monomial m (coeff m φ) := rfl
+
 theorem coeff_trunc (m) (n) (φ : R⟦X⟧) :
     (trunc n φ).coeff m = if m < n then coeff m φ else 0 := by
-  simp [trunc, Polynomial.coeff_monomial]
-
-@[simp]
-theorem trunc_zero (n) : trunc n (0 : R⟦X⟧) = 0 :=
-  Polynomial.ext fun m => by
-    rw [coeff_trunc, LinearMap.map_zero, Polynomial.coeff_zero]
-    split_ifs <;> rfl
+  simp [trunc, coeff_trunc_aux]
 
 @[simp]
 theorem trunc_one (n) : trunc (n + 1) (1 : R⟦X⟧) = 1 :=
@@ -62,17 +72,9 @@ theorem trunc_C (n) (a : R) : trunc (n + 1) (C a) = Polynomial.C a :=
     rw [coeff_trunc, coeff_C, Polynomial.coeff_C]
     split_ifs with H <;> first | rfl | try simp_all
 
-@[simp]
-theorem trunc_add (n) (φ ψ : R⟦X⟧) : trunc n (φ + ψ) = trunc n φ + trunc n ψ :=
-  Polynomial.ext fun m => by
-    simp only [coeff_trunc, Polynomial.coeff_add]
-    split_ifs with H
-    · rfl
-    · rw [zero_add]
-
 theorem trunc_succ (f : R⟦X⟧) (n : ℕ) :
     trunc n.succ f = trunc n f + Polynomial.monomial n (coeff n f) := by
-  rw [trunc, Ico_zero_eq_range, sum_range_succ, trunc, Ico_zero_eq_range]
+  rw [trunc_apply, Ico_zero_eq_range, sum_range_succ, trunc_apply, Ico_zero_eq_range]
 
 theorem natDegree_trunc_lt (f : R⟦X⟧) (n) : (trunc (n + 1) f).natDegree < n + 1 := by
   rw [Nat.lt_succ_iff, natDegree_le_iff_coeff_eq_zero]
@@ -155,6 +157,13 @@ lemma eq_X_pow_mul_shift_add_trunc (n : ℕ) (f : R⟦X⟧) :
     f = X ^ n * (mk fun i ↦ coeff (i + n) f) + (f.trunc n : R⟦X⟧) := by
   rw [← (commute_X_pow _ n).eq, ← eq_shift_mul_X_pow_add_trunc]
 
+lemma monomial_eq_C_mul_X_pow (r : R) (n : ℕ) : monomial n r = C r * X ^ n := by
+  ext; simp [coeff_X_pow, coeff_monomial]
+
+@[simp]
+lemma trunc_X_pow_self_mul (n : ℕ) (p : R⟦X⟧) : (X ^ n * p).trunc n = 0 := by
+  ext; simp +contextual [coeff_trunc, coeff_X_pow_mul']
+
 end Trunc
 
 section Trunc
@@ -237,6 +246,17 @@ theorem coeff_mul_eq_coeff_trunc_mul_trunc {d n} (f g) (h : d < n) :
 
 end Trunc
 
+section Ring
+
+variable [Ring R]
+
+@[simp]
+lemma trunc_sub (n : ℕ) (φ ψ : R⟦X⟧) : trunc n (φ - ψ) = trunc n φ - trunc n ψ := by
+  ext i
+  simp
+
+end Ring
+
 section Map
 variable {S : Type*} [Semiring R] [Semiring S] (f : R →+* S)