The prime spectrum of a power series ring

The power series ring R⟦X⟧ over a commutative ring R is X-adically complete, so X lies in its Jacobson radical. The zero locus V(X) is the image of Spec R under the closed embedding induced by the constant coefficient homomorphism R⟦X⟧ → R, that is, by X ↦ 0. So an open subset of Spec R⟦X⟧ containing the image of Spec R is all of Spec R⟦X⟧ (PrimeSpectrum.zeroLocus_subset_iff_eq_top_of_le_jacobson_bot).

Main results

• PowerSeries.range_comap_constantCoeff_subset_iff_eq_top: an open subset of Spec R⟦X⟧ contains the image of Spec R under the map induced by X ↦ 0 exactly when it is the whole spectrum.

theorem PowerSeries.range_comap_constantCoeff_subset_iff_eq_top {R : Type u_1} [CommRing R] {U : TopologicalSpace.Opens (PrimeSpectrum (PowerSeries R))} : Set.range (PrimeSpectrum.comap constantCoeff) ⊆ ↑U ↔ U = ⊤

An open subset of the prime spectrum of the power series ring R⟦X⟧ contains the image of the prime spectrum of R under the map induced by X ↦ 0 exactly when it is the whole spectrum.