Analytic points and the analytic locus of Spa(A, A⁺)

Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.39, Remark 7.40(2), (3), (5), Remark 7.42(2), and Proposition 7.49.

This file formalizes the analytic locus of the adic spectrum Spa(A, A⁺).

Main definitions

• TauCeti.ValuationSpectrum.IsAnalyticPoint : extends Wedhorn's analytic-point predicate from Cont A to Spv A; on continuous points it is Definition 7.39.
• TauCeti.ValuationSpectrum.spaAnalytic : Wedhorn's Spa(A, A⁺)ᵃ, the analytic locus of Spa(A, A⁺) as a Set (Spv A).
• TauCeti.ValuationSpectrum.spaAnalytic_def : the analytic locus as a set intersection.

Main results

• TauCeti.ValuationSpectrum.isAnalyticPoint_of_isTateRing : over a Tate ring every point of Spv A (and hence Spa(A, A⁺)) is analytic.
• TauCeti.ValuationSpectrum.spaAnalytic_eq_spa_of_isTateRing : Wedhorn Remark 7.40(3), for a Tate ring A, the analytic locus is the entire adic spectrum.
• TauCeti.ValuationSpectrum.isAnalyticPoint_iff_not_le_supp_of_isAdic : in an I-adic ring a point is analytic exactly when its support does not contain I.
• TauCeti.ValuationSpectrum.isOpen_val_preimage_spaAnalytic : the analytic locus is open.
• TauCeti.ValuationSpectrum.isCompact_val_preimage_spaAnalytic : Wedhorn Remark 7.40(2), the analytic locus is quasi-compact; with the previous result, open and quasi-compact.
• TauCeti.ValuationSpectrum.IsAnalyticPoint.isMicrobial : Wedhorn Remark 7.40(5), every continuous analytic point of a Huber ring is microbial.
• TauCeti.ValuationSpectrum.IsAnalyticPoint.exists_coarsenByUnits_mem_spaAnalytic : Wedhorn Remark 7.42(2), an analytic point has a height-one vertical generization in every adic spectrum containing it.
• TauCeti.ValuationSpectrum.spaAnalytic_eq_biUnion_rationalSubset : generators of an ideal of definition give a finite rational cover of the analytic locus.
• TauCeti.ValuationSpectrum.isTateRing_completion_locTopology_of_mem_generators : the completed coordinate ring of each chart in that cover is Tate.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Definition 7.39, Remark 7.40(2), (3), (5), Remark 7.42(2), and Proposition 7.49.

def TauCeti.ValuationSpectrum.IsAnalyticPoint {A : Type u_1} [CommRing A] [TopologicalSpace A] (v : ValuationSpectrum A) : Prop

Analytic points of Spv A. A point v : Spv A is analytic if its support v.supp is not an open ideal of A. This extends Wedhorn's Definition 7.39 from Cont A to all of Spv A; its restriction to continuous points is his predicate.

Equations

• v.IsAnalyticPoint = ¬IsOpen ↑v.supp

@[simp]

theorem TauCeti.ValuationSpectrum.isAnalyticPoint_def {A : Type u_1} [CommRing A] [TopologicalSpace A] (v : ValuationSpectrum A) : v.IsAnalyticPoint ↔ ¬IsOpen ↑v.supp

A point of Spv A is analytic exactly when its support is not open.

def TauCeti.ValuationSpectrum.spaAnalytic {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) : Set (ValuationSpectrum A)

Wedhorn's Analytic Locus Spa(A, A⁺)ᵃ: the subset of spa Aplus consisting of analytic points (Definition 7.39).

Equations

• TauCeti.ValuationSpectrum.spaAnalytic Aplus = TauCeti.ValuationSpectrum.spa Aplus ∩ {v : TauCeti.ValuationSpectrum A | v.IsAnalyticPoint}

theorem TauCeti.ValuationSpectrum.spaAnalytic_def {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) : spaAnalytic Aplus = spa Aplus ∩ {v : ValuationSpectrum A | v.IsAnalyticPoint}

The analytic locus as a set intersection.

