# The topology on a valued ring #

In this file, we define the non-Archimedean topology induced by a valuation on a ring. The main definition is a `Valued` type class which equips a ring with a valuation taking values in a group with zero. Other instances are then deduced from this.

NOTE (2025-07-02): The `Valued` class defined in this file will eventually get replaced with `ValuativeRel` from `Mathlib.RingTheory.Valuation.ValuativeRel.Basic`. New developments on valued rings/fields should take this into consideration.

source
theorem Valuation.map_eq_one_of_forall_lt {K : Type u} [DivisionRing K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [MulArchimedean Γ₀] {v : Valuation K Γ₀} {r : Γ₀} (hr : r ≠ 0) (h : ∀ (x : K), v x ≠ 0 → r < v x) (x : K) (hx : v x ≠ 0) :
v x = 1
source
theorem Valuation.subgroups_basis {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :
RingSubgroupsBasis fun (γ : Γ₀ ˣ) => v.ltAddSubgroup γ

The basis of open subgroups for the topology on a ring determined by a valuation.

source
class Valued (R : Type u) [Ring R] (Γ₀ : outParam (Type v)) [LinearOrderedCommGroupWithZero Γ₀] extends UniformSpace R, IsUniformAddGroup R :
Type (max u v)

A valued ring is a ring that comes equipped with a distinguished valuation. The class `Valued` is designed for the situation that there is a canonical valuation on the ring.

TODO: show that there always exists an equivalent valuation taking values in a type belonging to the same universe as the ring.

See Note [forgetful inheritance] for why we extend `UniformSpace`, `IsUniformAddGroup`.

- IsOpen : Set R → Prop
- isOpen_univ : TopologicalSpace.IsOpen Set.univ
- isOpen_inter (s t : Set R) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
- isOpen_sUnion (s : Set (Set R)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
- uniformity : Filter (R × R)
- symm : Filter.Tendsto Prod.swap UniformSpace.uniformity UniformSpace.uniformity
- comp : (UniformSpace.uniformity.lift' fun (s : Set (R × R)) => SetRel.comp s s) ≤ UniformSpace.uniformity
- nhds_eq_comap_uniformity (x : R) : nhds x = Filter.comap (Prod.mk x) UniformSpace.uniformity
- uniformContinuous_sub : UniformContinuous fun (p : R × R) => p.1 - p.2
- v : Valuation R Γ₀
- is_topological_valuation (s : Set R) : s ∈ nhds 0 ↔ ∃ (γ : Γ₀ ˣ), {x : R | v x < ↑γ} ⊆ s

Instances

source
def Valued.mk' {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) :
Valued R Γ₀

Alternative `Valued` constructor for use when there is no preferred `UniformSpace` structure.

Equations

- Valued.mk' v = { toUniformSpace := IsTopologicalAddGroup.rightUniformSpace R, toIsUniformAddGroup := ⋯, v := v, is_topological_valuation := ⋯ }

Instances For

source
theorem Valued.hasBasis_nhds_zero (R : Type u) [Ring R] (Γ₀ : Type v) [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
(nhds 0).HasBasis (fun (x : Γ₀ ˣ) => True) fun (γ : Γ₀ ˣ) => {x : R | v x < ↑γ}
source
theorem Valued.hasBasis_uniformity (R : Type u) [Ring R] (Γ₀ : Type v) [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
(uniformity R).HasBasis (fun (x : Γ₀ ˣ) => True) fun (γ : Γ₀ ˣ) => {p : R × R | v (p.2 - p.1) < ↑γ}
source
theorem Valued.toUniformSpace_eq (R : Type u) [Ring R] (Γ₀ : Type v) [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
_i.toUniformSpace = IsTopologicalAddGroup.rightUniformSpace R
source
theorem Valued.mem_nhds {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {s : Set R} {x : R} :
s ∈ nhds x ↔ ∃ (γ : Γ₀ ˣ), {y : R | v (y - x) < ↑γ} ⊆ s
source
theorem Valued.mem_nhds_zero {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {s : Set R} :
s ∈ nhds 0 ↔ ∃ (γ : Γ₀ ˣ), {x : R | v x < ↑γ} ⊆ s
source
theorem Valued.loc_const {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {x : R} (h : v x ≠ 0) :
{y : R | v y = v x} ∈ nhds x
source
@[instance 100]
instance Valued.instIsTopologicalRing {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
IsTopologicalRing R
source
theorem Valued.discreteTopology_of_forall_map_eq_one {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] (h : ∀ (x : R), x ≠ 0 → v x = 1) :
DiscreteTopology R
source
theorem Valued.discreteTopology_of_forall_lt {K : Type u} [DivisionRing K] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [MulArchimedean Γ₀] [Valued K Γ₀] {r : Γ₀} (hr : r ≠ 0) (h : ∀ (x : K), v x ≠ 0 → r < v x) :
DiscreteTopology K
source
theorem Valued.cauchy_iff {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {F : Filter R} :
Cauchy F ↔ F.NeBot ∧ ∀ (γ : Γ₀ ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v (y - x) < ↑γ
source
theorem Valued.isOpen_ball (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] (r : Γ₀) :
IsOpen {x : R | v x < r}

An open ball centred at the origin in a valued ring is open.

source
theorem Valued.isClosed_ball (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] (r : Γ₀) :
IsClosed {x : R | v x < r}

An open ball centred at the origin in a valued ring is closed.

source
theorem Valued.isClopen_ball (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] (r : Γ₀) :
IsClopen {x : R | v x < r}

An open ball centred at the origin in a valued ring is clopen.

source
theorem Valued.isOpen_closedBall (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {r : Γ₀} (hr : r ≠ 0) :
IsOpen {x : R | v x ≤ r}

A closed ball centred at the origin in a valued ring is open.

source
@[deprecated Valued.isOpen_closedBall (since := "2025-10-09")]
theorem Valued.isOpen_closedball (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {r : Γ₀} (hr : r ≠ 0) :
IsOpen {x : R | v x ≤ r}

Alias of `Valued.isOpen_closedBall`.

A closed ball centred at the origin in a valued ring is open.

source
theorem Valued.isClosed_closedBall (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] (r : Γ₀) :
IsClosed {x : R | v x ≤ r}

A closed ball centred at the origin in a valued ring is closed.

source
theorem Valued.isClopen_closedBall (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {r : Γ₀} (hr : r ≠ 0) :
IsClopen {x : R | v x ≤ r}

A closed ball centred at the origin in a valued ring is clopen.

source
theorem Valued.isClopen_sphere (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {r : Γ₀} (hr : r ≠ 0) :
IsClopen {x : R | v x = r}

A sphere centred at the origin in a valued ring is clopen.

source
theorem Valued.isOpen_sphere (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {r : Γ₀} (hr : r ≠ 0) :
IsOpen {x : R | v x = r}

A sphere centred at the origin in a valued ring is open.

source
theorem Valued.isClosed_sphere (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] (r : Γ₀) :
IsClosed {x : R | v x = r}

A sphere centred at the origin in a valued ring is closed.

source
theorem Valued.isOpen_integer (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
IsOpen ↑v.integer

The closed unit ball in a valued ring is open.

source
@[deprecated Valued.isOpen_integer (since := "2025-04-25")]
theorem Valued.integer_isOpen (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
IsOpen ↑v.integer

Alias of `Valued.isOpen_integer`.

The closed unit ball in a valued ring is open.

source
theorem Valued.isClosed_integer (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
IsClosed ↑v.integer

The closed unit ball of a valued ring is closed.

source
theorem Valued.isClopen_integer (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
IsClopen ↑v.integer

The closed unit ball of a valued ring is clopen.

source
theorem Valued.isOpen_valuationSubring {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] (K : Type u) [Field K] [hv : Valued K Γ₀] :
IsOpen ↑v.valuationSubring

The valuation subring of a valued field is open.

source
@[deprecated Valued.isOpen_valuationSubring (since := "2025-04-25")]
theorem Valued.valuationSubring_isOpen {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] (K : Type u) [Field K] [hv : Valued K Γ₀] :
IsOpen ↑v.valuationSubring

Alias of `Valued.isOpen_valuationSubring`.

The valuation subring of a valued field is open.

source
theorem Valued.isClosed_valuationSubring {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] (K : Type u) [Field K] [hv : Valued K Γ₀] :
IsClosed ↑v.valuationSubring

The valuation subring of a valued field is closed.

source
theorem Valued.isClopen_valuationSubring {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] (K : Type u) [Field K] [hv : Valued K Γ₀] :
IsClopen ↑v.valuationSubring

The valuation subring of a valued field is clopen.