Sheafy and stably sheafy Huber rings

Wedhorn calls a Huber ring A sheafy when, for every ring of integral elements Â⁺ of its completion Â, the structure presheaf of Spa(Â, Â⁺) is a sheaf of topological rings, and stably sheafy when every Â-algebra topologically of finite type is sheafy. Here the sheaf condition on a pair is TauCeti.Huber.IsSheafyForEveryPresentation, which asks it of the presentation-indexed limit presheaf for every compatible pair of definition.

That presheaf is isomorphic, as a presheaf, to Wedhorn's limit over rational subsets V ↦ lim_{U ⊆ V} Â⟨U⟩ (TauCeti.ValuationSpectrum.rationalSubsetLimitPresheaf), whose coordinate rings are built from a pair of definition P. Since the sheaf condition does not depend on P, sheafiness is the sheaf condition on that presheaf for every pair of definition of Â.

The stable condition quantifies over complete Hausdorff Huber rings B, the targets for which Wedhorn states Proposition and Definition 6.29; TauCeti.Huber.IsTopologicallyFiniteType itself does not require completeness.

Main definitions

• TauCeti.Huber.IsSheafyRing: sheafy Huber rings.
• TauCeti.Huber.IsStablySheafyRing: stably sheafy Huber rings.

Main results

• TauCeti.Huber.isSheafyRing_iff_isSheaf_rationalSubsetLimitPresheaf: for any pair of definition P of Â, A is sheafy exactly when the presheaf V ↦ lim_{U ⊆ V} Â⟨U⟩ of limits over rational subsets built from P is a sheaf for every ring of integral elements of Â.
• TauCeti.Huber.IsSheafyRing.isSheafyForEveryPresentation: if A is sheafy, every ring of integral elements A⁺ of A satisfies TauCeti.Huber.IsSheafyForEveryPresentation; the intermediate step TauCeti.Huber.IsSheafyRing.isSheafyForEveryPresentation_completionPlus gives the same for Â⁺, the closure of the image of A⁺.
• TauCeti.Huber.isSheafyRing_iff_forall_isSheafyForEveryPresentation: a complete Hausdorff Huber ring B is sheafy exactly when every ring of integral elements of B satisfies TauCeti.Huber.IsSheafyForEveryPresentation.
• TauCeti.Huber.isSheafyRing_completion_iff: Â is sheafy exactly when A is.
• TauCeti.Huber.isSheafyRing_iff_of_completion_ringEquiv: sheafiness depends only on the completion, up to isomorphism of topological rings.
• TauCeti.Huber.isSheafyRing_iff_of_ringEquiv: sheafiness is invariant under isomorphisms of topological rings.
• TauCeti.Huber.isStablySheafyRing_iff_forall_isSheafyForEveryPresentation: A is stably sheafy exactly when, for every B in the definition, every ring of integral elements of B satisfies TauCeti.Huber.IsSheafyForEveryPresentation.
• TauCeti.Huber.IsStablySheafyRing.isSheafyRing: a stably sheafy Huber ring is sheafy.
• TauCeti.Huber.isStablySheafyRing_completion_iff: Â is stably sheafy exactly when A is.
• TauCeti.Huber.isStablySheafyRing_iff_of_completion_ringEquiv: stable sheafiness depends only on the completion, up to isomorphism of topological rings.
• TauCeti.Huber.isStablySheafyRing_iff_of_ringEquiv: stable sheafiness is invariant under isomorphisms of topological rings.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), §8.1, Definition 8.26, and Proposition and Definition 6.29.

def TauCeti.Huber.IsSheafyRing (A : Type u) [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] : Prop

Wedhorn Definition 8.26: a Huber ring A is sheafy when every ring of integral elements Â⁺ of its completion Â satisfies TauCeti.Huber.IsSheafyForEveryPresentation, the sheaf condition on the presentation-indexed limit presheaves of Spa(Â, Â⁺).

Equations

• TauCeti.Huber.IsSheafyRing A = ∀ (Aplus : Subring (UniformSpace.Completion A)), TauCeti.Huber.IsRingOfIntegralElements Aplus → TauCeti.Huber.IsSheafyForEveryPresentation Aplus

