Adic Spaces — Lean blueprint

1. Huber rings and Tate rings🔗

Definition1.1
uses 0
Used by 7
Reverse dependency previews
Preview
Definition 1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A topological ring A is a Huber ring (or f-adic ring) if it admits a pair of definition: an open subring A_0 \subseteq A together with a finitely generated ideal I \subseteq A_0 such that the powers I^n form a neighbourhood basis of 0 in A_0. In Adic-Spaces the pair is the structure \texttt{PairOfDefinition} and the predicate is the class \texttt{IsHuberRing}. Following Wedhorn Definition 6.1.

Lean code for Definition1.1●2 definitions
  • structure(5 fields)defined in «Adic spaces»/HuberRings.lean
    complete
    structure PairOfDefinition.{u_1} (A : Type u_1) [CommRing A]
  [TopologicalSpace A] : Type u_1
    structure PairOfDefinition.{u_1} (A : Type u_1)
  [CommRing A] [TopologicalSpace A] :
  Type u_1
    A **pair of definition** `(A₀, I)` for a topological ring `A` consists of an
open subring `A₀ ⊆ A` and a finitely generated ideal `I ⊆ A₀` such that the subspace
topology on `A₀` equals the `I`-adic topology (Definition 6.1 of Wedhorn).

    Fields

    A₀ : Subring A
    The ring of definition `A₀`, an open subring of `A`. 
    I : Ideal ↥self.A₀
    The ideal of definition `I`, an ideal of `A₀`. 
    isOpen : IsOpen ↑self.A₀
    `A₀` is open in `A`. 
    fg : self.I.FG
    `I` is finitely generated. 
    isAdic : IsAdic self.I
    The subspace topology on `A₀` is the `I`-adic topology.
  • class(extends 5, 4 methods)defined in «Adic spaces»/HuberRings.lean
    complete
    class IsHuberRing.{u_1} (A : Type u_1) [CommRing A] [TopologicalSpace A] :
  Prop
    class IsHuberRing.{u_1} (A : Type u_1)
  [CommRing A] [TopologicalSpace A] : Prop
    A topological ring `A` is a **Huber ring** (or **f-adic ring**) if it admits a
pair of definition (Definition 6.1 of Wedhorn).

    Extends

    • IsTopologicalRing A

    Methods

    continuous_add : Continuous fun p ↦ p.1 + p.2
    Inherited from
    1. IsTopologicalRing
    2. IsTopologicalSemiring
    3. ContinuousAdd
    continuous_mul : Continuous fun p ↦ p.1 * p.2
    Inherited from
    1. IsTopologicalRing
    2. IsTopologicalSemiring
    3. ContinuousMul
    continuous_neg : Continuous fun a ↦ -a
    Inherited from
    1. IsTopologicalRing
    2. ContinuousNeg
    exists_pairOfDefinition : Nonempty (PairOfDefinition A)
    There exists a pair of definition.
Definition1.2
uses 1
Used by 8
Reverse dependency previews
Preview
Definition 1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A Tate ring is a Huber ring (Definition 1.1) containing a topologically nilpotent unit \varpi \in A^\times with \varpi^n \to 0 — a pseudo-uniformiser, playing the role of a uniformising parameter in non-archimedean geometry. In Adic-Spaces this is the class \texttt{IsTateRing}. Following Wedhorn Definition 6.10.

Lean code for Definition1.2●1 definition
  • class(extends 6, 5 methods)defined in «Adic spaces»/HuberRings.lean
    complete
    class IsTateRing.{u_1} (A : Type u_1) [CommRing A] [TopologicalSpace A] : Prop
    class IsTateRing.{u_1} (A : Type u_1)
  [CommRing A] [TopologicalSpace A] : Prop
    A Huber ring is a **Tate ring** if it contains a topologically nilpotent unit
(Definition 6.10 of Wedhorn).

    Extends

    • IsHuberRing A

    Methods

    continuous_add : Continuous fun p ↦ p.1 + p.2
    Inherited from
    1. IsHuberRing
    2. IsTopologicalRing
    3. IsTopologicalSemiring
    4. ContinuousAdd
    continuous_mul : Continuous fun p ↦ p.1 * p.2
    Inherited from
    1. IsHuberRing
    2. IsTopologicalRing
    3. IsTopologicalSemiring
    4. ContinuousMul
    continuous_neg : Continuous fun a ↦ -a
    Inherited from
    1. IsHuberRing
    2. IsTopologicalRing
    3. ContinuousNeg
    exists_pairOfDefinition : Nonempty (PairOfDefinition A)
    Inherited from
    1. IsHuberRing
    exists_topologicallyNilpotent_unit : ∃ u, IsTopologicallyNilpotent ↑u
    There exists a topologically nilpotent unit.
