The Laurent cover for the presentation-limit presheaf of a uniform Tate ring

For f ∈ A the rational opens {|f| ≤ 1} and {|f| ≥ 1} cover X = Spa(A, A⁺). When A is a complete Hausdorff uniform Tate ring and A⁺ consists of power-bounded elements, a section of the presentation-limit presheaf over X is determined by its restrictions to the two pieces, and sections over the pieces that agree on their overlap glue. This transports Buzzard--Verberkmoes, Corollary 4 (isClosedEmbedding_laurentCover_of_isUniform, laurentCover_exact_of_isUniform) to presentationLimit.

Main results

• TauCeti.ValuationSpectrum.injective_presentationLimitMap_laurentCoverOpen_of_isUniform : restriction from X to the two pieces is injective.
• TauCeti.ValuationSpectrum.exists_presentationLimitMap_eq_of_laurentCoverOpen_of_isUniform : sections over the two pieces that agree on their overlap come from a section over X.

References

• K. Buzzard, A. Verberkmoes, Stably uniform affinoids are sheafy, J. reine angew. Math. 740 (2018), 25--39, Corollary 4.

theorem TauCeti.ValuationSpectrum.injective_presentationLimitMap_laurentCoverOpen_of_isUniform {A : Type v} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [Huber.IsTateRing A] [Huber.IsUniform A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (f : A) : Function.Injective fun (x : (presentationLimit Aplus ⊤).obj.α) (b : Bool) => ↑(presentationLimitMap ⋯).hom x

Buzzard--Verberkmoes Laurent injectivity for the presentation-limit presheaf. A section over Spa(A, A⁺) is determined by its restrictions to {|f| ≤ 1} and {|f| ≥ 1} when A is a complete Hausdorff uniform Tate ring.

theorem TauCeti.ValuationSpectrum.exists_presentationLimitMap_eq_of_laurentCoverOpen_of_isUniform {A : Type v} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [CompleteSpace A] [T0Space A] [Huber.IsTateRing A] [Huber.IsUniform A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (f : A) (x : (b : Bool) → (presentationLimit Aplus (laurentCoverOpen Aplus f b)).obj.α) (hx : ↑(presentationLimitMap ⋯).hom (x true) = ↑(presentationLimitMap ⋯).hom (x false)) : ∃ (a : (presentationLimit Aplus ⊤).obj.α), ∀ (b : Bool), ↑(presentationLimitMap ⋯).hom a = x b

Buzzard--Verberkmoes Laurent gluing for the presentation-limit presheaf. Compatible sections on {|f| ≤ 1} and {|f| ≥ 1} glue to a section over Spa(A, A⁺) when A is a complete Hausdorff uniform Tate ring. The gluing is unique by injective_presentationLimitMap_laurentCoverOpen_of_isUniform.