The Laurent sheaf condition on rational subsets of a stably uniform affinoid

Let A be a stably uniform Tate ring and let W = R(T/s) be a rational subset of Spa(A, A⁺). The coordinate ring A⟨T/s⟩ is again stably uniform, hence its separated completion is uniform. Buzzard--Verberkmoes Laurent gluing on that coordinate ring therefore transports along Wedhorn's rational-localization comparison to the two-piece Laurent cover

W ∩ {|f| ≤ 1},  W ∩ {|f| ≥ 1}

of W. Thus sections on W are determined on the two pieces and compatible sections glue. This is the local input for the induction proving that stably uniform affinoids are sheafy.

Main results

• injective_presentationLimitMap_inf_laurentCoverOpen_of_isStablyUniform: sections on a rational subset are determined on its two Laurent pieces.
• exists_presentationLimitMap_eq_of_inf_laurentCoverOpen_of_isStablyUniform: compatible sections on the two pieces glue over the rational subset.

References

• K. Buzzard, A. Verberkmoes, Stably uniform affinoids are sheafy, J. reine angew. Math. 740 (2018), 25--39, Theorem 7.
• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Remark 8.4.

theorem TauCeti.ValuationSpectrum.injective_presentationLimitMap_inf_laurentCoverOpen_of_isStablyUniform {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStablyUniform A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) {T : Finset A} {s : A} (hT : IsOpen ↑(Ideal.span ↑T)) (f : A) : Function.Injective fun (x : (presentationLimit Aplus (spaBasicOpen Aplus T s)).obj.α) (b : Bool) => ↑(presentationLimitMap ⋯).hom x

Laurent injectivity on a rational subset of a stably uniform affinoid. A section over R(T/s) is determined by its restrictions to the intersections with {|f| ≤ 1} and {|f| ≥ 1}.

theorem TauCeti.ValuationSpectrum.exists_presentationLimitMap_eq_of_inf_laurentCoverOpen_of_isStablyUniform {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStablyUniform A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) {T : Finset A} {s : A} (hT : IsOpen ↑(Ideal.span ↑T)) (f : A) (x : (b : Bool) → (presentationLimit Aplus (spaBasicOpen Aplus T s ⊓ laurentCoverOpen Aplus f b)).obj.α) (hx : ↑(presentationLimitMap ⋯).hom (x true) = ↑(presentationLimitMap ⋯).hom (x false)) : ∃ (a : (presentationLimit Aplus (spaBasicOpen Aplus T s)).obj.α), ∀ (b : Bool), ↑(presentationLimitMap ⋯).hom a = x b

Laurent gluing on a rational subset of a stably uniform affinoid. Compatible sections on R(T/s) ∩ {|f| ≤ 1} and R(T/s) ∩ {|f| ≥ 1} glue to a section on R(T/s). The gluing is unique by injective_presentationLimitMap_inf_laurentCoverOpen_of_isStablyUniform.