The sheaf condition for a family of opens of Spa(A, A⁺)

Let 𝒪 be the presentation-limit presheaf of Spa(A, A⁺), regarded as a presheaf of sets. This file gives two descriptions of the sheaf condition of 𝒪 for a family of opens U i ⊆ W.

• Read on the presentation limits themselves, it says that sections over the U i agreeing on the pairwise overlaps U i ⊓ U j are the restrictions of a unique section over W (isSheafFor_ofArrows_iff_existsUnique_presentationLimitMap).
• When W and the U i are rational opens inside a rational subset R(T/s), it is equivalent to the sheaf condition of the presentation-limit presheaf of B = A⟨T/s⟩ for the family of their pullbacks along j : Spa(B, A_U⁺) → Spa(A, A⁺) (isSheafFor_ofArrows_iff_locOpensComap). This is Wedhorn's Remark 8.4, presentationLimitLocIso, applied to every member of the family and to the pairwise overlaps.

The second statement reduces the sheaf condition for a cover of a rational subset to the sheaf condition for a cover of the whole adic spectrum of a complete ring, where elements that vanish nowhere on the rational subset become units. This is how Wedhorn's proof of Lemma 8.34 passes between a rational subset and its coordinate ring.

Main results

• TauCeti.ValuationSpectrum.isSheafFor_ofArrows_iff_existsUnique_presentationLimitMap : the sheaf condition for a family of opens, in terms of presentationLimitMap.
• TauCeti.ValuationSpectrum.isSheafFor_ofArrows_iff_locOpensComap : the sheaf condition for a family of rational opens inside R(T/s) is the sheaf condition for their pullbacks to the adic spectrum of A⟨T/s⟩.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Remark 8.4 and Lemma 8.34.

theorem TauCeti.ValuationSpectrum.eqToHom_apply_presentationLimitPresheaf_map_apply {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} {V W : TopologicalSpace.Opens ↑(spa Aplus)} (h : W ≤ V) (x : ((presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat))).obj (Opposite.op V)) : ↑(CategoryTheory.eqToHom ⋯).hom ((CategoryTheory.ConcreteCategory.hom (((presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat))).map (CategoryTheory.homOfLE h).op)) x) = ↑(presentationLimitMap h).hom (↑(CategoryTheory.eqToHom ⋯).hom x)

The restriction maps of the presheaf of sets are those of presentationLimit. Read through the transports along presentationLimitPresheaf_obj, restricting a section of the presentation-limit presheaf of sets from V to W ≤ V is applying presentationLimitMap.

theorem TauCeti.ValuationSpectrum.isSheafFor_ofArrows_iff_existsUnique_presentationLimitMap {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} {W : TopologicalSpace.Opens ↑(spa Aplus)} {ι : Type u_1} {U : ι → TopologicalSpace.Opens ↑(spa Aplus)} (hUW : ∀ (i : ι), U i ≤ W) : CategoryTheory.Presieve.IsSheafFor ((presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat))) (CategoryTheory.Presieve.ofArrows U fun (i : ι) => CategoryTheory.homOfLE ⋯) ↔ ∀ (x : (i : ι) → (presentationLimit Aplus (U i)).obj.α), (∀ (i j : ι), ↑(presentationLimitMap ⋯).hom (x i) = ↑(presentationLimitMap ⋯).hom (x j)) → ∃! a : (presentationLimit Aplus W).obj.α, ∀ (i : ι), ↑(presentationLimitMap ⋯).hom a = x i

The sheaf condition for a family of opens, read on presentation limits. The presentation-limit presheaf of sets satisfies the sheaf condition for a family of opens U i ≤ W exactly when every family of sections x i of presentationLimit over the U i that agree on the pairwise overlaps U i ⊓ U j is the family of restrictions of a unique section over W.

theorem TauCeti.ValuationSpectrum.isSheafFor_ofArrows_iff_locOpensComap {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (T : Finset A) (s : A) (S : Type v) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower T s S) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hT : IsOpen ↑(Ideal.span ↑T)) {W : TopologicalSpace.Opens ↑(spa Aplus)} (hW : W ∈ spaRationalOpens Aplus) (hWT : W ≤ spaBasicOpen Aplus T s) {ι : Type u_1} {U : ι → TopologicalSpace.Opens ↑(spa Aplus)} (hU : ∀ (i : ι), U i ∈ spaRationalOpens Aplus) (hUW : ∀ (i : ι), U i ≤ W) : CategoryTheory.Presieve.IsSheafFor ((presentationLimitPresheaf P Aplus).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat))) (CategoryTheory.Presieve.ofArrows U fun (i : ι) => CategoryTheory.homOfLE ⋯) ↔ CategoryTheory.Presieve.IsSheafFor ((presentationLimitPresheaf (P.completionLocalization T s S hden) (P.completedPlusSubring Aplus T s S hden)).comp (TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat))) (CategoryTheory.Presieve.ofArrows (fun (i : ι) => locOpensComap P Aplus T s S hden (U i)) fun (i : ι) => CategoryTheory.homOfLE ⋯)

The sheaf condition transported along Wedhorn's Remark 8.4. Let W ⊆ R(T/s) be rational opens of Spa(A, A⁺), where T spans an open ideal and A⁺ consists of power-bounded elements, and let U i ⊆ W be rational opens. Write j : Spa(A⟨T/s⟩, A_U⁺) → Spa(A, A⁺) for the map induced by the structure map, with pullback locOpensComap. The presentation-limit presheaf of sets of A satisfies the sheaf condition for the family U i ⊆ W exactly when the presentation-limit presheaf of sets of A⟨T/s⟩ satisfies it for the family j⁻¹(U i) ⊆ j⁻¹(W).