Adic Space

Results named in Tau Ceti's TauCeti.AlgebraicGeometry.AdicSpace modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremBuzzard–Verberkmoes for the presheaf of sets#

Let A be a stably uniform Tate ring, P a pair of definition whose ring of definition lies in A⁺, and A⁺ a subring of power-bounded elements. The presheaf of sets underlying the presentation-limit structure presheaf of Spa(A, A⁺) is a sheaf on all opens. The ring need not be complete or Hausdorff.

TauCeti.ValuationSpectrum.isSheaf_underlying_presentationLimitPresheaf_of_isStablyUniform.{v}
  {A : Type v} [CommRing A] [UniformSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsTateRing A]
  [TauCeti.Huber.IsStablyUniform A] (P : TauCeti.Huber.PairOfDefinition A) {Aplus : Subring A}
  (hP : P.ringOfDefinition ≤ Aplus)
  (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → TauCeti.Huber.IsPowerBounded a) :
  CategoryTheory.Presheaf.IsSheaf
    (Opens.grothendieckTopology ↑(TauCeti.ValuationSpectrum.spa Aplus))
    ((TauCeti.ValuationSpectrum.presentationLimitPresheaf P Aplus).comp
      (TauCeti.TopCommRingCat.isCompleteSeparated.ι.comp (CategoryTheory.forget TopCommRingCat)))
Lean

Formalized in Tau Ceti as TauCeti.ValuationSpectrum.isSheaf_underlying_presentationLimitPresheaf_of_isStablyUniform.

Other forms

Buzzard–Verberkmoes: stably uniform Tate pairs are sheafy. Formalized in Tau Ceti as TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_of_isStablyUniform.

TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_of_isStablyUniform.{v} {A : Type v}
  [CommRing A] [UniformSpace A] [IsTopologicalRing A] [TauCeti.Huber.IsTateRing A]
  [TauCeti.Huber.IsStablyUniform A] (P : TauCeti.Huber.PairOfDefinition A) {Aplus : Subring A}
  (hP : P.ringOfDefinition ≤ Aplus)
  (hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → TauCeti.Huber.IsPowerBounded a) :
  CategoryTheory.Presheaf.IsSheaf
    (Opens.grothendieckTopology ↑(TauCeti.ValuationSpectrum.spa Aplus))
    (TauCeti.ValuationSpectrum.presentationLimitPresheaf P Aplus)
Sources
LeanTauCeti.ValuationSpectrum.isSheaf_underlying_presentationLimitPresheaf_of_isStablyUniform · TauCeti.ValuationSpectrum.isSheaf_presentationLimitPresheaf_of_isStablyUniform

TheoremThe remainder theorem in K⟨T⟩#

For a in the closed unit disc (power-bounded, that is ‖a‖ ≤ 1), T - a divides f - f(a) for every restricted power series f in one variable over a complete nonarchimedean field. This is the analogue of Mathlib's Polynomial.X_sub_C_dvd_sub_C_eval.

TauCeti.ValuationSpectrum.weightedX_sub_weightedC_dvd_sub_weightedC_evalAtHom.{u_1} {K : Type u_1}
  [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] (a : Fin 1 → K)
  (ha : ∀ (i : Fin 1), TauCeti.Huber.IsPowerBounded (a i))
  (f : ↥(TauCeti.Huber.weightedRestrictedSubring (fun x => {1}) ⋯)) :
  TauCeti.Huber.weightedX (fun x => {1}) ⋯ 0 - (TauCeti.Huber.weightedC (fun x => {1}) ⋯) (a 0) ∣
    f - (TauCeti.Huber.weightedC (fun x => {1}) ⋯) ((TauCeti.ValuationSpectrum.evalAtHom a ha) f)
Lean

Formalized in Tau Ceti as TauCeti.ValuationSpectrum.weightedX_sub_weightedC_dvd_sub_weightedC_evalAtHom.

Sources
LeanTauCeti.ValuationSpectrum.weightedX_sub_weightedC_dvd_sub_weightedC_evalAtHom
Uses 1 · Used by 1
Proof usesThe Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2)
Used byEvery point of the closed unit disc is of one of Wedhorn's five types

TheoremTate'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.

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

Formalized in Tau Ceti as TauCeti.ValuationSpectrum.quasiIso_cechAugmentation_closedDisc_spaBasicOpen.

Sources
LeanTauCeti.ValuationSpectrum.quasiIso_cechAugmentation_closedDisc_spaBasicOpen
Uses 4
Proof usesHenkel's open mapping theorem · Henkel's theorem in quotient form · Kedlaya's Hilbert basis theorem for restricted power series · The open mapping theorem over a Tate ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.