The structure presheaf on the opens of a fixed open, as a presheaf of abelian groups

Let W be an open subset of X = Spa(A, A⁺). The opens of X contained in W form the meet-semilattice Set.Iic W, whose greatest element is W; in the corresponding category W is a terminal object and binary products are meets. Covers of W are therefore families in Set.Iic W, and their Čech complexes (CategoryTheory.cechComplexFunctor, with the augmentation TauCeti.CategoryTheory.cechAugmentation) are defined for presheaves on Set.Iic W with values in an abelian category. This file provides the presheaf to which they are applied: the presentation-limit presheaf, restricted to Set.Iic W and regarded as a presheaf of abelian groups.

For an open Y ≤ W, the restriction of a cover U of W to Y is computed by the presheaf V ↦ 𝒪(Y ∩ V) on the opens contained in W. This presheaf is pulled back from the opens contained in Y along V ↦ Y ∩ V, so the restriction of U to Y is acyclic exactly when the cover Y ∩ U of Y is (quasiIso_cechAugmentation_prod_iff).

For an open W contained in a rational subset R(T/s), the opens contained in W correspond, under the open embedding j : Spa(A⟨T/s⟩, A_U⁺) → Spa(A, A⁺), to the opens contained in j⁻¹(W), and Wedhorn's Remark 8.4 (presentationLimitPresheafLocIso) identifies the structure presheaves. So a cover of W is acyclic exactly when its pullback along j, a cover of j⁻¹(W), is (quasiIso_cechAugmentation_iff_locOpensComap). Taking W = R(T/s) itself, elements vanishing nowhere on R(T/s) become units of A⟨T/s⟩, so this is how acyclicity statements about covers generated by units pass to covers of rational subsets.

Main definitions

• TauCeti.ValuationSpectrum.presentationLimitAddCommGrpPresheaf: the presentation-limit presheaf on the opens contained in W, as a presheaf of abelian groups.
• TauCeti.ValuationSpectrum.presentationLimitAddCommGrpPresheafObjEquiv: its sections over V are the additive group of presentationLimit Aplus V; under this identification its restriction maps are the presentationLimitMaps (TauCeti.ValuationSpectrum.presentationLimitAddCommGrpPresheafObjEquiv_map_apply).

Main results

