The topology on a valued ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

theorem valuation.subgroups_basis {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) :

ring_subgroups_basis (λ (γ : Γ₀ˣ), v.lt_add_subgroup γ)

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

source

@[class]

structure valued (R : Type u) [ring R] (Γ₀ : out_param (Type v)) [linear_ordered_comm_group_with_zero Γ₀] :

Type (max u v)

to_uniform_space : uniform_space R
to_uniform_add_group : uniform_add_group R
v : valuation R Γ₀
is_topological_valuation : ∀ (s : set R), s ∈ nhds 0 ↔ ∃ (γ : Γ₀ˣ), {x : R | ⇑valued.v x < ↑γ} ⊆ s

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 uniform_space, uniform_add_group.

Instances of this typeclass

Instances of other typeclasses for valued

valued.has_sizeof_inst

source

def valued.mk' {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] (v : valuation R Γ₀) :

valued R Γ₀

Alternative valued constructor for use when there is no preferred uniform_space structure.

Equations

valued.mk' v = {to_uniform_space := topological_add_group.to_uniform_space R _, to_uniform_add_group := _, v := v, is_topological_valuation := _}

source

theorem valued.has_basis_nhds_zero (R : Type u) [ring R] (Γ₀ : Type v) [linear_ordered_comm_group_with_zero Γ₀] [valued R Γ₀] :

(nhds 0).has_basis (λ (_x : Γ₀ˣ), true) (λ (γ : Γ₀ˣ), {x : R | ⇑valued.v x < ↑γ})

source

theorem valued.has_basis_uniformity (R : Type u) [ring R] (Γ₀ : Type v) [linear_ordered_comm_group_with_zero Γ₀] [valued R Γ₀] :

(uniformity R).has_basis (λ (_x : Γ₀ˣ), true) (λ (γ : Γ₀ˣ), {p : R × R | ⇑valued.v (p.snd - p.fst) < ↑γ})

source

theorem valued.to_uniform_space_eq (R : Type u) [ring R] (Γ₀ : Type v) [linear_ordered_comm_group_with_zero Γ₀] [valued R Γ₀] :

valued.to_uniform_space = topological_add_group.to_uniform_space R

source

theorem valued.mem_nhds {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] [valued R Γ₀] {s : set R} {x : R} :

s ∈ nhds x ↔ ∃ (γ : Γ₀ˣ), {y : R | ⇑valued.v (y - x) < ↑γ} ⊆ s

source

theorem valued.mem_nhds_zero {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] [valued R Γ₀] {s : set R} :

s ∈ nhds 0 ↔ ∃ (γ : Γ₀ˣ), {x : R | ⇑valued.v x < ↑γ} ⊆ s

source

theorem valued.loc_const {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] [valued R Γ₀] {x : R} (h : ⇑valued.v x ≠ 0) :

{y : R | ⇑valued.v y = ⇑valued.v x} ∈ nhds x

source

@[protected, instance]

def valued.topological_ring {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] [valued R Γ₀] :

topological_ring R

source

theorem valued.cauchy_iff {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] [valued R Γ₀] {F : filter R} :

cauchy F ↔ F.ne_bot ∧ ∀ (γ : Γ₀ˣ), ∃ (M : set R) (H : M ∈ F), ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ⇑valued.v (y - x) < ↑γ