The gauge of a Tate ring

Let A be a commutative ring, A₀ a subring and ϖ a unit of A. For a real base a > 1 the Tate gauge is tateGauge A₀ ϖ a x = inf { a ^ (-n) | n ∈ ℤ, ϖ ^ (-n) * x ∈ A₀ }, so x has gauge at most a ^ (-n) when it lies in ϖ ^ n A₀. Multiplication by ϖ ^ k scales the gauge exactly by a ^ (-k), and changing the base a > 1 to b > 1 raises it to the power log b / log a. When ϖ ∈ A₀, every element of A is moved into A₀ by some power of ϖ (that is, A = A₀[1/ϖ]) and a > 1, the gauge is an ultrametric ring seminorm whose closed ball of radius a ^ (-n) is exactly ϖ ^ n A₀.

When moreover A is a topological ring in which the sets ϖ ^ n A₀, n ≥ 0, form a neighbourhood basis of zero, as for a ring of definition of a Tate ring and a pseudo-uniformiser in it, the gauge recovers the topology: its open balls about zero form a neighbourhood basis of zero. Its zero set is the closure of zero, so it separates points exactly when A is Hausdorff, and it takes the value one at one when A is moreover nonzero. Two subrings with this property give gauges bounded by constant multiples of each other.

This is how a Tate ring is given a norm. The gauge is explicit data attached to the choice of the subring A₀, the unit ϖ ∈ A₀ and the base a, and its exact ϖ-scaling makes ϖ a multiplicative pseudo-uniformiser for it; a topologically nilpotent unit need not scale an arbitrary compatible norm in this way.

Main definitions

• TauCeti.Huber.tateGauge A₀ ϖ a: the Tate gauge.
• TauCeti.Huber.tateSeminorm: the Tate gauge as a RingSeminorm, when ϖ ∈ A₀, A = A₀[1/ϖ] and a > 1.

Main results

• TauCeti.Huber.tateGauge_zpow_mul: exact scaling tateGauge A₀ ϖ a (ϖ ^ k * x) = a ^ (-k) * tateGauge A₀ ϖ a x.
• TauCeti.Huber.tateGauge_rpow: changing the base.
• TauCeti.Huber.isNonarchimedean_tateGauge and TauCeti.Huber.tateGauge_le_zpow_iff: the gauge is ultrametric, and its closed ball of radius a ^ (-n) is ϖ ^ n A₀.
• TauCeti.Huber.hasBasis_tateGauge and TauCeti.Huber.exists_tateSeminorm: the gauge is an ultrametric ring seminorm defining the topology.
• TauCeti.Huber.tateGauge_equiv: changing the subring gives a bounded-equivalent gauge.
• TauCeti.Huber.tateGauge_eq_zero_iff and TauCeti.Huber.t2Space_iff_forall_tateGauge_eq_zero_iff: the zero set of the gauge is the closure of zero, so the gauge separates points exactly when the ring is Hausdorff.
• TauCeti.Huber.tateGauge_one: in a nonzero Hausdorff ring the gauge of one is one.

References

• K. S. Kedlaya and R. Liu, Relative p-adic Hodge theory: foundations, Astérisque 371 (2015), §2.4 and Remark 2.4.4.
• C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.

noncomputable def TauCeti.Huber.tateGauge {A : Type u_1} [CommRing A] (A₀ : Subring A) (ϖ : Aˣ) (a : ℝ) (x : A) : ℝ

The Tate gauge of a subring A₀, a unit ϖ and a base a: the infimum of a ^ (-n) over the integers n with ϖ ^ (-n) * x ∈ A₀, that is with x ∈ ϖ ^ n A₀. If no such n exists, the set is empty and the gauge takes the junk value sInf ∅ = 0.

theorem TauCeti.Huber.tateGauge_def {A : Type u_1} [CommRing A] (A₀ : Subring A) (ϖ : Aˣ) (a : ℝ) (x : A) : tateGauge A₀ ϖ a x = sInf ((fun (n : ℤ) => a ^ (-n)) '' {n : ℤ | ↑(ϖ ^ (-n)) * x ∈ A₀})

