Tate's acyclicity theorem for the standard Laurent cover of the closed unit disc

Let K be a complete nonarchimedean field. The coordinate ring K⟨T₁, …, Tₖ⟩ of the closed unit polydisc is a strongly noetherian Tate ring (Bosch–Güntzer–Remmert §5.2.6), so the augmented Čech complex of its structure presheaf, as a presheaf of abelian groups, is exact in every degree for every Laurent cover of a rational subset (quasiIso_cechAugmentation_laurentFamily, Wedhorn's Lemma 8.34(i)). The first example below records that this applies to the polydisc with no further hypotheses.

On the closed unit disc Spa(K⟨T⟩, K⟨T⟩°), the standard example is the Laurent cover generated by c⁻¹ (T - a) for a, c ∈ K with c ≠ 0. Its two pieces are the closed subdisc of radius |c| about a (TauCeti.ValuationSpectrum.closedSubdisc a c) and the region where T stays at distance at least |c| from a:

R({T - a, c} / c) = {|T - a| ≤ |c|},      R({c} / (T - a)) = {|T - a| ≥ |c|}.

This file proves that the cover of the closed unit disc by these two rational subsets is acyclic for the structure presheaf, which is Tate's acyclicity theorem for this cover. Over K = ℚ_[p] with a = 0 and c = p it is the cover of the closed p-adic unit disc by {|T| ≤ |p|} and {|T| ≥ |p|}, recorded in the second example.

Main results

• TauCeti.ValuationSpectrum.quasiIso_cechAugmentation_closedDisc_spaBasicOpen: the cover of the closed unit disc by {|T - a| ≤ |c|} and {|T - a| ≥ |c|} is acyclic for the structure presheaf.

References

• J. Tate, Rigid analytic spaces, Invent. Math. 12 (1971), 257–289, for the acyclicity of Laurent covers.
• S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis, §5.2.6 and §8.2.2.
• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Example 7.57 and Lemma 8.34.

theorem TauCeti.ValuationSpectrum.quasiIso_cechAugmentation_closedDisc_spaBasicOpen {K : Type u} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] [Huber.IsTateRing K] (P : Huber.PairOfDefinition K) [DecidableEq ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)] (a : K) {c : K} (hc : c ≠ 0) : QuasiIso (CategoryTheory.cechAugmentation ![⟨spaBasicOpen (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) {Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a, (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c} ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c), ⋯⟩, ⟨spaBasicOpen (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) {(Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c} (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a), ⋯⟩] CategoryTheory.Limits.isTerminalTop (presentationLimitAddCommGrpPresheaf (P.weighted ⋯) (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) ⊤))

Tate's acyclicity theorem for the standard Laurent cover of the closed unit disc. Let K be a complete nonarchimedean field and a, c ∈ K with c ≠ 0. The closed unit disc Spa(K⟨T⟩, K⟨T⟩°) is covered by the closed subdisc R({T - a, c} / c) = {|T - a| ≤ |c|} and by R({c} / (T - a)) = {|T - a| ≥ |c|}, the Laurent cover generated by c⁻¹ (T - a). The augmented Čech complex of the structure presheaf, as a presheaf of abelian groups, for this cover is exact in every degree.