mathlib documentation

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.

source
@[class]
structure valued (R : Type u) [ring R] (Γ₀ : out_param (Type v)) [linear_ordered_comm_group_with_zero Γ₀] :
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. It allows such a valuation to be registered as a typeclass; this is used for instance by valued.topological_space.

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

Instances
source
theorem valued.subgroups_basis {R : Type u} [ring R] (Γ₀ : Type v) [linear_ordered_comm_group_with_zero Γ₀] [hv : valued R Γ₀] :
ring_subgroups_basis (λ (γ : Γ₀ˣ), valued.v.lt_add_subgroup γ)

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

source
@[protected, nolint, instance]
def valued.topological_space {R : Type u} [ring R] (Γ₀ : Type v) [linear_ordered_comm_group_with_zero Γ₀] [hv : valued R Γ₀] :
topological_space R

The topological space structure on a valued ring.

NOTE: The dangerous_instance linter does not check whether the metavariables only occur in arguments marked with out_param, so in this instance it gives a false positive.

Equations
source
theorem valued.mem_nhds {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued R Γ₀] {s : set R} {x : R} :
s ∈ 𝓝 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 Γ₀] [hv : valued R Γ₀] {s : set R} :
s ∈ 𝓝 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 Γ₀] [hv : valued R Γ₀] {x : R} (h : ⇑valued.v x ≠ 0) :
{y : R | ⇑valued.v y = ⇑valued.v x} ∈ 𝓝 x
source
@[protected, nolint, instance]
def valued.uniform_space {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued R Γ₀] :
uniform_space R

The uniform structure on a valued ring.

NOTE: The dangerous_instance linter does not check whether the metavariables only occur in arguments marked with out_param, so in this instance it gives a false positive.

Equations
source
@[protected, instance]
def valued.uniform_add_group {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] [hv : valued R Γ₀] :
uniform_add_group R

A valued ring is a uniform additive group.

source
theorem valued.cauchy_iff {R : Type u} [ring R] {Γ₀ : Type v} [linear_ordered_comm_group_with_zero Γ₀] [hv : 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) < ↑γ