The sheaf condition for Laurent covers

Let X = Spa(A, A⁺), let W be an open subset of X and let T ⊆ A be finite. The Laurent cover of W generated by T consists of the pieces

W ∩ {v | v(t) ≤ 1 for t ∈ T \ J, v(t) ≥ 1 for t ∈ J},    J ⊆ T,

and the sieve it generates is laurentSieve Aplus T W: the opens V ≤ W on which every t ∈ T has a fixed sign, that is, V ≤ {|t| ≤ 1} or V ≤ {|t| ≥ 1}. Phrasing the cover as a sieve avoids indexing its pieces by sign sets, and restricting it to an open V ≤ W gives the Laurent sieve of V (laurentSieve_pullback).

A presheaf of sets on X that satisfies the sheaf condition for the two-piece Laurent covers W ∩ {|f| ≤ 1}, W ∩ {|f| ≥ 1} of every rational subset W satisfies it for the Laurent cover of every rational subset generated by a finite set (isSheafFor_laurentSieve_of_isSheafFor). This is the induction of Wedhorn's Lemma 8.34(i), which uses TauCeti.TopologicalSpace.Opens.isSheafFor_trans.

When A is a strongly noetherian Tate ring, A⁺ consists of power-bounded elements and W is a rational subset, the presentation-limit presheaf satisfies the sheaf condition for the two-piece cover (isSheafFor_ofArrows_inf_laurentCoverOpen, Lemma 8.33), hence for the Laurent sieve (isSheafFor_laurentSieve): sections over the pieces of the Laurent cover that agree on overlaps glue uniquely to a section over W. This is the degree-zero part of Wedhorn's Lemma 8.34(i), that Laurent covers are acyclic.

The rest of Wedhorn's proof of Lemma 8.34 passes to rational localisations, so it applies to any class of Tate rings that is stable under rational localisation and satisfies Lemma 8.33 on rational subsets. LaurentGluing packages these two hypotheses on a predicate on Tate rings, and strong noetherianness satisfies them (laurentGluing_isStronglyNoetherian).

Main definitions

• TauCeti.ValuationSpectrum.LaurentGluing : the hypotheses on a predicate on Tate rings under which Wedhorn's reduction of Lemma 8.34 to Laurent covers runs.

Main results

• TauCeti.ValuationSpectrum.isSheafFor_laurentSieve_of_isSheafFor : a presheaf of sets satisfying the sheaf condition for two-piece Laurent covers of rational subsets satisfies it for every Laurent sieve of a rational subset.
• TauCeti.ValuationSpectrum.isSheafFor_ofArrows_inf_laurentCoverOpen : over a strongly noetherian Tate ring, the presentation-limit presheaf satisfies the sheaf condition for the two-piece Laurent cover of a rational subset.
• TauCeti.ValuationSpectrum.isSheafFor_laurentSieve : the presentation-limit presheaf, as a presheaf of sets, satisfies the sheaf condition for the Laurent sieve of a rational subset.
• TauCeti.ValuationSpectrum.laurentGluing_isStronglyNoetherian : strong noetherianness satisfies LaurentGluing.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 8.33 and Lemma 8.34(i).
• S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis, §8.2.2, Lemma 2, the rigid-analytic original of the induction.

The induction over the generators

theorem TauCeti.ValuationSpectrum.isSheafFor_laurentSieve_of_isSheafFor {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsHuberRing A] {Aplus : Subring A} {F : CategoryTheory.Functor (TopologicalSpace.Opens ↑(spa Aplus))ᵒᵖ (Type w)} (hF : ∀ {W : TopologicalSpace.Opens ↑(spa Aplus)}, W ∈ spaRationalOpens Aplus → ∀ (f : A), CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows (fun (b : Bool) => W ⊓ laurentCoverOpen Aplus f b) fun (x : Bool) => CategoryTheory.homOfLE ⋯)) (T : Finset A) {W : TopologicalSpace.Opens ↑(spa Aplus)} (hW : W ∈ spaRationalOpens Aplus) : CategoryTheory.Presieve.IsSheafFor F (laurentSieve Aplus T W).arrows

The induction of Wedhorn's Lemma 8.34(i). Let F be a presheaf of sets on Spa(A, A⁺) that satisfies the sheaf condition for the two-piece Laurent cover W ∩ {|f| ≤ 1}, W ∩ {|f| ≥ 1} of every rational subset W and every f ∈ A. Then F satisfies the sheaf condition for the Laurent cover of every rational subset generated by a finite set T ⊆ A.

The strongly noetherian case

