The prime elements and height-one primes of O⟦X⟧

Let O be a discrete valuation ring with uniformiser ϖ, complete for its maximal ideal 𝔪. The power series ring Λ = O⟦X⟧ is a noetherian unique factorisation domain (Mathlib's instance for power series over a principal ideal domain), so its height-one primes are exactly the ideals generated by its prime elements. Weierstrass preparation with a uniformiser power writes every nonzero series as C (ϖ ^ m) * u * P with u a unit and P a distinguished polynomial, and this determines the prime elements: up to units they are ϖ and the irreducible distinguished polynomials. Consequently the height-one primes of Λ are (ϖ) and the ideals (F) for F an irreducible distinguished polynomial. This is the list of primes over which the structure theory of finitely generated Λ-modules, and the characteristic ideal of a torsion module, are built.

The comparison between polynomials and power series runs through Mathlib's identification A[X] ⧸ (g) ≃ A⟦X⟧ ⧸ (g) for a polynomial g distinguished at an ideal I of an I-adically complete ring A: such a g is prime in A[X] exactly when it is prime in A⟦X⟧.

The distinguished generator of a height-one prime other than (ϖ) is unique, because a power series has at most one Weierstrass factorization. It is recorded as a function on the prime spectrum, PrimeSpectrum.distinguishedGenerator, equal to 1 on primes, such as (ϖ), that have no distinguished generator.

No finiteness of the residue field of O is needed.

Main definitions

• PrimeSpectrum.distinguishedGenerator 𝔭: the polynomial distinguished at the maximal ideal that generates the prime 𝔭 of O⟦X⟧, or 1 if there is none.

Main results

• Polynomial.IsDistinguishedAt.isPrime_span_coe_iff and Polynomial.IsDistinguishedAt.prime_coe_iff: a distinguished polynomial over an adically complete ring is prime as a power series if and only if it is prime as a polynomial.
• PowerSeries.prime_iff_of_isDiscreteValuationRing: the prime elements of O⟦X⟧ are the associates of C ϖ and of the irreducible distinguished polynomials.
• PowerSeries.height_eq_one_iff_of_isDiscreteValuationRing: the height-one primes of O⟦X⟧ are (ϖ) and the ideals (F) with F irreducible and distinguished.
• PrimeSpectrum.distinguishedGenerator_eq, PrimeSpectrum.span_distinguishedGenerator and PrimeSpectrum.irreducible_distinguishedGenerator: a height-one prime other than (ϖ) is generated by its distinguished generator, which is irreducible and is the only distinguished polynomial generating it.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, second edition, Chapter V, §3, on the ring O⟦T⟧ and its height-one primes.
• L. Washington, Introduction to Cyclotomic Fields, second edition, GTM 83, §13.2, on the prime ideals of ℤ_p⟦T⟧.

theorem Polynomial.IsDistinguishedAt.isPrime_span_coe_iff {A : Type u_1} [CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I) [IsAdicComplete I A] : (Ideal.span {↑g}).IsPrime ↔ (Ideal.span {g}).IsPrime

A polynomial distinguished at I, over an I-adically complete ring, generates a prime ideal of power series if and only if it generates a prime ideal of polynomials.

theorem Polynomial.IsDistinguishedAt.prime_coe_iff {A : Type u_1} [CommRing A] {g : Polynomial A} {I : Ideal A} (H : g.IsDistinguishedAt I) [IsAdicComplete I A] : Prime ↑g ↔ Prime g

A polynomial distinguished at I, over an I-adically complete ring, is a prime element of the power series ring if and only if it is a prime element of the polynomial ring.

theorem PowerSeries.prime_iff_of_isDiscreteValuationRing {O : Type u_1} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] {ϖ : O} (hϖ : Irreducible ϖ) {f : PowerSeries O} : Prime f ↔ Associated (C ϖ) f ∨ ∃ (F : Polynomial O), F.IsDistinguishedAt (IsLocalRing.maximalIdeal O) ∧ Irreducible F ∧ Associated (↑F) f

The prime elements of O⟦X⟧. Over a discrete valuation ring O with uniformiser ϖ, complete for its maximal ideal, a power series is prime if and only if it is associated to C ϖ or to an irreducible polynomial distinguished at the maximal ideal.

