Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.SheafForEveryPresentation

Sheafhood across compatible presentations #

IsSheafyForEveryPresentation Aplus requires Aplus to be a ring of integral elements and the presentation-indexed limit presheaf presentationLimitPresheaf P Aplus to be a sheaf of complete separated topological rings for every pair of definition P contained in Aplus. Such a pair exists because Aplus is open. The universal condition is nevertheless equivalent to sheafhood for any single pair of definition, compatible or not (isSheafyForEveryPresentation_iff_isRingOfIntegralElements_and_isSheaf).

On rational opens, presentationLimitRationalIso identifies the presheaf's values with the completed rational localizations, and presentationLimitRationalIso_inv_comp_map_comp_hom identifies its restrictions with the canonical comparison maps. On all opens, when A⁺ consists of power-bounded elements, TauCeti.ValuationSpectrum.presentationLimitPresheafIsoRationalSubsetLimitPresheaf identifies the presentation-indexed presheaf of P with Wedhorn's presheaf V ↦ lim_{U ⊆ V} A⟨U⟩ of limits over rational subsets, whose coordinate rings are those of presentations over the same P, and isSheaf_presentationLimitPresheaf_iff_isSheaf_rationalSubsetLimitPresheaf transfers sheafhood along it.

Main results #

The sheaf-level comparisons behind these are in TauCeti.AlgebraicGeometry.AdicSpace.Spa.StructurePresheaf.Transport.

References #

source
structure TauCeti.Huber.IsSheafyForEveryPresentation {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] (Aplus : Subring A) :
Prop

The plus ring Aplus is a ring of integral elements, and its presentation-indexed limit presheaf is a sheaf for every compatible pair of definition. When A⁺ consists of power-bounded elements, that presheaf is isomorphic to the presheaf of limits over rational subsets built from the same pair of definition (TauCeti.ValuationSpectrum.presentationLimitPresheafIsoRationalSubsetLimitPresheaf), so this is equivalently the sheaf condition on Wedhorn's presheaf.

Instances For
    source
    theorem TauCeti.Huber.IsSheafyForEveryPresentation.exists_compatible_isSheaf {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {Aplus : Subring A} (h : IsSheafyForEveryPresentation Aplus) :
    ∃ (P : PairOfDefinition A), P.ringOfDefinition ≤ Aplus ∧ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(ValuationSpectrum.spa Aplus)) (ValuationSpectrum.presentationLimitPresheaf P Aplus)

    The universal condition supplies a compatible pair of definition whose presentation-indexed limit presheaf is a sheaf.

    Invariance under isomorphism and completion #

    source
    theorem TauCeti.Huber.isSheafyForEveryPresentation_iff_isRingOfIntegralElements_and_isSheaf {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {Aplus : Subring A} (P : PairOfDefinition A) :
    IsSheafyForEveryPresentation Aplus ↔ IsRingOfIntegralElements Aplus ∧ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(ValuationSpectrum.spa Aplus)) (ValuationSpectrum.presentationLimitPresheaf P Aplus)

    IsSheafyForEveryPresentation is the sheaf condition for any one pair of definition: the presentation-limit presheaves of all pairs of definition of A are sheaves together, so the universal condition reduces to a single pair, which need not be compatible with A⁺.

    source
    theorem TauCeti.Huber.IsSheafyForEveryPresentation.map {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {B : Type v} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {Aplus : Subring A} (h : IsSheafyForEveryPresentation Aplus) (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) :
    IsSheafyForEveryPresentation (Subring.map (↑e) Aplus)

    IsSheafyForEveryPresentation is carried along an isomorphism of topological rings.

    source
    theorem TauCeti.Huber.isSheafyForEveryPresentation_iff_of_ringEquiv {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {B : Type v} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] {Aplus : Subring A} (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) {Bplus : Subring B} (hplus : Subring.map (↑e) Aplus = Bplus) :
    IsSheafyForEveryPresentation Aplus ↔ IsSheafyForEveryPresentation Bplus

    IsSheafyForEveryPresentation is invariant under isomorphism of Huber pairs: if e : A ≃+* B is an isomorphism of topological rings carrying A⁺ onto B⁺, then A⁺ satisfies IsSheafyForEveryPresentation exactly when B⁺ does.

    source
    theorem TauCeti.Huber.forall_isSheafyForEveryPresentation_iff_of_ringEquiv {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [IsHuberRing A] {B : Type v} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B] [IsHuberRing B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) :
    (∀ (Aplus : Subring A), IsRingOfIntegralElements Aplus → IsSheafyForEveryPresentation Aplus) ↔ ∀ (Bplus : Subring B), IsRingOfIntegralElements Bplus → IsSheafyForEveryPresentation Bplus

    The sheaf condition for every plus ring is invariant under isomorphism: along an isomorphism of topological rings e : A ≃+* B, every ring of integral elements of A satisfies IsSheafyForEveryPresentation exactly when every ring of integral elements of B does.

    source
    theorem TauCeti.Huber.isSheafyForEveryPresentation_completionPlus_iff {A : Type u_1} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] {Aplus : Subring A} (hA : IsRingOfIntegralElements Aplus) :
    IsSheafyForEveryPresentation (ValuationSpectrum.completionPlus Aplus) ↔ IsSheafyForEveryPresentation Aplus

    IsSheafyForEveryPresentation is invariant under completion: for a ring of integral elements A⁺ of A, the closure Â⁺ of its image in the completion  satisfies IsSheafyForEveryPresentation exactly when A⁺ does.