Foundations of adic spaces

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremThe interval ring B^I is strongly noetherian#

The interval ring B^I is strongly noetherian (Kedlaya, Theorem 4.10 and Remark 4.11), for all radii ρ₁ ≤ ρ₂: each completed Huber algebra B^I⟨X₁, …, Xₙ⟩ is the Gauss-normed ring B^I{X₁, …, Xₙ} of unit-radius restricted series, which is noetherian by TauCeti.WittVector.isNoetherianRing_isRestricted_subring_intervalRing.

TauCeti.WittVector.isStronglyNoetherian_intervalRing.{u_1, u_2} (p : ℕ) [Fact (Nat.Prime p)]
  {K : Type u_1} {O : Type u_2} [Field K] [CommRing O] [Algebra O K] [CharP O p] [PerfectRing O p]
  {v : Valuation K NNReal} {ϖ : O} (hv : v.Integers O) (hϖ : ϖ ≠ 0)
  (hϖ' : v ((algebraMap O K) ϖ) < 1) {ρ₁ ρ₂ : NNReal} (hρ₁ : ρ₁ ∈ Set.Ioo 0 1)
  (hρ₂ : ρ₂ ∈ Set.Ioo 0 1) (hρ : ρ₁ ≤ ρ₂) :
  TauCeti.Huber.IsStronglyNoetherian (TauCeti.WittVector.IntervalRing p hv hϖ hϖ' hρ₁ hρ₂)
Lean

Formalized in Tau Ceti as TauCeti.WittVector.isStronglyNoetherian_intervalRing.

Sources
LeanTauCeti.WittVector.isStronglyNoetherian_intervalRing
Uses 2 · Used by 2
Proof usesKedlaya's estimate (4.9.1) in the normalisation λ_ρ(p) = ρ · Kedlaya's Hilbert basis theorem for restricted power series
Used by𝒪_𝒴 is a sheaf · The interval ring B^I is stably sheafy for all radii 0 < ρ₁ ≤ ρ₂ < 1

TheoremThe interval ring B^I is stably sheafy for all radii 0 < ρ₁ ≤ ρ₂ < 1#

every complete Hausdorff Huber ring topologically of finite type over B^I is sheafy. The ring B^I is a complete Hausdorff Tate ring that is strongly noetherian by Kedlaya's Theorem 4.10 (TauCeti.WittVector.isStronglyNoetherian_intervalRing), so this is Wedhorn's Corollary 8.35 (TauCeti.Huber.isStablySheafyRing_of_isStronglyNoetherian). In particular B^I is sheafy (TauCeti.Huber.IsStablySheafyRing.isSheafyRing).

TauCeti.WittVector.isStablySheafyRing_intervalRing.{u, w, u_1} (p : ℕ) [Fact (Nat.Prime p)]
  {O : Type u} [CommRing O] {ϖ : O} {K : Type u_1} [Field K] [Algebra O K] {v : Valuation K NNReal}
  [CharP O p] [PerfectRing O p] (hv : v.Integers O) (hϖ : ϖ ≠ 0) (hϖ' : v ((algebraMap O K) ϖ) < 1)
  {ρ₁ ρ₂ : NNReal} (hρ₁ : ρ₁ ∈ Set.Ioo 0 1) (hρ₂ : ρ₂ ∈ Set.Ioo 0 1) (hρ : ρ₁ ≤ ρ₂) :
  TauCeti.Huber.IsStablySheafyRing (TauCeti.WittVector.IntervalRing p hv hϖ hϖ' hρ₁ hρ₂)
Lean

Formalized in Tau Ceti as TauCeti.WittVector.isStablySheafyRing_intervalRing.

Sources
LeanTauCeti.WittVector.isStablySheafyRing_intervalRing
Uses 4
Proof usesHenkel's open mapping theorem · Henkel's theorem in quotient form · The interval ring B^I is strongly noetherian · The open mapping theorem over a Tate ring

Theorem𝒪_𝒴 is a sheaf#

let R be the ring of integers of a valuation v on a field K, perfect of characteristic p, and ϖ ∈ R with 0 < v(ϖ) < 1; for R = 𝒪_F this is the Fargues–Fontaine space 𝒴 ⊆ Spa(A_inf, A_inf). Then the structure presheaf 𝒪_𝒴 is a sheaf, so 𝒴 and 𝒳 = 𝒴 / φ^ℤ are adic spaces (isAdic_spaYPreAdicSpace_iff, isAdic_spaXPreAdicSpace). The window W_n = {p ^ (-n) ≤ κ ≤ p ^ n} is Spa(B^I, B^{I,+}) for I = [v(ϖ) ^ (p ^ n), v(ϖ) ^ (p ^ (-n))] (TauCeti.FarguesFontaine.windowPreAdicSpaceIso), and this pair is sheafy because B^I is strongly noetherian (Kedlaya's Theorem 4.10), so 𝒪_𝒴 is sheafy on each window (isSheafy_spaYPreAdicSpace_restrict), and hence a sheaf (isSheaf_spaYPresheaf_of_isSheafy_restrict).

TauCeti.FarguesFontaine.isSheaf_spaYPresheaf.{v, u_1} {p : ℕ} [Fact (Nat.Prime p)] {R : Type v}
  [CommRing R] [TopologicalSpace (WittVector p R)] [IsTopologicalRing (WittVector p R)] {ϖ : R}
  {P : TauCeti.Huber.PairOfDefinition (WittVector p R)}
  (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) ϖ})) [CharP R p] [PerfectRing R p]
  {K : Type u_1} [Field K] [Algebra R K] {v : Valuation K NNReal} (hv : v.Integers R) (hϖ : ϖ ≠ 0)
  (hϖ' : v ((algebraMap R K) ϖ) < 1) : (TauCeti.FarguesFontaine.spaYPresheaf P ϖ).IsSheaf
Lean

Formalized in Tau Ceti as TauCeti.FarguesFontaine.isSheaf_spaYPresheaf.

Sources
LeanTauCeti.FarguesFontaine.isSheaf_spaYPresheaf
Uses 5
Proof usesAdic spaces (Wedhorn, Definition 8.22) · Henkel's open mapping theorem · Henkel's theorem in quotient form · The interval ring B^I is strongly noetherian · The open mapping theorem over a Tate ring

TheoremThe image in 𝒳 of a wandering window is an open affinoid subspace#

Let O be the ring of integers of v, perfect of characteristic p, with pseudouniformiser ϖ, and suppose 𝒪_𝒴 is a sheaf. If 0 < q ≤ q' and the window W = {v ∈ 𝒴 : q ≤ κ(v) ≤ q'} meets none of its nontrivial integer Frobenius translates, then 𝒳 restricted to q(W) is affinoid: it is isomorphic to Spa(B^I, B^{I,+}) for the interval I = [v(ϖ) ^ (1 / q), v(ϖ) ^ (1 / q')], through the window chart spaXWindowChart.

TauCeti.FarguesFontaine.quotientMap_image_window_mem_affinoidOpens.{u, u_1} {p : ℕ}
  [Fact (Nat.Prime p)] {O : Type u} [CommRing O] {ϖ : O} {q q' : ℚ≥0} {K : Type u_1} [Field K]
  [Algebra O K] {v : Valuation K NNReal} [CharP O p] [PerfectRing O p] (hv : v.Integers O)
  (hϖ : ϖ ≠ 0) (hϖ' : v ((algebraMap O K) ϖ) < 1) [TopologicalSpace (WittVector p O)]
  [IsTopologicalRing (WittVector p O)] {hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) ϖ})}
  {P : TauCeti.Huber.PairOfDefinition (WittVector p O)}
  (hY : (TauCeti.FarguesFontaine.spaYPresheaf P ϖ).IsSheaf) (hq : q ≠ 0) (hqq' : q ≤ q')
  (hW :
    ∀ (k : ℤ),
      k ≠ 0 →
        Disjoint
          (⇑(TauCeti.FarguesFontaine.frobeniusHomeomorph hI ^ k) ⁻¹'
            Subtype.val ⁻¹'
              {v |
                v ∈ TauCeti.FarguesFontaine.spaY p ϖ ∧
                  TauCeti.FarguesFontaine.IsRadiusLowerBound p ϖ q v ∧
                    TauCeti.FarguesFontaine.IsRadiusUpperBound p ϖ q' v})
          (Subtype.val ⁻¹'
            {v |
              v ∈ TauCeti.FarguesFontaine.spaY p ϖ ∧
                TauCeti.FarguesFontaine.IsRadiusLowerBound p ϖ q v ∧
                  TauCeti.FarguesFontaine.IsRadiusUpperBound p ϖ q' v})) :
  {
      carrier :=
        TauCeti.FarguesFontaine.quotientMap hI ''
          Subtype.val ⁻¹'
            {v |
              v ∈ TauCeti.FarguesFontaine.spaY p ϖ ∧
                TauCeti.FarguesFontaine.IsRadiusLowerBound p ϖ q v ∧
                  TauCeti.FarguesFontaine.IsRadiusUpperBound p ϖ q' v},
      is_open' := ⋯ } ∈
    (TauCeti.FarguesFontaine.spaXPreAdicSpace P hI hY).affinoidOpens
Lean

Formalized in Tau Ceti as TauCeti.FarguesFontaine.quotientMap_image_window_mem_affinoidOpens.

Sources
LeanTauCeti.FarguesFontaine.quotientMap_image_window_mem_affinoidOpens

DefinitionThe adic Fargues–Fontaine curves 𝒳 = 𝒴 / φ^ℤ for two pseudouniformisers are isomorphic#

If ϖ and ϖ' define the same subset 𝒴 of Spa(𝕎 R, 𝕎 R), as they do when they generate ideals with the same radical (spaY_eq_of_radical_eq), and 𝒪_𝒴 is a sheaf, then the isomorphism spaXPreAdicSpaceCongr of pre-adic spaces is an isomorphism in the full subcategory (Adic). It is the isomorphism induced by spaYAdicSpaceCongr on the quotients by Frobenius (quotientAdicHom_comp_spaXAdicSpaceCongr_hom), and on points it is the homeomorphism spaXCongr of orbit spaces (spaXPreAdicSpaceCongr_hom_base). When R is perfect of characteristic p and is the ring of integers of a valuation v on a field, and 0 < v(ϖ) < 1, 𝒪_𝒴 is a sheaf by isSheaf_spaYPresheaf.

TauCeti.FarguesFontaine.spaXAdicSpaceCongr.{v} {p : ℕ} [Fact (Nat.Prime p)] {R : Type v}
  [CommRing R] {ϖ ϖ' : R} [TopologicalSpace (WittVector p R)] [CharP R p] [PerfectRing R p]
  [IsTopologicalRing (WittVector p R)] (P : TauCeti.Huber.PairOfDefinition (WittVector p R))
  (hI : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) ϖ}))
  (hI' : IsAdic (Ideal.span {↑p, (WittVector.teichmuller p) ϖ'}))
  (h : TauCeti.FarguesFontaine.spaY p ϖ = TauCeti.FarguesFontaine.spaY p ϖ')
  (hY : (TauCeti.FarguesFontaine.spaYPresheaf P ϖ).IsSheaf) :
  TauCeti.FarguesFontaine.spaXAdicSpace P hI hY ≅ TauCeti.FarguesFontaine.spaXAdicSpace P hI' ⋯
Lean

Formalized in Tau Ceti as TauCeti.FarguesFontaine.spaXAdicSpaceCongr.

Sources
LeanTauCeti.FarguesFontaine.spaXAdicSpaceCongr
Uses 1
Statement usesAdic spaces (Wedhorn, Definition 8.22)

TheoremEvery strongly noetherian Tate ring is sheafy#

Every strongly noetherian Tate ring is sheafy in the sense of Wedhorn's Definition 8.26 (TauCeti.Huber.IsSheafyRing). This is Wedhorn's Theorem 8.28(b); A need not be complete or Hausdorff. The identity of  is topologically of finite type, so this is the case B =  of TauCeti.Huber.isStablySheafyRing_of_isStronglyNoetherian.

TauCeti.Huber.isSheafyRing_of_isStronglyNoetherian.{v} {A : Type v} [CommRing A] [UniformSpace A]
  [IsUniformAddGroup A] [IsTopologicalRing A] [TauCeti.Huber.IsTateRing A]
  [TauCeti.Huber.IsStronglyNoetherian A] : TauCeti.Huber.IsSheafyRing A
Lean

Formalized in Tau Ceti as TauCeti.Huber.isSheafyRing_of_isStronglyNoetherian.

Sources
LeanTauCeti.Huber.isSheafyRing_of_isStronglyNoetherian
Uses 3
Proof usesHenkel's open mapping theorem · Henkel's theorem in quotient form · The open mapping theorem over a Tate ring

TheoremAffinoid algebras are the algebras topologically of finite type#

A complete ultrametric normed K-algebra B is topologically of finite type over K in Huber's sense (Wedhorn, Definition 5.57) exactly when it is a quotient of a Tate algebra K⟨X₁, …, Xₙ⟩ as a K-algebra.

TauCeti.Huber.isTopologicallyFiniteType_algebraMap_iff_isAffinoidAlgebra.{u_1, u_2} {K : Type u_1}
  [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {B : Type u_2}
  [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B] :
  TauCeti.Huber.IsTopologicallyFiniteType (algebraMap K B) ↔ TauCeti.IsAffinoidAlgebra K B
Lean

Formalized in Tau Ceti as TauCeti.Huber.isTopologicallyFiniteType_algebraMap_iff_isAffinoidAlgebra.

Sources
LeanTauCeti.Huber.isTopologicallyFiniteType_algebraMap_iff_isAffinoidAlgebra
Uses 3
Proof usesKedlaya's Hilbert basis theorem for restricted power series · The open mapping theorem over a Tate ring · TauCeti.IsAffinoidAlgebra.continuous_algHom

TheoremThe adic spectrum of a classical affinoid algebra is an affinoid adic space#

Let K be a complete nonarchimedean field with a nontrivial absolute value and B a quotient of a Tate algebra K⟨X₁, …, Xₙ⟩, carrying a complete ultrametric algebra norm, for instance the quotient Gauss norm. Then for any pair of definition P of B and any plus ring B⁺ of power-bounded elements containing its ring of definition, such as B°, Spa(B, B⁺) is an affinoid adic space.

TauCeti.ValuationSpectrum.isAdic_presentationLimitPreAdicSpace_of_isAffinoidAlgebra.{u, u_1}
  {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K] {B : Type u}
  [NormedCommRing B] [NormedAlgebra K B] [IsUltrametricDist B] [CompleteSpace B]
  (P : TauCeti.Huber.PairOfDefinition B) {Bplus : Subring B} (hB : TauCeti.IsAffinoidAlgebra K B)
  (hP : P.ringOfDefinition ≤ Bplus)
  (hBplus : ∀ ⦃b : B⦄, b ∈ Bplus → TauCeti.Huber.IsPowerBounded b) :
  (TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace P Bplus hBplus hP).isAdic
Lean

Formalized in Tau Ceti as TauCeti.ValuationSpectrum.isAdic_presentationLimitPreAdicSpace_of_isAffinoidAlgebra.

Sources
LeanTauCeti.ValuationSpectrum.isAdic_presentationLimitPreAdicSpace_of_isAffinoidAlgebra
Uses 7
Statement usesAdic spaces (Wedhorn, Definition 8.22)
Proof usesThe first isomorphism theorem for a surjective strict homomorphism of topological groups · Henkel'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 · TauCeti.IsAffinoidAlgebra.continuous_algHom

TheoremEvery point of the closed unit disc is of one of Wedhorn's five types#

Every point of the closed unit disc is of one of Wedhorn's five types, over an algebraically closed complete nonarchimedean field (Example 7.57): a classical point x_a (type (1)), a point η_{a,r} (types (2) and (3)), the point attached to a decreasing sequence of discs D(aₙ, |cₙ|) with no common point in K (type (4)), or a rank-two point η_{a,r⁺} or η_{a,r⁻} with r the norm of an element of K (type (5)).

TauCeti.ValuationSpectrum.exists_eq_classicalPoint_or_discPoint_or_discPointAbove_or_discPointBelow_or_nestedDiscPoint.{u_1}
  {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] [IsUltrametricDist K]
  [CompleteSpace K] [IsAlgClosed K] (x : ↑(TauCeti.ValuationSpectrum.closedPolydisc 1 K)) :
  (∃ y a,
      ∃ (ha : ∀ (i : Fin 1), TauCeti.Huber.IsPowerBounded (a i)),
        x = TauCeti.ValuationSpectrum.classicalPoint y a ha) ∨
    (∃ a,
        ∃ (ha : ‖a‖ ≤ 1),
          ∃ r,
            ∃ (hr₀ : 0 < r) (hr₁ : r ≤ 1), x = TauCeti.ValuationSpectrum.discPoint a ha hr₀ hr₁) ∨
      (∃ a,
          ∃ (ha : ‖a‖ ≤ 1),
            ∃ c,
              ∃ (hc₀ : 0 < ‖c‖) (hc₁ : ‖c‖ < 1),
                x = TauCeti.ValuationSpectrum.discPointAbove a ha hc₀ hc₁) ∨
        (∃ a,
            ∃ (ha : ‖a‖ ≤ 1),
              ∃ c,
                ∃ (hc₀ : 0 < ‖c‖) (hc₁ : ‖c‖ ≤ 1),
                  x = TauCeti.ValuationSpectrum.discPointBelow a ha hc₀ hc₁) ∨
          ∃ a,
            ∃ (ha : ∀ (n : ℕ), ‖a n‖ ≤ 1),
              ∃ c,
                ∃ (hc₀ : ∀ (n : ℕ), c n ≠ 0) (hc₁ : ∀ (n : ℕ), ‖c n‖ ≤ 1) (hac :
                  ∀ (n : ℕ), ‖a (n + 1) - a n‖ ≤ ‖c n‖) (hcc : ∀ (n : ℕ), ‖c (n + 1)‖ ≤ ‖c n‖),
                  (∀ (b : K), ∃ n, ‖c n‖ < ‖b - a n‖) ∧
                    x = TauCeti.ValuationSpectrum.nestedDiscPoint a ha c hc₀ hc₁ hac hcc
Lean

Formalized in Tau Ceti as TauCeti.ValuationSpectrum.exists_eq_classicalPoint_or_discPoint_or_discPointAbove_or_discPointBelow_or_nestedDiscPoint.

Sources
LeanTauCeti.ValuationSpectrum.exists_eq_classicalPoint_or_discPoint_or_discPointAbove_or_discPointBelow_or_nestedDiscPoint
Uses 3
Proof usesThe remainder theorem in K⟨T⟩ · The Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2) · Weierstrass preparation

DefinitionAdic spaces (Wedhorn, Definition 8.22)#

the objects of 𝒱, the sheafy objects of 𝒱^pre, that admit an open cover by affinoid adic spaces. Since the restriction of a sheafy object to an open is sheafy (isSheafy_restrict), an open cover by affinoid adic spaces is the same as an open cover by open affinoid subspaces: an adic space is a sheafy locally affinoid object of 𝒱^pre. Their full subcategory of 𝒱^pre is Wedhorn's category (Adic), TauCeti.AdicSpace.

TauCeti.PreAdicSpace.isAdic.{u} : CategoryTheory.ObjectProperty TauCeti.PreAdicSpace
Lean

Formalized in Tau Ceti as TauCeti.PreAdicSpace.isAdic.

Sources
LeanTauCeti.PreAdicSpace.isAdic
Used by 4
Used byClosed immersions of adic spaces are monomorphisms · 𝒪_𝒴 is a sheaf · The adic Fargues–Fontaine curves 𝒳 = 𝒴 / φ^ℤ for two pseudouniformisers are isomorphic · The adic spectrum of a classical affinoid algebra is an affinoid adic space

TheoremClosed immersions of adic spaces are monomorphisms#

a morphism into an adic space factors through a closed immersion in at most one way.

TauCeti.AdicSpace.mono_of_isClosedImmersion.{u} {X Y : TauCeti.AdicSpace} (f : X ⟶ Y)
  (hf : TauCeti.PreAdicSpace.IsClosedImmersion f.hom) : CategoryTheory.Mono f
Lean

Formalized in Tau Ceti as TauCeti.AdicSpace.mono_of_isClosedImmersion.

Sources
LeanTauCeti.AdicSpace.mono_of_isClosedImmersion
Uses 1
Statement usesAdic spaces (Wedhorn, Definition 8.22)

TheoremWedhorn Corollary 6.4(2)#

An open subring of a Huber ring, with the subspace topology, is a Huber ring.

TauCeti.Huber.IsHuberRing.subring.{u_2} {A : Type u_2} [CommRing A] [TopologicalSpace A]
  [IsTopologicalRing A] [TauCeti.Huber.IsHuberRing A] {C : Subring A} (hC : IsOpen ↑C) :
  TauCeti.Huber.IsHuberRing ↥C
Lean

Formalized in Tau Ceti as TauCeti.Huber.IsHuberRing.subring.

Sources
LeanTauCeti.Huber.IsHuberRing.subring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.