theorem TauCeti.ValuationSpectrum.isSheafFor_ofArrows_inf_laurentCoverOpen {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) {W : TopologicalSpace.Opens ↑(spa Aplus)} (hW : W ∈ spaRationalOpens Aplus) (f : A) : CategoryTheory.Presieve.IsSheafFor ((presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat))) (CategoryTheory.Presieve.ofArrows (fun (b : Bool) => W ⊓ laurentCoverOpen Aplus f b) fun (x : Bool) => CategoryTheory.homOfLE ⋯)

Wedhorn's Lemma 8.33 on a rational subset, as a sheaf condition. Let A be a strongly noetherian Tate ring, A⁺ a subring of power-bounded elements, W a rational subset of Spa(A, A⁺) and f ∈ A. The presentation-limit presheaf, as a presheaf of sets, satisfies the sheaf condition for the two-piece Laurent cover W ∩ {|f| ≤ 1}, W ∩ {|f| ≥ 1} of W.

theorem TauCeti.ValuationSpectrum.isSheafFor_laurentSieve {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (T : Finset A) {W : TopologicalSpace.Opens ↑(spa Aplus)} (hW : W ∈ spaRationalOpens Aplus) : CategoryTheory.Presieve.IsSheafFor ((presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat))) (laurentSieve Aplus T W).arrows

Wedhorn's Lemma 8.34(i) in degree zero: the sheaf condition for Laurent covers. Let A be a strongly noetherian Tate ring, A⁺ a subring of power-bounded elements, W a rational subset of Spa(A, A⁺) and T ⊆ A finite. The presentation-limit presheaf, as a presheaf of sets, satisfies the sheaf condition for the Laurent cover of W generated by T: sections over the opens of laurentSieve Aplus T W that are compatible under restriction glue uniquely to a section over W. A itself need not be complete.

Predicates on Tate rings admitting Laurent gluing

structure TauCeti.ValuationSpectrum.LaurentGluing (C : (A : Type v) → [inst : CommRing A] → [inst_1 : UniformSpace A] → [inst_2 : IsTopologicalRing A] → [Huber.IsTateRing A] → Prop) : Prop

The hypotheses of Wedhorn's reduction to Laurent covers, on a predicate C on Tate rings.

• C passes from a Tate ring A to each completed rational localisation A⟨T/s⟩ for which T spans an open ideal, with the topology locUniformSpace built from a pair of definition.
• On every Tate ring A satisfying C, and for every subring A⁺ of power-bounded elements, the presentation-limit presheaf of sets of Spa(A, A⁺) satisfies the sheaf condition for the two-piece Laurent cover W ∩ {|f| ≤ 1}, W ∩ {|f| ≥ 1} of every rational subset W and every f ∈ A. This is Wedhorn's Lemma 8.33 on rational subsets, in degree zero.

For such a C, Wedhorn's proof of Lemma 8.34 shows that over a Tate ring satisfying C every cover of a rational subset by rational subsets satisfies the sheaf condition (isSheafFor_ofArrows_spaRationalOpens_of_iSup_eq_of_laurentGluing). Strong noetherianness is an example (laurentGluing_isStronglyNoetherian).

• completion_localization {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] (P : Huber.PairOfDefinition A) (T : Finset A) (s : A) (hT : IsOpen ↑(Ideal.span ↑T)) : C A → let hden := ⋯; C (UniformSpace.Completion (Localization.Away s))

  C passes to completed rational localisations.

• isSheafFor_ofArrows_inf_laurentCoverOpen {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} : C A → (∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) → ∀ {W : TopologicalSpace.Opens ↑(spa Aplus)}, W ∈ spaRationalOpens Aplus → ∀ (f : A), CategoryTheory.Presieve.IsSheafFor ((presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat))) (CategoryTheory.Presieve.ofArrows (fun (b : Bool) => W ⊓ laurentCoverOpen Aplus f b) fun (x : Bool) => CategoryTheory.homOfLE ⋯)

  Over a Tate ring satisfying C, two-piece Laurent covers of rational subsets glue.

theorem TauCeti.ValuationSpectrum.laurentGluing_isStronglyNoetherian : LaurentGluing fun (A : Type v) (x : CommRing A) (x_1 : UniformSpace A) (x_2 : IsTopologicalRing A) (x_3 : Huber.IsTateRing A) => Huber.IsStronglyNoetherian A

Strong noetherianness admits Laurent gluing. A completed rational localisation of a strongly noetherian Tate ring is strongly noetherian (TauCeti.Huber.PairOfDefinition.isStronglyNoetherian_completion), and over a strongly noetherian Tate ring two-piece Laurent covers of rational subsets glue (isSheafFor_ofArrows_inf_laurentCoverOpen).