Ultrametric (nonarchimedean) uniform spaces

Ultrametric (nonarchimedean) uniform spaces are ones that generalize ultrametric spaces by having a uniformity based on equivalence relations.

Main definitions

In this file we define IsUltraUniformity, a Prop mixin typeclass.

Main results

• TopologicalSpace.isTopologicalBasis_clopens: a uniform space with a nonarchimedean uniformity has a topological basis of clopen sets in the topology, meaning that it is topologically zero-dimensional.

Implementation notes

As in the Mathlib/Topology/UniformSpace/Defs.lean file, we do not reuse Mathlib/Basic/Rel.lean but rather extend the relation properties as needed.

TODOs

• Prove that IsUltraUniformity iff metrizable by IsUltrametricDist on a PseudoMetricSpace under a countable system/basis condition
• Generalize IsUltrametricDist to IsUltrametricUniformity
• Provide IsUltraUniformity for the uniformity in a Valued ring
• Generalize results about open/closed balls and spheres in IsUltraUniformity to combine applications for MetricSpace.ball and valued "balls"
• Use IsUltraUniformity to work with profinite/totally separated spaces

References

• D. Windisch, Equivalent characterizations of non-Archimedean uniform spaces
• [A. C. M. van Rooij, Non-Archimedean uniformities][vanrooij1970]

theorem IsTransitiveRel.prod_subset_trans {X : Type u_1} {s : SetRel X X} {t u v : Set X} [s.IsTrans] (htu : t ×ˢ u ⊆ s) (huv : u ×ˢ v ⊆ s) (hu : u.Nonempty) : t ×ˢ v ⊆ s

theorem IsTransitiveRel.mem_filter_prod_trans {X : Type u_1} {s : SetRel X X} {f g h : Filter X} [g.NeBot] [s.IsTrans] (hfg : s ∈ f ×ˢ g) (hgh : s ∈ g ×ˢ h) : s ∈ f ×ˢ h

theorem ball_subset_of_mem {X : Type u_1} {V : SetRel X X} [V.IsTrans] {x y : X} (hy : y ∈ V.ball x) : V.ball y ⊆ V.ball x

theorem ball_eq_of_mem {X : Type u_1} {V : SetRel X X} [V.IsSymm] [V.IsTrans] {x y : X} (hy : y ∈ V.ball x) : V.ball x = V.ball y

class IsUltraUniformity (X : Type u_1) [UniformSpace X] : Prop

A uniform space is ultrametric if the uniformity 𝓤 X has a basis of equivalence relations.

• hasBasis : (uniformity X).HasBasis (fun (s : SetRel X X) => s ∈ uniformity X ∧ s.IsSymm ∧ s.IsTrans) id

theorem IsUltraUniformity.mk_of_hasBasis {X : Type u_1} [UniformSpace X] {ι : Type u_2} {p : ι → Prop} {s : ι → SetRel X X} (h_basis : (uniformity X).HasBasis p s) (h_symm : ∀ (i : ι), p i → (s i).IsSymm) (h_trans : ∀ (i : ι), p i → (s i).IsTrans) : IsUltraUniformity X

theorem IsUltraUniformity.mem_nhds_iff_symm_trans {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] {x : X} {s : Set X} : s ∈ nhds x ↔ ∃ V ∈ uniformity X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ SetRel.ball V x ⊆ s

theorem UniformSpace.isOpen_ball_of_mem_uniformity {X : Type u_1} [UniformSpace X] (x : X) {V : SetRel X X} [V.IsTrans] (h' : V ∈ uniformity X) : IsOpen (V.ball x)

theorem UniformSpace.isClosed_ball_of_isSymm_of_isTrans_of_mem_uniformity {X : Type u_1} [UniformSpace X] (x : X) {V : SetRel X X} [V.IsSymm] [V.IsTrans] (h' : V ∈ uniformity X) : IsClosed (V.ball x)

theorem UniformSpace.isClopen_ball_of_isSymm_of_isTrans_of_mem_uniformity {X : Type u_1} [UniformSpace X] (x : X) {V : SetRel X X} [V.IsSymm] [V.IsTrans] (h' : V ∈ uniformity X) : IsClopen (V.ball x)

theorem UniformSpace.nhds_basis_clopens {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => x ∈ s ∧ IsClopen s) id

theorem TopologicalSpace.isTopologicalBasis_clopens {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] : IsTopologicalBasis {s : Set X | IsClopen s}

A uniform space with a nonarchimedean uniformity is zero-dimensional.