theorem TauCeti.Huber.isSheafyRing_iff {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] : IsSheafyRing A ↔ ∀ (Aplus : Subring (UniformSpace.Completion A)), IsRingOfIntegralElements Aplus → IsSheafyForEveryPresentation Aplus

Unfolding lemma for the sealed definition TauCeti.Huber.IsSheafyRing.

theorem TauCeti.Huber.isSheafyRing_iff_isSheaf_rationalSubsetLimitPresheaf {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] (P : PairOfDefinition (UniformSpace.Completion A)) : IsSheafyRing A ↔ ∀ (Aplus : Subring (UniformSpace.Completion A)) (hAplus : IsRingOfIntegralElements Aplus), CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(ValuationSpectrum.spa Aplus)) (ValuationSpectrum.rationalSubsetLimitPresheaf P Aplus ⋯)

Sheafiness through Wedhorn's limit over rational subsets: for any pair of definition P of Â, A is sheafy exactly when, for every ring of integral elements Â⁺ of Â, the presheaf V ↦ lim_{U ⊆ V} Â⟨U⟩ of limits over the rational subsets of Spa(Â, Â⁺), with coordinate rings built from P, is a sheaf. P need not be contained in Â⁺.

theorem TauCeti.Huber.IsSheafyRing.isSheafyForEveryPresentation_completionPlus {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] (h : IsSheafyRing A) {Aplus : Subring A} (hAplus : IsRingOfIntegralElements Aplus) : IsSheafyForEveryPresentation (ValuationSpectrum.completionPlus Aplus)

If A is sheafy and A⁺ is a ring of integral elements of A, then Â⁺, the closure of the image of A⁺ in Â, satisfies TauCeti.Huber.IsSheafyForEveryPresentation. For this Â⁺, TauCeti.ValuationSpectrum.spaCompletionHomeomorph identifies Spa(Â, Â⁺) with Spa(A, A⁺).

theorem TauCeti.Huber.IsSheafyRing.isSheafyForEveryPresentation {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] (h : IsSheafyRing A) {Aplus : Subring A} (hAplus : IsRingOfIntegralElements Aplus) : IsSheafyForEveryPresentation Aplus

If A is sheafy, every ring of integral elements A⁺ of A satisfies TauCeti.Huber.IsSheafyForEveryPresentation: the sheaf condition on Spa(Â, Â⁺) descends to Spa(A, A⁺) by completion invariance, TauCeti.Huber.isSheafyForEveryPresentation_completionPlus_iff.

