The spectrum of a power series ring

The constant coefficient homomorphism R⟦X⟧ → R, that is X ↦ 0, embeds Spec R into Spec R⟦X⟧ as the closed subscheme X = 0. Every open subscheme of Spec R⟦X⟧ containing it is all of Spec R⟦X⟧, since X lies in the Jacobson radical of the X-adically complete ring R⟦X⟧.

Main results

• PowerSeries.range_SpecMap_constantCoeff_subset_iff_eq_top: an open subscheme of Spec R⟦X⟧ contains the image of Spec R under Spec of X ↦ 0 exactly when it is the whole scheme.

theorem PowerSeries.range_SpecMap_constantCoeff_subset_iff_eq_top {R : Type u} [CommRing R] {U : (AlgebraicGeometry.Spec ↧(PowerSeries R)).Opens} : Set.range ⇑(AlgebraicGeometry.Spec.map (CommRingCat.ofHom constantCoeff)) ⊆ ↑U ↔ U = ⊤

An open subscheme of Spec R⟦X⟧ contains the image of Spec R under Spec of the constant coefficient R⟦X⟧ → R, the locus X = 0, exactly when it is the whole scheme.