Adic Spaces — Lean blueprint

8. Analytic points🔗

Definition8.1
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 8.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A point v \in \mathrm{Spv}(A) is analytic if its support \ker v is not an open ideal (\texttt{IsAnalytic}) (Definition 6.1); a point is trivial if all elements outside the support are v-equivalent (\texttt{IsTrivialValuation}), and \mathrm{Spa}(A, A^{+}) is analytic when it has no trivial points (\texttt{SpaIsAnalytic}). Following Wedhorn Definition 8.35.

Lean code for Definition8.1●3 definitions
  • defdefined in «Adic spaces»/AnalyticPoints.lean
    complete
    def ValuationSpectrum.IsAnalytic.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] (v : Spv A) : Prop
    def ValuationSpectrum.IsAnalytic.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A] (v : Spv A) : Prop
    A point `v : Spv A` is *analytic* if its support `supp(v)` is not an open ideal
(Definition 8.35 of Wedhorn).
  • defdefined in «Adic spaces»/AnalyticPoints.lean
    complete
    def ValuationSpectrum.IsTrivialValuation.{u_1} {A : Type u_1} [CommRing A]
  (v : Spv A) : Prop
    def ValuationSpectrum.IsTrivialValuation.{u_1}
  {A : Type u_1} [CommRing A]
  (v : Spv A) : Prop
    A point `v : Spv A` has a **trivial valuation** if all elements outside the support are
`v`-equivalent: `v(a) ≤ v(b)` whenever `a ∉ supp(v)` and `b ∉ supp(v)`. This corresponds
to the induced valuation on `A / supp(v)` being the trivial (rank-zero) valuation.
  • defdefined in «Adic spaces»/AnalyticPoints.lean
    complete
    def ValuationSpectrum.SpaIsAnalytic.{u_2} (A : Type u_2) [CommRing A]
  [TopologicalSpace A] [ValuationSpectrum.PlusSubring A] : Prop
    def ValuationSpectrum.SpaIsAnalytic.{u_2}
  (A : Type u_2) [CommRing A]
  [TopologicalSpace A]
  [ValuationSpectrum.PlusSubring A] : Prop
    The adic spectrum `Spa(A, A⁺)` is **analytic** if it contains no trivial valuation
points. This is the condition appearing in Scottish Book Problem 10
(cf. Definition 8.35, Proposition 8.36 of Wedhorn).
Theorem8.2
Statement uses 3
Statement dependency previews
Preview
Definition 1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

If A is a Tate ring then every point of \mathrm{Spv}(A) is analytic (Definition 8.1, Definition 1.2, Definition 1.3). In Adic-Spaces: \texttt{IsTateRing.isAnalytic}. Following Wedhorn Proposition 8.36.

Lean code for Theorem8.2●1 theorem
  • theoremdefined in «Adic spaces»/AnalyticPoints.lean
    complete
    theorem ValuationSpectrum.IsTateRing.isAnalytic.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] [IsTateRing A] (v : Spv A) :
  v.IsAnalytic
    theorem ValuationSpectrum.IsTateRing.isAnalytic.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [IsTateRing A]
  (v : Spv A) : v.IsAnalytic
    **Proposition 8.36 of Wedhorn.** If `A` is a Tate ring, every point of `Spv A` is analytic.
Proof for Theorem 8.2
uses 1

Let \varpi be a pseudo-uniformiser (Definition 1.3); it is a unit, so \varpi \notin \mathrm{supp}(v) for any v. If \mathrm{supp}(v) were open it would contain a power \varpi^n of the topologically nilpotent \varpi (since powers of \varpi shrink to 0), forcing \varpi^n \in \mathrm{supp}(v), hence \varpi \in \mathrm{supp}(v) — contradicting that \varpi is a unit. So \mathrm{supp}(v) is never open and v is analytic. Following Wedhorn Proposition 8.36.

Theorem8.3
Statement uses 2
Statement dependency previews
Preview
Definition 1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

In an I-adically complete ring of definition, the defining ideal I lies in every maximal ideal of A_0 (\texttt{I\_le\_maximal\_of\_isAdicComplete}); equivalently a prime not containing I is not maximal (Definition 1.1, Definition 8.1). This is the completeness input controlling which supports can occur. Following Wedhorn §8.4 (Remark 8.4).

Lean code for Theorem8.3●2 theorems
  • theoremdefined in «Adic spaces»/AnalyticPoints.lean
    complete
    theorem PairOfDefinition.I_le_maximal_of_isAdicComplete.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] (P : PairOfDefinition A)
  [IsAdicComplete P.I ↥P.A₀] {𝔪 : Ideal ↥P.A₀} (h𝔪 : 𝔪.IsMaximal) :
  P.I ≤ 𝔪
    theorem PairOfDefinition.I_le_maximal_of_isAdicComplete.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  (P : PairOfDefinition A)
  [IsAdicComplete P.I ↥P.A₀]
  {𝔪 : Ideal ↥P.A₀} (h𝔪 : 𝔪.IsMaximal) :
  P.I ≤ 𝔪
    If `A₀` is `I`-adically complete, then `I ≤ 𝔪` for every maximal `𝔪`.
  • theoremdefined in «Adic spaces»/AnalyticPoints.lean
    complete
    theorem PairOfDefinition.not_isMaximal_of_I_not_le.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] (P : PairOfDefinition A)
  [IsAdicComplete P.I ↥P.A₀] {𝔭₀ : Ideal ↥P.A₀} (h : ¬P.I ≤ 𝔭₀) :
  ¬𝔭₀.IsMaximal
    theorem PairOfDefinition.not_isMaximal_of_I_not_le.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  (P : PairOfDefinition A)
  [IsAdicComplete P.I ↥P.A₀]
  {𝔭₀ : Ideal ↥P.A₀} (h : ¬P.I ≤ 𝔭₀) :
  ¬𝔭₀.IsMaximal
    If `A₀` is `I`-adically complete and `I ⊄ 𝔭₀`, then `𝔭₀` is not maximal.
Proof for Theorem 8.3
uses 0

If \mathfrak m is maximal but I \not\subseteq \mathfrak m, pick u \in I outside \mathfrak m; then u is a unit modulo \mathfrak m. But u \in I is topologically nilpotent, so 1 - u is a unit by I-adic completeness, and standard Jacobson-radical reasoning forces u \in \mathfrak m, a contradiction. Hence I \subseteq \mathfrak m. Following Wedhorn §8.4.