Adic homomorphisms and the analytic locus

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 7.46(2).

Let φ : A → B be a continuous homomorphism of Huber rings carrying A⁺ into B⁺, and write f = Spa(φ) : Spa(B, B⁺) → Spa(A, A⁺), which on points is ValuationSpectrum.comap φ. Wedhorn's Lemma 7.46 states that

1. f maps non-analytic points to non-analytic points, and if φ is adic it also maps analytic points to analytic points;
2. if B is complete and f maps analytic points to analytic points, then φ is adic.

Part (1) is in TauCeti/AlgebraicGeometry/AdicSpace/Spa/Analytic.lean; this file proves part (2). So over a complete target, adicness of φ is detected on the adic spectrum. This is the affinoid input to the notion of an adic morphism of adic spaces, which asks exactly that analytic points go to analytic points.

Part (2) rests on a description of the open ideals of a complete Huber pair by its analytic points: an ideal 𝔞 is open exactly when no analytic point of Spa(B, B⁺) has its support containing 𝔞.

Main results

• TauCeti.ValuationSpectrum.isOpen_iff_forall_mem_spaAnalytic_not_le_supp : over a complete Huber ring, an ideal is open exactly when it lies in the support of no analytic point.
• TauCeti.ValuationSpectrum.isAdicHom_iff_forall_isAnalyticPoint_comap : Lemma 7.46, over a complete target a continuous homomorphism is adic exactly when pullback preserves analytic points of Spa(B, B⁺).
• TauCeti.ValuationSpectrum.isAdicHom_of_mapsTo_spaAnalytic : Lemma 7.46(2), in the form f(Spa(B, B⁺)ᵃ) ⊆ Spa(A, A⁺)ᵃ.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemmas 7.45 and 7.46.
• R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), Proposition 3.2.

Provenance

Developed here; no external formalization is followed. Wedhorn derives Lemma 7.46(2) from his Lemma 7.45; the openness criterion here instead reuses the coarsening construction behind Proposition 7.18(1) in TauCeti/RingTheory/Huber/Continuous/ValuativeCriterion.lean.

theorem TauCeti.ValuationSpectrum.isOpen_iff_forall_mem_spaAnalytic_not_le_supp {B : Type u_1} [CommRing B] [UniformSpace B] [T2Space B] [CompleteSpace B] [IsTopologicalRing B] [IsUniformAddGroup B] [Huber.IsHuberRing B] {Bplus : Subring B} (hle : Bplus ≤ Huber.powerBoundedSubring B) (𝔞 : Ideal B) : IsOpen ↑𝔞 ↔ ∀ v ∈ spaAnalytic Bplus, ¬𝔞 ≤ v.supp

Open ideals of a complete Huber pair, by analytic points. Let B be a complete Huber ring and B⁺ ⊆ B° a subring. An ideal 𝔞 of B is open exactly when no analytic point of Spa(B, B⁺) has support containing 𝔞.

theorem TauCeti.ValuationSpectrum.isAdicHom_iff_forall_isAnalyticPoint_comap {B : Type u_1} [CommRing B] [UniformSpace B] [T2Space B] [CompleteSpace B] [IsTopologicalRing B] [IsUniformAddGroup B] [Huber.IsHuberRing B] {A : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] {φ : A →+* B} (hφ : Continuous ⇑φ) {Bplus : Subring B} (hle : Bplus ≤ Huber.powerBoundedSubring B) : Huber.IsAdicHom φ ↔ ∀ v ∈ spaAnalytic Bplus, (comap φ v).IsAnalyticPoint

Wedhorn Lemma 7.46. Let φ : A → B be a continuous homomorphism of Huber rings with B complete, and B⁺ ⊆ B° a subring. Then φ is adic exactly when the pullback of every analytic point of Spa(B, B⁺) is analytic.

No plus ring of A enters: whether a pulled-back point is analytic does not depend on one.

theorem TauCeti.ValuationSpectrum.isAdicHom_of_mapsTo_spaAnalytic {B : Type u_1} [CommRing B] [UniformSpace B] [T2Space B] [CompleteSpace B] [IsTopologicalRing B] [IsUniformAddGroup B] [Huber.IsHuberRing B] {A : Type u_2} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] {φ : A →+* B} (hφ : Continuous ⇑φ) {Aplus : Subring A} {Bplus : Subring B} (hle : Bplus ≤ Huber.powerBoundedSubring B) (h : Set.MapsTo (comap φ) (spaAnalytic Bplus) (spaAnalytic Aplus)) : Huber.IsAdicHom φ

Wedhorn Lemma 7.46(2). Let φ : A → B be a continuous homomorphism of Huber rings with B complete, and B⁺ ⊆ B° a subring. If Spa(φ) maps the analytic points of Spa(B, B⁺) to analytic points of Spa(A, A⁺), then φ is adic.