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 (γ : Γ₀ˣ) => Valuation.ltAddSubgroup v γ

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.

• IsOpen : Set R → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter : ∀ (s t : Set R), TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion : ∀ (s : Set (Set R)), (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• uniformity : Filter (R × R)
• refl : Filter.principal idRel ≤ self.uniformity
• symm : Filter.Tendsto Prod.swap self.uniformity self.uniformity
• comp : (Filter.lift' self.uniformity fun (s : Set (R × R)) => compRel s s) ≤ self.uniformity
• isOpen_uniformity : ∀ (s : Set R), IsOpen s ↔ ∀ x ∈ s, {p : R × R | p.1 = x → p.2 ∈ s} ∈ self.uniformity
• uniformContinuous_sub : UniformContinuous fun (p : R × R) => p.1 - p.2
• v : Valuation R Γ₀
• is_topological_valuation : ∀ (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

• Valued.mk' v = Valued.mk v (_ : ∀ (s : Set R), s ∈ nhds 0 ↔ ∃ (γ : Γ₀ˣ), {x : R | v x < ↑γ} ⊆ s)

theorem Valued.hasBasis_nhds_zero (R : Type u) [Ring R] (Γ₀ : Type v) [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] : Filter.HasBasis (nhds 0) (fun (x : Γ₀ˣ) => True) fun (γ : Γ₀ˣ) => {x : R | Valued.v x < ↑γ}

theorem Valued.hasBasis_uniformity (R : Type u) [Ring R] (Γ₀ : Type v) [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] : Filter.HasBasis (uniformity R) (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 Valued.instTopologicalRingToTopologicalSpaceToUniformSpaceToNonUnitalNonAssocRingToNonAssocRing {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] : TopologicalRing R

Equations

• (_ : TopologicalRing R) = (_ : TopologicalRing R)

theorem Valued.cauchy_iff {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀] {F : Filter R} : Cauchy F ↔ Filter.NeBot F ∧ ∀ (γ : Γ₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, Valued.v (y - x) < ↑γ