The height-one prime (p) of ℤ_[p]⟦X⟧

The ideal of ℤ_[p]⟦X⟧ generated by p is the kernel of the coefficientwise reduction ℤ_[p]⟦X⟧ → (ℤ/pℤ)⟦X⟧. Hence it is prime, and by Krull's principal ideal theorem it has height one.

Main results

• PadicInt.ker_map_toZMod: the kernel of ℤ_[p]⟦X⟧ → (ℤ/pℤ)⟦X⟧ is (p).
• PadicInt.isPrime_span_C_p: (p) is a prime ideal of ℤ_[p]⟦X⟧.
• PadicInt.height_span_C_p: (p) has height one in ℤ_[p]⟦X⟧.
• PadicInt.one_lt_height_of_C_p_mem_of_X_mem: an ideal containing p and X has height at least two.

theorem PadicInt.ker_map_toZMod {p : ℕ} [Fact (Nat.Prime p)] : RingHom.ker (PowerSeries.map toZMod) = Ideal.span {PowerSeries.C ↑p}

The kernel of the coefficientwise reduction ℤ_[p]⟦X⟧ → (ℤ/pℤ)⟦X⟧ is the ideal generated by p.

theorem PadicInt.isPrime_span_C_p {p : ℕ} [Fact (Nat.Prime p)] : (Ideal.span {PowerSeries.C ↑p}).IsPrime

The ideal of ℤ_[p]⟦X⟧ generated by p is prime.

theorem PadicInt.height_span_C_p {p : ℕ} [Fact (Nat.Prime p)] : (Ideal.span {PowerSeries.C ↑p}).height = 1

The ideal of ℤ_[p]⟦X⟧ generated by p has height one.

theorem PadicInt.one_lt_height_of_C_p_mem_of_X_mem {p : ℕ} [Fact (Nat.Prime p)] {𝔮 : Ideal (PowerSeries ℤ_[p])} (hp : PowerSeries.C ↑p ∈ 𝔮) (hX : PowerSeries.X ∈ 𝔮) : 1 < 𝔮.height

An ideal of ℤ_[p]⟦X⟧ containing both p and X has height at least two: it strictly contains the height-one prime (p), which does not contain X.