The adic spectrum is unchanged by completion

For a Huber ring A with a compatible uniform structure and any subring A⁺ ⊆ A, pullback along the completion map ι : A → Â is a homeomorphism

Spa (Â, Â⁺) ≃ₜ Spa (A, A⁺),

where Â⁺ is the closure in Â of the image of A⁺.

This is Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.48. The two halves are already available and this file only assembles them: pullback along a dense map is inducing (isInducing_spaComap_of_denseRange), and pullback along the completion map is surjective (spaComap_coeRingHom_surjective). Since spa A⁺ is T0, inducing upgrades to an embedding, and an embedding onto everything is a homeomorphism.

The statement here is more general than Wedhorn's, which is for an affinoid ring: no Huber, Hausdorff or completeness hypothesis is imposed on A⁺, and A⁺ need not be a ring of integral elements. Lemma 7.47 enters only as the justification for taking Â⁺ to be the closure of the image — when A⁺ is a ring of integral elements, so is Â⁺, by TauCeti.Huber.IsRingOfIntegralElements.completion.

Wedhorn's Proposition 7.48 also asserts that the homeomorphism matches rational subsets. That clause is proved in TauCeti.AlgebraicGeometry.AdicSpace.Spa.Completion.RationalSubset. One direction is available for any dense map, as exists_mem_spaRationalFamily_spaComap_preimage_eq_of_denseRange; the other rests on TauCeti.Huber.isOpen_map_coeRingHom, that the image of an open ideal of A generates an open ideal of Â.

Main definitions

• TauCeti.ValuationSpectrum.completionPlus: the plus ring Â⁺ of the completion, the closure of the image of A⁺. It is opaque; completionPlus_def is its characterisation.

Main results

• TauCeti.ValuationSpectrum.spaCompletionHomeomorph: the adic spectrum is unchanged by completion.
• TauCeti.ValuationSpectrum.spaCompletionHomeomorph_apply and TauCeti.ValuationSpectrum.coe_spaCompletionHomeomorph: the homeomorphism is pullback along the completion map, pointwise and as an equality of functions.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 7.48 and Lemma 7.47.

noncomputable def TauCeti.ValuationSpectrum.completionPlus {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] (Aplus : Subring A) : Subring (UniformSpace.Completion A)

The plus ring of the completion: the closure in Â of the image of A⁺. When A⁺ is a ring of integral elements so is this, by TauCeti.Huber.IsRingOfIntegralElements.completion, which is Wedhorn's Lemma 7.47.

Equations

• TauCeti.ValuationSpectrum.completionPlus Aplus = (Subring.map UniformSpace.Completion.coeRingHom Aplus).topologicalClosure

theorem TauCeti.ValuationSpectrum.completionPlus_def {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] (Aplus : Subring A) : completionPlus Aplus = (Subring.map UniformSpace.Completion.coeRingHom Aplus).topologicalClosure

completionPlus is the closure of the image of A⁺. This is the bridge to the unbundled statements, whose plus ring is spelled out — completionPlus is opaque, so unfolding goes through this lemma.

theorem TauCeti.ValuationSpectrum.map_mem_completionPlus {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] {Aplus : Subring A} {a : A} (ha : a ∈ Aplus) : UniformSpace.Completion.coeRingHom a ∈ completionPlus Aplus

The completion map carries A⁺ into Â⁺: this is the hplus argument spaComap takes along A → Â.

noncomputable def TauCeti.ValuationSpectrum.spaCompletionHomeomorph {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) : ↑(spa (completionPlus Aplus)) ≃ₜ ↑(spa Aplus)

Wedhorn Proposition 7.48. Pullback along the completion map is a homeomorphism from Spa (Â, Â⁺) onto Spa (A, A⁺), where Â⁺ is the closure of the image of A⁺.

Equations

• TauCeti.ValuationSpectrum.spaCompletionHomeomorph Aplus = ⋯.toHomeomorphOfSurjective ⋯

@[simp]

theorem TauCeti.ValuationSpectrum.spaCompletionHomeomorph_apply {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) (v : ↑(spa (completionPlus Aplus))) : (spaCompletionHomeomorph Aplus) v = spaComap UniformSpace.Completion.coeRingHom ⋯ Aplus (completionPlus Aplus) ⋯ v

The completion homeomorphism is pullback along the completion map.

@[simp]

theorem TauCeti.ValuationSpectrum.coe_spaCompletionHomeomorph {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [Huber.IsHuberRing A] (Aplus : Subring A) : ⇑(spaCompletionHomeomorph Aplus) = spaComap UniformSpace.Completion.coeRingHom ⋯ Aplus (completionPlus Aplus) ⋯

The completion homeomorphism, as a function, is pullback along the completion map. This is the functional companion of the pointwise spaCompletionHomeomorph_apply, in the form that rewrites under Set.preimage and Set.image.