Documentation

Mathlib.Topology.Algebra.Valued.ValuationTopology

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} [LinearOrderedCommGroupWithZero Γ₀] (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] (Γ₀ : outParam (Type v)) [LinearOrderedCommGroupWithZero Γ₀] extends UniformSpace , UniformAddGroup :
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} :
    ∀ {inst : Ring R} {Γ₀ : outParam (Type v)} {inst_1 : LinearOrderedCommGroupWithZero Γ₀} [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} [LinearOrderedCommGroupWithZero Γ₀] (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) [LinearOrderedCommGroupWithZero Γ₀] [_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) [LinearOrderedCommGroupWithZero Γ₀] [_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) [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
      Valued.toUniformSpace = TopologicalAddGroup.toUniformSpace R
      theorem Valued.mem_nhds {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_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} [LinearOrderedCommGroupWithZero Γ₀] [_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} [LinearOrderedCommGroupWithZero Γ₀] [_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} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
      Equations
      • =
      theorem Valued.cauchy_iff {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {F : Filter R} :
      Cauchy F F.NeBot ∀ (γ : Γ₀ˣ), MF, xM, yM, Valued.v (y - x) < γ
      theorem Valued.integer_isOpen (R : Type u) [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] :
      IsOpen Valued.v.integer

      The unit ball of a valued ring is open.

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

      The valuation subring of a valued field is open.