Elementary properties

theorem TauCeti.Huber.tateGauge_nonneg {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (ha : 0 ≤ a) (x : A) : 0 ≤ tateGauge A₀ ϖ a x

The Tate gauge is nonnegative for a nonnegative base.

theorem TauCeti.Huber.tateGauge_le_zpow {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (ha : 0 ≤ a) {x : A} {n : ℤ} (hn : ↑(ϖ ^ (-n)) * x ∈ A₀) : tateGauge A₀ ϖ a x ≤ a ^ (-n)

An element of ϖ ^ n A₀ has Tate gauge at most a ^ (-n).

theorem TauCeti.Huber.tateGauge_le_one {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (ha : 0 ≤ a) {x : A} (hx : x ∈ A₀) : tateGauge A₀ ϖ a x ≤ 1

An element of A₀ has Tate gauge at most one.

theorem TauCeti.Huber.tateGauge_lt_iff {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (ha : 0 ≤ a) {x : A} (hx : ∃ (n : ℤ), ↑(ϖ ^ n) * x ∈ A₀) {r : ℝ} : tateGauge A₀ ϖ a x < r ↔ ∃ (n : ℤ), ↑(ϖ ^ (-n)) * x ∈ A₀ ∧ a ^ (-n) < r

The Tate gauge is below r exactly when x ∈ ϖ ^ n A₀ for some n with a ^ (-n) < r, provided some power of ϖ moves x into A₀.

@[simp]

theorem TauCeti.Huber.tateGauge_neg {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (x : A) : tateGauge A₀ ϖ a (-x) = tateGauge A₀ ϖ a x

theorem TauCeti.Huber.tateGauge_zpow_mul {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (ha : 0 < a) (k : ℤ) (x : A) : tateGauge A₀ ϖ a (↑(ϖ ^ k) * x) = a ^ (-k) * tateGauge A₀ ϖ a x

Multiplication by ϖ ^ k scales the Tate gauge exactly by a ^ (-k).

@[simp]

theorem TauCeti.Huber.tateGauge_zero {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (ha : 1 < a) : tateGauge A₀ ϖ a 0 = 0

theorem TauCeti.Huber.tateGauge_le_zpow_mul_tateGauge {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (ha : 0 < a) {B₀ : Subring A} (x : A) (hB : ∃ (n : ℤ), ↑(ϖ ^ n) * x ∈ B₀) {k : ℤ} (hk : ∀ y ∈ B₀, ↑(ϖ ^ k) * y ∈ A₀) : tateGauge A₀ ϖ a x ≤ a ^ k * tateGauge B₀ ϖ a x

If ϖ ^ k B₀ ⊆ A₀ and a power of ϖ moves x into B₀, then the Tate gauge of A₀ at x is at most a ^ k times that of B₀.

theorem TauCeti.Huber.tateGauge_rpow {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (ha : 1 < a) {b : ℝ} (hb : 1 < b) (x : A) : tateGauge A₀ ϖ b x = tateGauge A₀ ϖ a x ^ (Real.log b / Real.log a)

Changing the base a > 1 to b > 1 raises the Tate gauge to the power log b / log a.

The Tate gauge as an ultrametric ring seminorm

theorem TauCeti.Huber.zpow_neg_mul_mem_of_le {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} (hϖ : ↑ϖ ∈ A₀) {x : A} {m n : ℤ} (hmn : m ≤ n) (hn : ↑(ϖ ^ (-n)) * x ∈ A₀) : ↑(ϖ ^ (-m)) * x ∈ A₀

If ϖ ∈ A₀, the sets ϖ ^ n A₀ decrease in n: an element of ϖ ^ n A₀ lies in ϖ ^ m A₀ for every m ≤ n.

theorem TauCeti.Huber.tateGauge_le_zpow_iff {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (hϖ : ↑ϖ ∈ A₀) {x : A} (hx : ∃ (m : ℤ), ↑(ϖ ^ m) * x ∈ A₀) (ha : 1 < a) {n : ℤ} : tateGauge A₀ ϖ a x ≤ a ^ (-n) ↔ ↑(ϖ ^ (-n)) * x ∈ A₀

If some power of ϖ moves x into A₀, then membership of x in the closed ball of radius a ^ (-n) of the Tate gauge is equivalent to membership in ϖ ^ n A₀.

theorem TauCeti.Huber.isNonarchimedean_tateGauge {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (hϖ : ↑ϖ ∈ A₀) (hA : ∀ (x : A), ∃ (n : ℤ), ↑(ϖ ^ n) * x ∈ A₀) (ha : 0 ≤ a) : IsNonarchimedean (tateGauge A₀ ϖ a)

The Tate gauge is ultrametric.

theorem TauCeti.Huber.tateGauge_mul_le_of_mem {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} {x y : A} (hy : ∃ (n : ℤ), ↑(ϖ ^ n) * y ∈ A₀) (ha : 0 ≤ a) (hx : x ∈ A₀) : tateGauge A₀ ϖ a (x * y) ≤ tateGauge A₀ ϖ a y

Multiplying an eligible element by an element of A₀ does not increase the Tate gauge.

theorem TauCeti.Huber.tateGauge_mul_le {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (x y : A) (hx : ∃ (n : ℤ), ↑(ϖ ^ n) * x ∈ A₀) (hy : ∃ (n : ℤ), ↑(ϖ ^ n) * y ∈ A₀) (ha : 0 < a) : tateGauge A₀ ϖ a (x * y) ≤ tateGauge A₀ ϖ a x * tateGauge A₀ ϖ a y

The Tate gauge is submultiplicative on elements that some powers of ϖ move into A₀.

noncomputable def TauCeti.Huber.tateSeminorm {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (hϖ : ↑ϖ ∈ A₀) (hA : ∀ (x : A), ∃ (n : ℤ), ↑(ϖ ^ n) * x ∈ A₀) (ha : 1 < a) : RingSeminorm A

The Tate gauge of A₀, ϖ and a > 1 as a ring seminorm, when every element of A is moved into A₀ by some power of ϖ.

@[simp]

theorem TauCeti.Huber.coe_tateSeminorm {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (hϖ : ↑ϖ ∈ A₀) (hA : ∀ (x : A), ∃ (n : ℤ), ↑(ϖ ^ n) * x ∈ A₀) (ha : 1 < a) : ⇑(tateSeminorm hϖ hA ha) = tateGauge A₀ ϖ a

theorem TauCeti.Huber.tateGauge_eq_zero_iff_forall {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} (hϖ : ↑ϖ ∈ A₀) {x : A} (hx : ∃ (m : ℤ), ↑(ϖ ^ m) * x ∈ A₀) (ha : 1 < a) : tateGauge A₀ ϖ a x = 0 ↔ ∀ (n : ℕ), ↑(ϖ ^ (-↑n)) * x ∈ A₀

An element that some power of ϖ moves into A₀ has Tate gauge zero exactly when it lies in every ϖ ^ n A₀, n ≥ 0.

Recovering the topology

theorem TauCeti.Huber.exists_zpow_mul_mem_of_hasBasis {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} [TopologicalSpace A] (hb : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {x : A | ↑(ϖ ^ (-↑n)) * x ∈ A₀}) [SeparatelyContinuousMul A] (x : A) : ∃ (n : ℤ), ↑(ϖ ^ n) * x ∈ A₀

If the sets ϖ ^ n A₀, n ≥ 0, form a neighbourhood basis of zero and multiplication is separately continuous, then every element of A is moved into A₀ by some power of ϖ.

theorem TauCeti.Huber.hasBasis_tateGauge {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} [TopologicalSpace A] (hb : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {x : A | ↑(ϖ ^ (-↑n)) * x ∈ A₀}) [SeparatelyContinuousMul A] (ha : 1 < a) (hϖ : ↑ϖ ∈ A₀) : (nhds 0).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {x : A | tateGauge A₀ ϖ a x < ε}

If the sets ϖ ^ n A₀, n ≥ 0, form a neighbourhood basis of zero, then so do the open balls about zero of the Tate gauge.

theorem TauCeti.Huber.exists_tateSeminorm {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} [TopologicalSpace A] (hb : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {x : A | ↑(ϖ ^ (-↑n)) * x ∈ A₀}) [SeparatelyContinuousMul A] (ha : 1 < a) (hϖ : ↑ϖ ∈ A₀) : ∃ (α : RingSeminorm A), (∀ (x : A), α x = tateGauge A₀ ϖ a x) ∧ IsNonarchimedean ⇑α ∧ (nhds 0).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {x : A | α x < ε}

A ring with separately continuous multiplication in which the sets ϖ ^ n A₀, n ≥ 0, form a neighbourhood basis of zero carries an ultrametric ring seminorm, equal to the Tate gauge, whose open balls about zero form a neighbourhood basis of zero.

theorem TauCeti.Huber.tateGauge_equiv {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} [TopologicalSpace A] (hb : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {x : A | ↑(ϖ ^ (-↑n)) * x ∈ A₀}) [SeparatelyContinuousMul A] (ha : 0 < a) {B₀ : Subring A} (hbB : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {x : A | ↑(ϖ ^ (-↑n)) * x ∈ B₀}) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : A), tateGauge A₀ ϖ a x ≤ C * tateGauge B₀ ϖ a x ∧ tateGauge B₀ ϖ a x ≤ C * tateGauge A₀ ϖ a x

For two subrings A₀ and B₀ such that the sets ϖ ^ n A₀ and the sets ϖ ^ n B₀ both form neighbourhood bases of zero, the two Tate gauges for any positive base are bounded by constant multiples of each other.

theorem TauCeti.Huber.tateGauge_eq_zero_iff {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} [TopologicalSpace A] (hb : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {x : A | ↑(ϖ ^ (-↑n)) * x ∈ A₀}) [SeparatelyContinuousMul A] [R0Space A] (ha : 1 < a) (hϖ : ↑ϖ ∈ A₀) {x : A} : tateGauge A₀ ϖ a x = 0 ↔ x ∈ closure {0}

If the sets ϖ ^ n A₀, n ≥ 0, form a neighbourhood basis of zero and ϖ ∈ A₀, then the zero set of the Tate gauge is the closure of zero.

theorem TauCeti.Huber.t2Space_iff_forall_tateGauge_eq_zero_iff {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} [TopologicalSpace A] (hb : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {x : A | ↑(ϖ ^ (-↑n)) * x ∈ A₀}) [SeparatelyContinuousMul A] [IsTopologicalAddGroup A] (ha : 1 < a) (hϖ : ↑ϖ ∈ A₀) : T2Space A ↔ ∀ (x : A), tateGauge A₀ ϖ a x = 0 ↔ x = 0

If the sets ϖ ^ n A₀, n ≥ 0, form a neighbourhood basis of zero and ϖ ∈ A₀, then the Tate gauge separates points exactly when A is Hausdorff.

theorem TauCeti.Huber.tateGauge_one {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ} {a : ℝ} [TopologicalSpace A] (hb : (nhds 0).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {x : A | ↑(ϖ ^ (-↑n)) * x ∈ A₀}) [SeparatelyContinuousMul A] [T1Space A] [Nontrivial A] (ha : 1 < a) (hϖ : ↑ϖ ∈ A₀) : tateGauge A₀ ϖ a 1 = 1

If the sets ϖ ^ n A₀, n ≥ 0, form a neighbourhood basis of zero in a nonzero T₁ ring with separately continuous multiplication and ϖ ∈ A₀, then the Tate gauge of one is one.