theorem PowerSeries.height_eq_one_iff_of_isDiscreteValuationRing {O : Type u_1} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] {ϖ : O} (hϖ : Irreducible ϖ) (𝔭 : Ideal (PowerSeries O)) [𝔭.IsPrime] : 𝔭.height = 1 ↔ 𝔭 = Ideal.span {C ϖ} ∨ ∃ (F : Polynomial O), F.IsDistinguishedAt (IsLocalRing.maximalIdeal O) ∧ Irreducible F ∧ 𝔭 = Ideal.span {↑F}

The height-one primes of O⟦X⟧. Over a discrete valuation ring O with uniformiser ϖ, complete for its maximal ideal, a prime ideal of O⟦X⟧ has height one if and only if it is generated by C ϖ or by an irreducible polynomial distinguished at the maximal ideal.

noncomputable def PrimeSpectrum.distinguishedGenerator {O : Type u_1} [CommRing O] [IsLocalRing O] (𝔭 : PrimeSpectrum (PowerSeries O)) : Polynomial O

The distinguished generator of a prime 𝔭 of O⟦X⟧, for a local ring O: a polynomial distinguished at the maximal ideal of O that generates 𝔭, if there is one, and 1 otherwise. Over a domain that is Hausdorff for its maximal ideal, such a polynomial is unique (distinguishedGenerator_eq). Over a complete discrete valuation ring with uniformiser ϖ, every height-one prime other than (ϖ) has one (span_distinguishedGenerator), while (ϖ) has none (distinguishedGenerator_eq_one_of_asIdeal_eq_span_C).

theorem PrimeSpectrum.isDistinguishedAt_distinguishedGenerator {O : Type u_1} [CommRing O] [IsLocalRing O] (𝔭 : PrimeSpectrum (PowerSeries O)) : 𝔭.distinguishedGenerator.IsDistinguishedAt (IsLocalRing.maximalIdeal O)

The distinguished generator is distinguished at the maximal ideal.

theorem PrimeSpectrum.distinguishedGenerator_eq {O : Type u_1} [CommRing O] [IsLocalRing O] [IsDomain O] [IsHausdorff (IsLocalRing.maximalIdeal O) O] {𝔭 : PrimeSpectrum (PowerSeries O)} {F : Polynomial O} (hF : F.IsDistinguishedAt (IsLocalRing.maximalIdeal O)) (h𝔭 : 𝔭.asIdeal = Ideal.span {↑F}) : 𝔭.distinguishedGenerator = F

Uniqueness of the distinguished generator. If a polynomial F distinguished at the maximal ideal generates the prime 𝔭 of O⟦X⟧, then F is the distinguished generator of 𝔭.

theorem PrimeSpectrum.distinguishedGenerator_eq_one_of_asIdeal_eq_span_C {O : Type u_1} [CommRing O] [IsLocalRing O] {𝔭 : PrimeSpectrum (PowerSeries O)} {ϖ : O} (hϖ : ϖ ∈ IsLocalRing.maximalIdeal O) (h𝔭 : 𝔭.asIdeal = Ideal.span {PowerSeries.C ϖ}) : 𝔭.distinguishedGenerator = 1

A prime generated by C ϖ with ϖ in the maximal ideal has no distinguished generator, since C ϖ divides no monic polynomial, so its distinguished generator is 1.

theorem PrimeSpectrum.span_distinguishedGenerator {O : Type u_1} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] {ϖ : O} (hϖ : Irreducible ϖ) {𝔭 : PrimeSpectrum (PowerSeries O)} (h𝔭 : 𝔭.asIdeal.height = 1) (hv : 𝔭.asIdeal ≠ Ideal.span {PowerSeries.C ϖ}) : Ideal.span {↑𝔭.distinguishedGenerator} = 𝔭.asIdeal

Over a complete discrete valuation ring with uniformiser ϖ, a height-one prime of O⟦X⟧ other than (ϖ) is generated by its distinguished generator.

theorem PrimeSpectrum.irreducible_distinguishedGenerator {O : Type u_1} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O] {ϖ : O} (hϖ : Irreducible ϖ) {𝔭 : PrimeSpectrum (PowerSeries O)} (h𝔭 : 𝔭.asIdeal.height = 1) (hv : 𝔭.asIdeal ≠ Ideal.span {PowerSeries.C ϖ}) : Irreducible 𝔭.distinguishedGenerator

Over a complete discrete valuation ring with uniformiser ϖ, the distinguished generator of a height-one prime of O⟦X⟧ other than (ϖ) is irreducible.