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 , TopologicalSpace : 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)
• symm : Filter.Tendsto Prod.swap UniformSpace.uniformity UniformSpace.uniformity
• comp : (UniformSpace.uniformity.lift' fun (s : Set (R × R)) => compRel s s) ≤ UniformSpace.uniformity
• nhds_eq_comap_uniformity : ∀ (x : R), nhds x = Filter.comap (Prod.mk x) UniformSpace.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

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

• Valued.mk' v = Valued.mk v ⋯

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 Γ₀] : TopologicalRing R

Equations

• ⋯ = ⋯

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