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)

• IsOpen : Set R → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter : ∀ (s_1 t : Set R), TopologicalSpace.IsOpen s_1 → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s_1 ∩ t)
• isOpen_sUnion : ∀ (s_1 : Set (Set R)), (∀ (t : Set R), t ∈ s_1 → TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s_1)
• uniformity : Filter (R × R)
• refl : Filter.principal idRel ≤ s.uniformity
• symm : Filter.Tendsto Prod.swap s.uniformity s.uniformity
• comp : (Filter.lift' s.uniformity fun s => compRel s s) ≤ s.uniformity
• isOpen_uniformity : ∀ (s_1 : Set R), IsOpen s_1 ↔ ∀ (x : R), x ∈ s_1 → {p | p.fst = x → p.snd ∈ s_1} ∈ s.uniformity
• uniformContinuous_sub : UniformContinuous fun p => p.fst - p.snd
• v : Valuation R Γ₀
• is_topological_valuation : ∀ (s_1 : Set R), s_1 ∈ nhds 0 ↔ ∃ γ, {x | ↑Valued.v x < ↑γ} ⊆ s_1

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.

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.

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 | ↑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 | ↑Valued.v (p.snd - p.fst) < ↑γ}

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 | ↑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 | ↑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 | ↑Valued.v y = ↑Valued.v x} ∈ nhds x

instance Valued.instTopologicalRingToTopologicalSpaceToUniformSpaceToNonUnitalNonAssocRingToNonAssocRing {R : Type u} [Ring R] {Γ₀ : Type v} [LinearOrderedCommGroupWithZero Γ₀] [_i : Valued 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, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑Valued.v (y - x) < ↑γ