Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.StandardCover.Topology

Continuous gluing for standard rational covers #

On a rational open of the adic spectrum of a strongly noetherian Tate ring, the topology on sections is induced by restriction to a standard rational cover generated by units. Compatible continuous ring homomorphisms into the sections on the pieces therefore glue continuously.

The Laurent cover generated by all ratios of the generators refines the standard cover. Its restriction maps factor continuously through those of the standard cover, so the inducing property for Laurent covers implies the inducing property here. This supplies the unit-generated case of the topological reduction from Laurent covers to rational covers. No completeness or Hausdorffness assumption on the original ring is needed.

More generally, suppose the generators vanish nowhere on a rational open W. They become units in the completed coordinate ring of W. Wedhorn's Remark 8.4 identifies sections on rational subsets of W with sections over that coordinate ring as topological rings, compatibly with restriction. Transporting the unit-generated case along these isomorphisms shows that restriction to the original standard cover of W is inducing, and hence gives continuous gluing there as well.

Finally, if the generators span the unit ideal, Wedhorn's Laurent-cover reduction decomposes the standard cover into covers whose nonempty generators vanish nowhere. Continuous gluing first on those pieces and then on the Laurent cover gives continuous gluing for the original standard cover.

The general reduction from all arrows of a generated sieve to its generating arrows is provided by TauCeti.TopCommRingCat.isInducing_restrictionMap_ofArrows_iff.

References #

theorem TauCeti.ValuationSpectrum.isInducing_presentationLimitPresheafMap_standardSieve_of_isUnit {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} (hT : T.Nonempty) (hu : ∀ t ∈ T, IsUnit t) {W : TopologicalSpace.Opens ↑(spa Aplus)} (hW : W ∈ spaRationalOpens Aplus) :
have S := CategoryTheory.Sieve.ofArrows (fun (t : ↥T) => W ⊓ spaBasicOpen Aplus T ↑t) fun (x : ↥T) => CategoryTheory.homOfLE ⋯; Topology.IsInducing fun (x : ((presentationLimitPresheaf P Aplus).obj (Opposite.op W)).obj.α) (g : (V : TopologicalSpace.Opens ↑(spa Aplus)) × { f : V ⟶ W // S.arrows f }) => ↑((presentationLimitPresheaf P Aplus).map (↑g.snd).op).hom x

Sections on a rational open carry the topology induced by restriction to the sieve of a standard rational cover generated by a nonempty finite set of units.

The presentation-limit presheaf of topological commutative rings satisfies the sheaf condition for every standard rational cover of a rational open generated by units. Compatible continuous ring homomorphisms from any topological commutative ring into sections on the pieces glue to a unique continuous ring homomorphism into sections on the original open.

theorem TauCeti.ValuationSpectrum.isInducing_presentationLimitPresheafMap_standardSieve {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hP : P.ringOfDefinition ≤ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) {T : Finset A} (hT : T.Nonempty) {W : TopologicalSpace.Opens ↑(spa Aplus)} (hW : W ∈ spaRationalOpens Aplus) (hTW : ∀ t ∈ T, ∀ v ∈ W, t ∉ (↑v).supp) :
have S := CategoryTheory.Sieve.ofArrows (fun (t : ↥T) => W ⊓ spaBasicOpen Aplus T ↑t) fun (x : ↥T) => CategoryTheory.homOfLE ⋯; Topology.IsInducing fun (x : ((presentationLimitPresheaf P Aplus).obj (Opposite.op W)).obj.α) (g : (V : TopologicalSpace.Opens ↑(spa Aplus)) × { f : V ⟶ W // S.arrows f }) => ↑((presentationLimitPresheaf P Aplus).map (↑g.snd).op).hom x

Sections on a rational open carry the topology induced by restriction to a standard rational cover whose generators vanish nowhere on that open.

The presentation-limit presheaf of topological commutative rings satisfies the sheaf condition for a standard rational cover whose generators vanish nowhere on the rational open.

Standard covers generated by the unit ideal #

theorem TauCeti.ValuationSpectrum.isSheafFor_ofArrows_inf_spaBasicOpen_of_subset_laurentPiece_topCommRingCat {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] [Huber.IsStronglyNoetherian A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (hP : P.ringOfDefinition ≤ Aplus) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) {T : Finset A} (hT : T.Nonempty) {ϖ : Aˣ} (hϖ : ∀ v ∈ spa Aplus, ∃ t ∈ T, ↑ϖ <ᵥ t) {J : Set ↥T} {V : TopologicalSpace.Opens ↑(spa Aplus)} (hV : V ∈ spaRationalOpens Aplus) (hVJ : ↑V ⊆ Subtype.val ⁻¹' laurentPiece Aplus (fun (t : ↥T) => ↑ϖ⁻¹ * ↑t) J) (E : TopCommRingCat) :

Wedhorn's Lemma 8.34(ii), with topology, on a Laurent piece. The presentation-limit presheaf of topological commutative rings satisfies the sheaf condition for the restriction of a standard cover to a rational subset of a Laurent piece.

Wedhorn's Lemma 8.34(ii), with topology. The presentation-limit presheaf of topological commutative rings satisfies the sheaf condition for a standard rational cover generated by a nonempty finite set spanning the unit ideal. Thus compatible continuous ring homomorphisms into the rings of sections on the cover glue uniquely and continuously.