@[simp]

theorem TauCeti.ValuationSpectrum.mem_spaAnalytic_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (v : ValuationSpectrum A) : v ∈ spaAnalytic Aplus ↔ v ∈ spa Aplus ∧ v.IsAnalyticPoint

Membership in the analytic locus: v ∈ Spa(A, A⁺)ᵃ iff v ∈ Spa(A, A⁺) and v is an analytic point.

theorem TauCeti.ValuationSpectrum.spaAnalytic_subset_spa {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) : spaAnalytic Aplus ⊆ spa Aplus

The analytic locus is contained in the adic spectrum.

theorem TauCeti.ValuationSpectrum.spaAnalytic_antitone {A : Type u_1} [CommRing A] [TopologicalSpace A] : Antitone spaAnalytic

Enlarging the plus ring shrinks the analytic locus.

theorem TauCeti.ValuationSpectrum.isAnalyticPoint_iff_not_le_supp_of_isAdic {A : Type u_1} [CommRing A] [TopologicalSpace A] {I : Ideal A} (hI : IsAdic I) (v : ValuationSpectrum A) : v.IsAnalyticPoint ↔ ¬I ≤ v.supp

In a ring whose topology is I-adic, a point is analytic exactly when its support does not contain I.

theorem TauCeti.ValuationSpectrum.isAnalyticPoint_iff_exists_mem_extendedIdealOfDefinition_notMem_supp {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (v : ValuationSpectrum A) : v.IsAnalyticPoint ↔ ∃ a ∈ P.extendedIdealOfDefinition, a ∉ v.supp

A point is analytic exactly when some element of the extended ideal of definition is outside its support. This is Wedhorn Proposition 7.49(2)(i), expressed using Lemma 6.6.

theorem TauCeti.ValuationSpectrum.IsAnalyticPoint.exists_mem_idealOfDefinition_notMem_supp {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) {v : ValuationSpectrum A} (hv : v.IsAnalyticPoint) : ∃ b ∈ P.idealOfDefinition, ↑b ∉ v.supp

An analytic point supplies an element of an ideal of definition which is outside its support. Unlike an arbitrary element of the extended ideal, this witness is topologically nilpotent because it comes from the ring of definition itself.

theorem TauCeti.ValuationSpectrum.IsAnalyticPoint.isMicrobial {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] {v : ValuationSpectrum A} (hana : v.IsAnalyticPoint) (hcont : v.IsContinuous) : v.valuation.IsMicrobial

Wedhorn Remark 7.40(5). Every continuous analytic point of a Huber ring is microbial.

theorem TauCeti.ValuationSpectrum.IsAnalyticPoint.exists_coarsenByUnits_mem_spaAnalytic {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] {v : ValuationSpectrum A} (hana : v.IsAnalyticPoint) (Aplus : Subring A) (hAplus : Aplus ≤ Huber.powerBoundedSubring A) (hcont : v.IsContinuous) : ∃ (H : ConvexSubgroup (↑v.valuation).ValueGroup₀ˣ), Nontrivial ((↑v.valuation).ValueGroup₀ˣ ⧸ H.toSubgroup) ∧ MulArchimedean ((↑v.valuation).ValueGroup₀ˣ ⧸ H.toSubgroup) ∧ ofValuation (v.valuation.restrict.coarsenByUnits H) ∈ spaAnalytic Aplus ∧ (ofValuation (v.valuation.restrict.coarsenByUnits H)).supp = v.supp

Wedhorn Remark 7.42(2). A continuous analytic point has a height-one vertical generization in Spa(A, A⁺) whenever A⁺ consists of power-bounded elements; in particular, this applies to every ring of integral elements.

theorem TauCeti.ValuationSpectrum.isOpen_val_preimage_spaAnalytic {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) : IsOpen (Subtype.val ⁻¹' spaAnalytic Aplus)

The analytic locus is open in the adic spectrum. It is the union, over the extended ideal of definition, of the loci on which an element does not vanish.

theorem TauCeti.ValuationSpectrum.rationalSubset_subset_spaAnalytic_of_mem_extendedIdealOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) {s : A} (hs : s ∈ P.extendedIdealOfDefinition) : rationalSubset Aplus T s ⊆ spaAnalytic Aplus

A rational subset whose denominator belongs to the extended ideal of definition consists of analytic points.

theorem TauCeti.ValuationSpectrum.spaAnalytic_eq_biUnion_rationalSubset_of_span_eq_extendedIdealOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (hspan : Ideal.span ↑T = P.extendedIdealOfDefinition) : spaAnalytic Aplus = ⋃ t ∈ T, rationalSubset Aplus T t

A finite rational cover of the analytic locus. If T generates the extended ideal of definition, then the rational subsets R(T/t), for t ∈ T, cover exactly the analytic locus. This is the cover in Wedhorn Proposition 7.49(2).

theorem TauCeti.ValuationSpectrum.spaAnalytic_eq_biUnion_rationalSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (G : Finset ↥P.ringOfDefinition) (hG : Ideal.span ↑G = P.idealOfDefinition) : spaAnalytic Aplus = ⋃ g ∈ G, rationalSubset Aplus (Finset.image Subtype.val G) ↑g

The finite standard rational cover of the analytic locus. If G generates an ideal of definition, then the rational subsets R(G/g), for g ∈ G, cover exactly the analytic locus. This is the cover in Wedhorn Proposition 7.49(2).

theorem TauCeti.ValuationSpectrum.val_preimage_rationalSubset_mem_spaRationalFamily_of_span_eq_idealOfDefinition {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (G : Finset ↥P.ringOfDefinition) (hG : Ideal.span ↑G = P.idealOfDefinition) (g : ↥P.ringOfDefinition) : Subtype.val ⁻¹' rationalSubset Aplus (Finset.image Subtype.val G) ↑g ∈ spaRationalFamily Aplus

Every set in the standard analytic cover is a member of the rational basis: its numerator ideal is the extended ideal of definition, hence open.

theorem TauCeti.ValuationSpectrum.isTateRing_completion_locTopology_of_mem_generators {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (G : Finset ↥P.ringOfDefinition) (hG : Ideal.span ↑G = P.idealOfDefinition) {g : ↥P.ringOfDefinition} (hg : g ∈ G) (S : Type u_2) [CommRing S] [Algebra A S] [IsLocalization.Away (↑g) S] : have hden := ⋯; Huber.IsTateRing (UniformSpace.Completion S)

The completed coordinate ring of a chart in the standard analytic cover is a Tate ring. The denominator belongs to the ideal of definition, hence is topologically nilpotent, and localization makes it a unit. The localization's standing hypothesis is constructed from the same generating set.

theorem TauCeti.ValuationSpectrum.isCompact_val_preimage_spaAnalytic {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) : IsCompact (Subtype.val ⁻¹' spaAnalytic Aplus)

Wedhorn Remark 7.40(2). The analytic locus is quasi-compact. A finite generating set of the extended ideal of definition gives a finite rational cover of it, and each rational subset in that cover is quasi-compact, so their union is. Together with isOpen_val_preimage_spaAnalytic this is the whole of 7.40(2): the analytic locus is an open quasi-compact subset of Spa(A, A⁺).

Stated for the preimage in spa Aplus rather than for spaAnalytic Aplus : Set (Spv A), matching isOpen_val_preimage_spaAnalytic, because quasi-compactness of a rational subset is available in that form.

theorem TauCeti.ValuationSpectrum.isAnalyticPoint_of_isTateRing {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] (v : ValuationSpectrum A) : v.IsAnalyticPoint

Over a Tate ring, every point of Spv A is analytic, extending Wedhorn Remark 7.40(3) beyond continuous points.

@[simp]

theorem TauCeti.ValuationSpectrum.spaAnalytic_eq_spa_of_isTateRing {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] (Aplus : Subring A) : spaAnalytic Aplus = spa Aplus

Wedhorn Remark 7.40(3). Over a Tate ring, the analytic locus is the entire adic spectrum: Spa (A, A⁺)ᵃ = Spa (A, A⁺).