The spectrum of an open subring of a Huber ring

Let A be a Huber ring and B ⊆ A an open subring, with the subspace topology, and let f : Spec A → Spec B be the morphism induced by the inclusion. Write T ⊆ Spec B for the set of open prime ideals of B. Away from T the two spectra agree:

• T is Zariski closed: it is the zero locus of the elements of B that are topologically nilpotent in A;
• f⁻¹(T) is the set of open prime ideals of A;
• f restricts to an isomorphism of schemes from f⁻¹(Spec B ∖ T) onto Spec B ∖ T.

The complement Spec B ∖ T is covered by the basic opens D(s) for s ∈ B topologically nilpotent in A, and over D(s) the morphism f is Spec of the map B_s → A_s, which is an isomorphism because s absorbs every element of A into the open subring B (TauCeti.Localization.awayRingEquivOfIsTopologicallyNilpotent). Being an isomorphism is local on the target, so f is an isomorphism over the union of these basic opens.

No completeness, separatedness or noetherian hypothesis enters. The main case is a ring of definition B = A₀ with ideal of definition I, where Huber's sheafiness argument for rings with a noetherian ring of definition uses this comparison to pass between Spec A₀ and Spec A away from the primes containing I.

Main results

• Subring.setOf_isOpen_eq_zeroLocus: the open primes of B are the zero locus of the elements of B topologically nilpotent in A.
• Subring.isClosed_setOf_isOpen: in particular they form a Zariski closed set.
• Subring.nonOpenPrimes: the non-open primes of B, as an open subset of Spec B.
• Subring.nonOpenPrimes_eq_iSup_basicOpen: it is covered by the basic opens D(s) for s ∈ B topologically nilpotent in A.
• Subring.preimage_setOf_isOpen: the preimage in Spec A of the open primes of B is the set of open primes of A.
• Subring.isIso_morphismRestrict_nonOpenPrimes: Spec A → Spec B restricts to an isomorphism over the non-open primes of B.

References

• R. Huber, Continuous valuations, Math. Z. 212 (1993), Lemma 3.7 and its proof.
• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), §2, proof of (1.3.1)(i).
• Wedhorn, Adic Spaces, Lemma 7.44(1).

theorem Subring.setOf_isOpen_eq_zeroLocus {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A] (B : Subring A) : {q : PrimeSpectrum ↥B | IsOpen ↑q.asIdeal} = PrimeSpectrum.zeroLocus {s : ↥B | IsTopologicallyNilpotent ↑s}

The open primes of a subring of a Huber ring are a zero locus: they are the primes containing every element of the subring that is topologically nilpotent in the ambient ring.

theorem Subring.isClosed_setOf_isOpen {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A] (B : Subring A) : IsClosed {q : PrimeSpectrum ↥B | IsOpen ↑q.asIdeal}

Huber, Continuous valuations, Lemma 3.7: the open primes of a subring of a Huber ring form a Zariski closed subset of its spectrum.

def Subring.nonOpenPrimes {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A] (B : Subring A) : (AlgebraicGeometry.Spec ↧↥B).Opens

The prime ideals of a subring B of a Huber ring that are not open for the subspace topology, as an open subset of Spec B: the complement of the closed set of open primes (Subring.isClosed_setOf_isOpen).

@[simp]

theorem Subring.mem_nonOpenPrimes {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A] (B : Subring A) {q : PrimeSpectrum ↥B} : q ∈ B.nonOpenPrimes ↔ ¬IsOpen ↑q.asIdeal

A prime of B lies in Subring.nonOpenPrimes B exactly when it is not open.

theorem Subring.nonOpenPrimes_eq_iSup_basicOpen {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A] (B : Subring A) : B.nonOpenPrimes = ⨆ (s : { s : ↥B // IsTopologicallyNilpotent ↑s }), PrimeSpectrum.basicOpen ↑s

The non-open primes are covered by basic opens: the non-open primes of B are the union of the basic opens D(s) for s ∈ B topologically nilpotent in the ambient ring.

theorem Subring.preimage_setOf_isOpen {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (B : Subring A) (hB : IsOpen ↑B) : ⇑(AlgebraicGeometry.Spec.map (CommRingCat.ofHom B.subtype)) ⁻¹' {q : PrimeSpectrum ↥B | IsOpen ↑q.asIdeal} = {p : PrimeSpectrum A | IsOpen ↑p.asIdeal}

Huber, Continuous valuations, Lemma 3.7: open primes pull back to open primes. For an open subring B of a topological ring A, a prime of A is open exactly when its image in Spec B is an open prime of B.

theorem Subring.mem_preimage_nonOpenPrimes {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A] (B : Subring A) (hB : IsOpen ↑B) {p : PrimeSpectrum A} : p ∈ (TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map (CommRingCat.ofHom B.subtype)).base).obj B.nonOpenPrimes ↔ ¬IsOpen ↑p.asIdeal

The preimage of the non-open primes of an open subring B of a Huber ring A is the set of non-open primes of A: this is the source of the isomorphism Subring.isIso_morphismRestrict_nonOpenPrimes.

theorem Subring.isIso_morphismRestrict_nonOpenPrimes {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A] (B : Subring A) (hB : IsOpen ↑B) : CategoryTheory.IsIso (AlgebraicGeometry.Spec.map (CommRingCat.ofHom B.subtype) ∣_ B.nonOpenPrimes)

Huber, Continuous valuations, Lemma 3.7: away from the open primes, an open subring has the same spectrum. For an open subring B of a Huber ring A, the morphism Spec A → Spec B restricts to an isomorphism over the non-open primes of B.