theorem TauCeti.Huber.isSheafyRing_iff_forall_isSheafyForEveryPresentation {B : Type u} [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [IsTopologicalRing B] [IsHuberRing B] [CompleteSpace B] [T0Space B] : IsSheafyRing B ↔ ∀ (Bplus : Subring B), IsRingOfIntegralElements Bplus → IsSheafyForEveryPresentation Bplus

Sheafiness of a complete Hausdorff Huber ring: a complete Hausdorff Huber ring B is sheafy exactly when every ring of integral elements B⁺ of B itself satisfies TauCeti.Huber.IsSheafyForEveryPresentation. For an arbitrary Huber ring, TauCeti.Huber.IsSheafyRing.isSheafyForEveryPresentation gives the forward direction.

@[simp]

theorem TauCeti.Huber.isSheafyRing_completion_iff {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] : IsSheafyRing (UniformSpace.Completion A) ↔ IsSheafyRing A

Sheafiness is invariant under completion: the completion Â of a Huber ring A is sheafy exactly when A is.

theorem TauCeti.Huber.isSheafyRing_iff_of_completion_ringEquiv {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] {B : Type u} [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [IsTopologicalRing B] [IsHuberRing B] (e : UniformSpace.Completion A ≃+* UniformSpace.Completion B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : IsSheafyRing A ↔ IsSheafyRing B

Sheafiness depends only on the completion: if the completions Â and B̂ of Huber rings A and B are isomorphic as topological rings, then A is sheafy exactly when B is.

theorem TauCeti.Huber.isSheafyRing_iff_of_ringEquiv {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] {B : Type u} [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [IsTopologicalRing B] [IsHuberRing B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : IsSheafyRing A ↔ IsSheafyRing B

Sheafiness is invariant under isomorphism: if e : A ≃+* B is an isomorphism of topological rings between Huber rings, then A is sheafy exactly when B is. The corresponding statement for a plus ring A⁺ and its image under e is TauCeti.Huber.isSheafyForEveryPresentation_iff_of_ringEquiv.

Stably sheafy Huber rings

def TauCeti.Huber.IsStablySheafyRing (A : Type u) [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] : Prop

Wedhorn Definition 8.26: a Huber ring A with completion Â is stably sheafy when every complete Hausdorff Huber ring B topologically of finite type over Â, in the sense of Wedhorn's Proposition and Definition 6.29(i) (TauCeti.Huber.IsTopologicallyFiniteType), is sheafy (TauCeti.Huber.IsSheafyRing). The rings B range over an arbitrary universe v.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Huber.isStablySheafyRing_iff {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] : IsStablySheafyRing A ↔ ∀ (B : Type v) [inst : CommRing B] [inst_1 : UniformSpace B] [inst_2 : IsUniformAddGroup B] [inst_3 : IsTopologicalRing B] [inst_4 : IsHuberRing B] [CompleteSpace B] [T0Space B] (φ : UniformSpace.Completion A →+* B), IsTopologicallyFiniteType φ → IsSheafyRing B

Unfolding lemma for the sealed definition TauCeti.Huber.IsStablySheafyRing.

theorem TauCeti.Huber.isStablySheafyRing_iff_forall_isSheafyForEveryPresentation {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] : IsStablySheafyRing A ↔ ∀ (B : Type v) [inst : CommRing B] [inst_1 : UniformSpace B] [IsUniformAddGroup B] [inst_3 : IsTopologicalRing B] [inst_4 : IsHuberRing B] [CompleteSpace B] [T0Space B] (φ : UniformSpace.Completion A →+* B), IsTopologicallyFiniteType φ → ∀ (Bplus : Subring B), IsRingOfIntegralElements Bplus → IsSheafyForEveryPresentation Bplus

Stable sheafiness on the rings themselves: A is stably sheafy exactly when, for every complete Hausdorff Huber ring B topologically of finite type over Â, every ring of integral elements B⁺ of B satisfies TauCeti.Huber.IsSheafyForEveryPresentation.

theorem TauCeti.Huber.IsStablySheafyRing.isSheafyRing {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] (h : IsStablySheafyRing A) : IsSheafyRing A

A stably sheafy Huber ring is sheafy, since the identity of Â is topologically of finite type. This uses the stable condition for rings B in the universe of A.

theorem TauCeti.Huber.isStablySheafyRing_iff_of_completion_ringEquiv {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] {B : Type w} [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [IsTopologicalRing B] [IsHuberRing B] (e : UniformSpace.Completion A ≃+* UniformSpace.Completion B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : IsStablySheafyRing A ↔ IsStablySheafyRing B

Stable sheafiness depends only on the completion: if the completions Â and B̂ of Huber rings A and B are isomorphic as topological rings, then A is stably sheafy exactly when B is. A and B may lie in different universes; the rings topologically of finite type on the two sides lie in the same universe.

@[simp]

theorem TauCeti.Huber.isStablySheafyRing_completion_iff {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] : IsStablySheafyRing (UniformSpace.Completion A) ↔ IsStablySheafyRing A

Stable sheafiness is invariant under completion: the completion Â of a Huber ring A is stably sheafy exactly when A is.

theorem TauCeti.Huber.isStablySheafyRing_iff_of_ringEquiv {A : Type u} [CommRing A] [UniformSpace A] [IsUniformAddGroup A] [IsTopologicalRing A] [IsHuberRing A] {B : Type w} [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [IsTopologicalRing B] [IsHuberRing B] (e : A ≃+* B) (he : Continuous ⇑e) (he' : Continuous ⇑e.symm) : IsStablySheafyRing A ↔ IsStablySheafyRing B

Stable sheafiness is invariant under isomorphism: if e : A ≃+* B is an isomorphism of topological rings between Huber rings, then A is stably sheafy exactly when B is.