• TauCeti.ValuationSpectrum.quasiIso_cechAugmentation_prod_iff: the restriction to Y ≤ W of a family of opens contained in W is acyclic for the structure presheaf if and only if its intersection with Y, as a cover of Y, is.
• TauCeti.ValuationSpectrum.quasiIso_cechAugmentation_iff_locOpensComap: a family of opens contained in an open W ⊆ R(T/s) is acyclic for the structure presheaf of Spa(A, A⁺) if and only if its pullback to Spa(A⟨T/s⟩, A_U⁺) is acyclic for the structure presheaf there.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Remark 8.4 and Lemma 8.34.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitAddCommGrpPresheaf {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (W : TopologicalSpace.Opens ↑(spa Aplus)) : CategoryTheory.Functor (↑(Set.Iic W))ᵒᵖ AddCommGrpCat

The presentation-limit presheaf restricted to the opens contained in W, as a presheaf of abelian groups: its value at V ≤ W is the additive group of presentationLimit Aplus V and its restriction maps are the presentationLimitMaps, as for presentationLimitPresheaf. Its Čech complexes for families in Set.Iic W are those of covers of W.

theorem TauCeti.ValuationSpectrum.presentationLimitAddCommGrpPresheaf_obj {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) (W : TopologicalSpace.Opens ↑(spa Aplus)) (V : (↑(Set.Iic W))ᵒᵖ) : (presentationLimitAddCommGrpPresheaf P Aplus W).obj V = ↧(presentationLimit Aplus ↑(Opposite.unop V)).obj.α

The sections of presentationLimitAddCommGrpPresheaf over V are the additive group of presentationLimit Aplus V.

noncomputable def TauCeti.ValuationSpectrum.presentationLimitAddCommGrpPresheafObjEquiv {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) {W : TopologicalSpace.Opens ↑(spa Aplus)} (V : ↑(Set.Iic W)) : ↑((presentationLimitAddCommGrpPresheaf P Aplus W).obj (Opposite.op V)) ≃+ (presentationLimit Aplus ↑V).obj.α

The sections of presentationLimitAddCommGrpPresheaf over V, identified with the additive group of presentationLimit Aplus V.

@[simp]

theorem TauCeti.ValuationSpectrum.presentationLimitAddCommGrpPresheafObjEquiv_map_apply {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) (Aplus : Subring A) {W : TopologicalSpace.Opens ↑(spa Aplus)} {V V' : ↑(Set.Iic W)} (h : V' ⟶ V) (x : ↑((presentationLimitAddCommGrpPresheaf P Aplus W).obj (Opposite.op V))) : (presentationLimitAddCommGrpPresheafObjEquiv P Aplus V') ((CategoryTheory.ConcreteCategory.hom ((presentationLimitAddCommGrpPresheaf P Aplus W).map h.op)) x) = ↑(presentationLimitMap ⋯).hom ((presentationLimitAddCommGrpPresheafObjEquiv P Aplus V) x)

Under presentationLimitAddCommGrpPresheafObjEquiv, the restriction maps of presentationLimitAddCommGrpPresheaf are the presentationLimitMaps.

Restriction to a smaller open

theorem TauCeti.ValuationSpectrum.quasiIso_cechAugmentation_prod_iff {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} {W : TopologicalSpace.Opens ↑(spa Aplus)} [CategoryTheory.Limits.HasProducts AddCommGrpCat] (Y : ↑(Set.Iic W)) {ι : Type w} (U : ι → ↑(Set.Iic W)) : QuasiIso (CategoryTheory.cechAugmentation U CategoryTheory.Limits.isTerminalTop ((CategoryTheory.Limits.prod.functor.obj Y).op.comp (presentationLimitAddCommGrpPresheaf P Aplus W))) ↔ QuasiIso (CategoryTheory.cechAugmentation (fun (i : ι) => ⟨↑Y ⊓ ↑(U i), ⋯⟩) CategoryTheory.Limits.isTerminalTop (presentationLimitAddCommGrpPresheaf P Aplus ↑Y))

Restricting a cover to a smaller open. Let Y ≤ W be opens of Spa(A, A⁺) and let U be a family of opens contained in W. The augmented Čech complex of the structure presheaf restricted to Y, the presheaf V ↦ 𝒪(Y ∩ V) on the opens contained in W, for U is exact if and only if the augmented Čech complex of the structure presheaf on the opens contained in Y for the family Y ∩ U i is.

Transport along a rational localisation

theorem TauCeti.ValuationSpectrum.quasiIso_cechAugmentation_iff_locOpensComap {A : Type v} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] (P : Huber.PairOfDefinition A) {Aplus : Subring A} (T : Finset A) (s : A) (S : Type v) [CommRing S] [Algebra A S] [IsLocalization.Away s S] (hden : P.HasDenominatorPower (↑T) s S) (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a) (hP : P.ringOfDefinition ≤ Aplus) (hT : IsOpen ↑(Ideal.span ↑T)) [CategoryTheory.Limits.HasProducts AddCommGrpCat] {W : TopologicalSpace.Opens ↑(spa Aplus)} (hWT : W ≤ spaBasicOpen Aplus T s) {ι : Type w} (U : ι → ↑(Set.Iic W)) : QuasiIso (CategoryTheory.cechAugmentation U CategoryTheory.Limits.isTerminalTop (presentationLimitAddCommGrpPresheaf P Aplus W)) ↔ QuasiIso (CategoryTheory.cechAugmentation (fun (i : ι) => ⟨locOpensComap P Aplus T s S hden ↑(U i), ⋯⟩) CategoryTheory.Limits.isTerminalTop (presentationLimitAddCommGrpPresheaf (P.completionLocalization (↑T) s S hden) (P.completedPlusSubring Aplus T s S hden) (locOpensComap P Aplus T s S hden W)))

Acyclicity transported along a rational localisation. Let W be an open of Spa(A, A⁺) contained in the rational subset R(T/s), where T spans an open ideal and A⁺ consists of power-bounded elements and contains the ring of definition, and let j : Spa(A⟨T/s⟩, A_U⁺) → Spa(A, A⁺) be the open embedding induced by the structure map, with pullback locOpensComap. For a family U of opens contained in W, the augmented Čech complex of the structure presheaf of Spa(A, A⁺) for U is exact if and only if the augmented Čech complex of the structure presheaf of Spa(A⟨T/s⟩, A_U⁺) for the family j⁻¹(U i) of opens contained in j⁻¹(W) is.