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 [Wat07].

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 is used to prove that, for a domain R, we have IsPrincipalIdealRing R → UniqueFactorizationMonoid R⟦X⟧.

TODO #

Prove noetherianity of MvPowerSeries in finitely many variables.

source

theorem PowerSeries.map_constantCoeff_le_self_of_X_mem {R : Type u_1} [CommRing R] {I : Ideal (PowerSeries R)} (hXI : X ∈ I) :

Ideal.map (C.comp constantCoeff) I ≤ I

source

theorem PowerSeries.eq_span_insert_X_of_X_mem_of_span_eq {R : Type u_1} [CommRing R] {I : Ideal (PowerSeries R)} {S : Set R} (hXI : X ∈ I) (hSI : Ideal.span S = Ideal.map constantCoeff I) :

I = Ideal.span (insert X (⇑C '' S))

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).

source

theorem PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem {R : Type u_1} [CommRing R] {I : Ideal (PowerSeries R)} (hI : X ∈ I) :

Submodule.spanFinrank I ≤ Submodule.spanFinrank (Ideal.map constantCoeff I) + 1

source

theorem PowerSeries.eq_of_le_of_X_notMem_of_fg_of_isPrime {R : Type u_1} [CommRing R] {I : Ideal (PowerSeries R)} [I.IsPrime] {J : Ideal (PowerSeries R)} (hJI : J ≤ I) (hXI : X ∉ I) (hJ : J.FG) (h' : Ideal.map constantCoeff I ≤ Ideal.map constantCoeff J) :

I = J

source

theorem PowerSeries.exist_eq_span_eq_ncard_of_X_notMem {R : Type u_1} [CommRing R] {I : Ideal (PowerSeries R)} [I.IsPrime] (hI : X ∉ I) {S : Set R} (hSI : Ideal.span S = Ideal.map constantCoeff I) (hS : S.Finite) :

∃ (T : Set (PowerSeries R)), I = Ideal.span T ∧ T.Finite ∧ T.ncard = S.ncard

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.

source