# Documentation

Mathlib.Topology.Algebra.Valuation

# 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 Γ₀) :

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

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

Instances For
theorem Valued.hasBasis_nhds_zero (R : Type u) [Ring R] (Γ₀ : Type v) [_i : Valued R Γ₀] :
Filter.HasBasis (nhds 0) (fun x => True) fun γ => {x | Valued.v x < γ}
theorem Valued.hasBasis_uniformity (R : Type u) [Ring R] (Γ₀ : Type v) [_i : Valued R Γ₀] :
Filter.HasBasis () (fun x => True) fun γ => {p | Valued.v (p.snd - p.fst) < γ}
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 | 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 | 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 | Valued.v y = Valued.v x} nhds x
theorem Valued.cauchy_iff {R : Type u} [Ring R] {Γ₀ : Type v} [_i : Valued R Γ₀] {F : } :
∀ (γ : Γ₀ˣ), M, M F ∀ (x : R), x M∀ (y : R), y MValued.v (y - x) < γ