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/Data/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
• Show that the UniformSpace.Completion of an IsUltraUniformity is IsUltraUniformity

References

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

def IsTransitiveRel {X : Type u_1} (V : Set (X × X)) : Prop

The relation is transitive.

Equations

• IsTransitiveRel V = ∀ ⦃x y z : X⦄, (x, y) ∈ V → (y, z) ∈ V → (x, z) ∈ V

theorem IsTransitiveRel.comp_subset_self {X : Type u_1} {s : Set (X × X)} (h : IsTransitiveRel s) : compRel s s ⊆ s

theorem isTransitiveRel_iff_comp_subset_self {X : Type u_1} {s : Set (X × X)} : IsTransitiveRel s ↔ compRel s s ⊆ s

theorem isTransitiveRel_empty {X : Type u_1} : IsTransitiveRel ∅

theorem isTransitiveRel_univ {X : Type u_1} : IsTransitiveRel Set.univ

theorem isTransitiveRel_singleton {X : Type u_1} (x y : X) : IsTransitiveRel {(x, y)}

theorem IsTransitiveRel.inter {X : Type u_1} {s t : Set (X × X)} (hs : IsTransitiveRel s) (ht : IsTransitiveRel t) : IsTransitiveRel (s ∩ t)

theorem IsTransitiveRel.iInter {X : Type u_1} {ι : Type u_2} {U : ι → Set (X × X)} (hU : ∀ (i : ι), IsTransitiveRel (U i)) : IsTransitiveRel (⋂ (i : ι), U i)

theorem IsTransitiveRel.sInter {X : Type u_1} {s : Set (Set (X × X))} (h : ∀ i ∈ s, IsTransitiveRel i) : IsTransitiveRel (⋂₀ s)

theorem IsTransitiveRel.preimage_prodMap {X : Type u_1} {Y : Type u_2} {t : Set (Y × Y)} (ht : IsTransitiveRel t) (f : X → Y) : IsTransitiveRel (Prod.map f f ⁻¹' t)

theorem IsTransitiveRel.symmetrizeRel {X : Type u_1} {s : Set (X × X)} (h : IsTransitiveRel s) : IsTransitiveRel (_root_.symmetrizeRel s)

theorem IsTransitiveRel.comp_eq_of_idRel_subset {X : Type u_1} {s : Set (X × X)} (h : IsTransitiveRel s) (h' : idRel ⊆ s) : compRel s s = s

theorem IsTransitiveRel.ball_subset_of_mem {X : Type u_1} {V : Set (X × X)} (h : IsTransitiveRel V) {x y : X} (hy : y ∈ UniformSpace.ball x V) : UniformSpace.ball y V ⊆ UniformSpace.ball x V

theorem UniformSpace.ball_eq_of_mem_of_isSymmetricRel_of_isTransitiveRel {X : Type u_1} {V : Set (X × X)} (h_symm : IsSymmetricRel V) (h_trans : IsTransitiveRel V) {x y : X} (hy : y ∈ ball x V) : ball x V = ball y V

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 : Set (X × X)) => s ∈ uniformity X ∧ IsSymmetricRel s ∧ IsTransitiveRel s) id

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

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

theorem UniformSpace.isClosed_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity {X : Type u_1} [UniformSpace X] (x : X) {V : Set (X × X)} (h_symm : IsSymmetricRel V) (h_trans : IsTransitiveRel V) (h' : V ∈ uniformity X) : IsClosed (ball x V)

theorem UniformSpace.isClopen_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity {X : Type u_1} [UniformSpace X] (x : X) {V : Set (X × X)} (h_symm : IsSymmetricRel V) (h_trans : IsTransitiveRel V) (h' : V ∈ uniformity X) : IsClopen (ball x V)

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.