Definition1.3
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 1.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A pseudo-uniformiser of a topological ring A is a unit w \in A^\times that is topologically nilpotent, w^n \to 0. In Adic-Spaces: the predicate \texttt{IsPseudoUniformizer} and the bundled type \texttt{PseudoUniformizer}\,A. A Tate ring is precisely a Huber ring possessing one (Definition 1.2). Following Wedhorn Definition 6.10.

Lean code for Definition1.3●2 definitions
  • defdefined in «Adic spaces»/PseudoUniformizer.lean
    complete
    def IsPseudoUniformizer.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] (w : Aˣ) : Prop
    def IsPseudoUniformizer.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A]
  (w : Aˣ) : Prop
    A unit `w : Aˣ` is a **pseudo-uniformizer** if it is topologically nilpotent
(Definition 6.10 of Wedhorn).
  • defdefined in «Adic spaces»/PseudoUniformizer.lean
    complete
    def PseudoUniformizer.{u_2} (A : Type u_2) [CommRing A]
  [TopologicalSpace A] : Type u_2
    def PseudoUniformizer.{u_2} (A : Type u_2)
  [CommRing A] [TopologicalSpace A] :
  Type u_2
    The type of pseudo-uniformizers of a topological ring `A`.
Definition1.4
uses 1used by 0✓L∃∀N

For a pair of definition (A_0, I) (Definition 1.1), each ideal power I^n is open in A_0 (\texttt{pow\_isOpen}) and the ring of definition A_0 is bounded in A (\texttt{isBounded\_A}_0). These two facts say that A_0 is an open bounded subring whose I-adic filtration realises the topology — the defining data of a Huber ring. Following Wedhorn §6.

Lean code for Definition1.4●2 theorems
  • theoremdefined in «Adic spaces»/HuberRings.lean
    complete
    theorem PairOfDefinition.pow_isOpen.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A)
  (n : ℕ) : IsOpen ↑(P.I ^ n)
    theorem PairOfDefinition.pow_isOpen.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [IsTopologicalRing A]
  (P : PairOfDefinition A) (n : ℕ) :
  IsOpen ↑(P.I ^ n)
    Each power `Iⁿ` is open in `A₀` (in the subspace topology).
  • theoremdefined in «Adic spaces»/HuberRings.lean
    complete
    theorem PairOfDefinition.isBounded_A₀.{u_1} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [IsTopologicalRing A] (P : PairOfDefinition A) :
  TopologicalRing.IsBounded ↑P.A₀
    theorem PairOfDefinition.isBounded_A₀.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  [IsTopologicalRing A]
  (P : PairOfDefinition A) :
  TopologicalRing.IsBounded ↑P.A₀
    The ring of definition `A₀` is bounded (Corollary 6.4(2) of Wedhorn).
Theorem1.5
Statement uses 2
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

In a Tate ring A (Definition 1.2, Definition 1.3) the set A^{\circ\circ} of topologically nilpotent elements is open.

Lean code for Theorem1.5●1 theorem
  • theoremdefined in «Adic spaces»/HuberRings.lean
    complete
    theorem IsTateRing.isOpen_topologicalNilradical.{u_1} {A : Type u_1}
  [CommRing A] [TopologicalSpace A] [IsTateRing A]
  [IsLinearTopology A A] : IsOpen ↑(topologicalNilradical A)
    theorem IsTateRing.isOpen_topologicalNilradical.{u_1}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A] [IsTateRing A]
  [IsLinearTopology A A] :
  IsOpen ↑(topologicalNilradical A)
    In a Tate ring with linear topology, the topological nilradical `A°°` is open
(Proposition 6.13(1) of Wedhorn).
Proof for Theorem 1.5
uses 0

Let \varpi be a pseudo-uniformiser. Since \varpi^n \to 0, the sets \varpi^n A_0 (images of a ring of definition) shrink to 0, so for large n the neighbourhood \varpi^n A_0 of 0 consists of topologically nilpotent elements; as \varpi is a unit this neighbourhood translates to show A^{\circ\circ} contains an open set around each of its points. Hence A^{\circ\circ} is open. Following Wedhorn §6.