# 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.

theorem Valuation.subgroups_basis {R : Type u} [Ring R] {Γ₀ : Type v} (v : Valuation R Γ₀) :
RingSubgroupsBasis fun (γ : Γ₀ˣ) => v.ltAddSubgroup γ

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

class Valued (R : Type u) [Ring R] (Γ₀ : ) extends , :
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, UniformAddGroup.

Instances
theorem Valued.is_topological_valuation {R : Type u} [Ring R] {Γ₀ : } [self : Valued R Γ₀] (s : Set R) :
s nhds 0 ∃ (γ : Γ₀ˣ), {x : R | Valued.v x < γ} s
def Valued.mk' {R : Type u} [Ring R] {Γ₀ : Type v} (v : Valuation R Γ₀) :
Valued R Γ₀

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

Equations
Instances For
theorem Valued.hasBasis_nhds_zero (R : Type u) [Ring R] (Γ₀ : Type v) [_i : Valued R Γ₀] :
(nhds 0).HasBasis (fun (x : Γ₀ˣ) => True) fun (γ : Γ₀ˣ) => {x : R | Valued.v x < γ}
theorem Valued.hasBasis_uniformity (R : Type u) [Ring R] (Γ₀ : Type v) [_i : Valued R Γ₀] :
(uniformity R).HasBasis (fun (x : Γ₀ˣ) => True) fun (γ : Γ₀ˣ) => {p : R × R | Valued.v (p.2 - p.1) < γ}
theorem Valued.toUniformSpace_eq (R : Type u) [Ring R] (Γ₀ : Type v) [_i : Valued R Γ₀] :
Valued.toUniformSpace =
theorem Valued.mem_nhds {R : Type u} [Ring R] {Γ₀ : Type v} [_i : Valued R Γ₀] {s : Set R} {x : R} :
s nhds x ∃ (γ : Γ₀ˣ), {y : R | Valued.v (y - x) < γ} s
theorem Valued.mem_nhds_zero {R : Type u} [Ring R] {Γ₀ : Type v} [_i : Valued R Γ₀] {s : Set R} :
s nhds 0 ∃ (γ : Γ₀ˣ), {x : R | Valued.v x < γ} s
theorem Valued.loc_const {R : Type u} [Ring R] {Γ₀ : Type v} [_i : Valued R Γ₀] {x : R} (h : Valued.v x 0) :
{y : R | Valued.v y = Valued.v x} nhds x
@[instance 100]
instance Valued.instTopologicalRing {R : Type u} [Ring R] {Γ₀ : Type v} [_i : Valued R Γ₀] :
Equations
• =
theorem Valued.cauchy_iff {R : Type u} [Ring R] {Γ₀ : Type v} [_i : Valued R Γ₀] {F : } :
F.NeBot ∀ (γ : Γ₀ˣ), MF, xM, yM, Valued.v (y - x) < γ
theorem Valued.integer_isOpen (R : Type u) [Ring R] {Γ₀ : Type v} [_i : Valued R Γ₀] :
IsOpen Valued.v.integer

The unit ball of a valued ring is open.

theorem Valued.valuationSubring_isOpen {Γ₀ : Type v} (K : Type u) [] [hv : Valued K Γ₀] :
IsOpen Valued.v.valuationSubring

The valuation subring of a valued field is open.