mathlib documentation


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 (living in the same universe). Other instances are then deduced from this.

structure valued (R : Type u) [ring R] :
Type (u+1)

A valued ring is a ring that comes equipped with a distinguished valuation.

theorem valued.subgroups_basis {R : Type u_1} [ring R] [valued R] :

The basis of open subgroups for the topology on a valued ring.

@[protected, instance]
def valued.topological_space {R : Type u_1} [ring R] [valued R] :
theorem valued.mem_nhds {R : Type u_1} [ring R] [valued R] {s : set R} {x : R} :
s 𝓝 x ∃ (γ : units (valued.Γ₀ R)), {y : R | valued.v (y - x) < γ} s
theorem valued.mem_nhds_zero {R : Type u_1} [ring R] [valued R] {s : set R} :
s 𝓝 0 ∃ (γ : units (valued.Γ₀ R)), {x : R | valued.v x < γ} s
theorem valued.loc_const {R : Type u_1} [ring R] [valued R] {x : R} (h : valued.v x 0) :
{y : R | valued.v y = valued.v x} 𝓝 x
@[protected, instance]
def valued.uniform_space {R : Type u_1} [ring R] [valued R] :

The uniform structure on a valued ring.

@[protected, instance]
def valued.uniform_add_group {R : Type u_1} [ring R] [valued R] :

A valued ring is a uniform additive group.

theorem valued.cauchy_iff {R : Type u_1} [ring R] [valued R] {F : filter R} :
cauchy F F.ne_bot ∀ (γ : units (valued.Γ₀ R)), ∃ (M : set R) (H : M F), ∀ (x y : R), x My Mvalued.v (y - x) < γ