mathlib documentation

topology.uniform_space.separation

Hausdorff properties of uniform spaces. Separation quotient. #

This file studies uniform spaces whose underlying topological spaces are separated (also known as Hausdorff or T₂). This turns out to be equivalent to asking that the intersection of all entourages is the diagonal only. This condition actually implies the stronger separation property that the space is regular (T₃), hence those conditions are equivalent for topologies coming from a uniform structure.

More generally, the intersection 𝓢 X of all entourages of X, which has type set (X × X) is an equivalence relation on X. Points which are equivalent under the relation are basically undistinguishable from the point of view of the uniform structure. For instance any uniformly continuous function will send equivalent points to the same value.

The quotient separation_quotient X of X by 𝓢 X has a natural uniform structure which is separated, and satisfies a universal property: every uniformly continuous function from X to a separated uniform space uniquely factors through separation_quotient X. As usual, this allows to turn separation_quotient into a functor (but we don't use the category theory library in this file).

These notions admit relative versions, one can ask that s : set X is separated, this is equivalent to asking that the uniform structure induced on s is separated.

Main definitions #

separation_relation X : set (X × X): the separation relation
separated_space X: a predicate class asserting that X is separated
is_separated s: a predicate asserting that s : set X is separated
separation_quotient X: the maximal separated quotient of X.
separation_quotient.lift f: factors a map f : X → Y through the separation quotient of X.
separation_quotient.map f: turns a map f : X → Y into a map between the separation quotients of X and Y.

Main results #

separated_iff_t2: the equivalence between being separated and being Hausdorff for uniform spaces.
separation_quotient.uniform_continuous_lift: factoring a uniformly continuous map through the separation quotient gives a uniformly continuous map.
separation_quotient.uniform_continuous_map: maps induced between separation quotients are uniformly continuous.

Notations #

Localized in uniformity, we have the notation 𝓢 X for the separation relation on a uniform space X,

Implementation notes #

The separation setoid separation_setoid is not declared as a global instance. It is made a local instance while building the theory of separation_quotient. The factored map separation_quotient.lift f is defined without imposing any condition on f, but returns junk if f is not uniformly continuous (constant junk hence it is always uniformly continuous).

Separated uniform spaces #

@[protected]

def separation_rel (α : Type u) [u : uniform_space α] :

set (α × α)

The separation relation is the intersection of all entourages. Two points which are related by the separation relation are "indistinguishable" according to the uniform structure.

Equations

𝓢 α = ⋂₀ (𝓤 α).sets

theorem separated_equiv {α : Type u} [uniform_space α] :

equivalence (λ (x y : α), (x, y) ∈ 𝓢 α)

@[class]

structure separated_space (α : Type u) [uniform_space α] :

Prop

out : 𝓢 α = id_rel

A uniform space is separated if its separation relation is trivial (each point is related only to itself).

Instances

theorem separated_space_iff {α : Type u} [uniform_space α] :

separated_space α ↔ 𝓢 α = id_rel

theorem separated_def {α : Type u} [uniform_space α] :

separated_space α ↔ ∀ (x y : α), (∀ (r : set (α × α)), r ∈ 𝓤 α → (x, y) ∈ r) → x = y

theorem separated_def' {α : Type u} [uniform_space α] :

separated_space α ↔ ∀ (x y : α), x ≠ y → (∃ (r : set (α × α)) (H : r ∈ 𝓤 α), (x, y) ∉ r)

theorem eq_of_uniformity {α : Type u_1} [uniform_space α] [separated_space α] {x y : α} (h : ∀ {V : set (α × α)}, V ∈ 𝓤 α → (x, y) ∈ V) :

x = y

theorem eq_of_uniformity_basis {α : Type u_1} [uniform_space α] [separated_space α] {ι : Type u_2} {p : ι → Prop} {s : ι → set (α × α)} (hs : (𝓤 α).has_basis p s) {x y : α} (h : ∀ {i : ι}, p i → (x, y) ∈ s i) :

x = y

theorem eq_of_forall_symmetric {α : Type u_1} [uniform_space α] [separated_space α] {x y : α} (h : ∀ {V : set (α × α)}, V ∈ 𝓤 α → symmetric_rel V → (x, y) ∈ V) :

x = y

theorem id_rel_sub_separation_relation (α : Type u_1) [uniform_space α] :

id_rel ⊆ 𝓢 α

theorem separation_rel_comap {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : α → β} (h : _inst_1 = uniform_space.comap f _inst_2) :

𝓢 α = prod.map f f ⁻¹' 𝓢 β

@[protected]

theorem filter.has_basis.separation_rel {α : Type u} [uniform_space α] {ι : Sort u_1} {p : ι → Prop} {s : ι → set (α × α)} (h : (𝓤 α).has_basis p s) :

𝓢 α = ⋂ (i : ι) (hi : p i), s i

theorem separation_rel_eq_inter_closure {α : Type u} [uniform_space α] :

𝓢 α = ⋂₀ (closure '' (𝓤 α).sets)

theorem is_closed_separation_rel {α : Type u} [uniform_space α] :

is_closed (𝓢 α)

theorem separated_iff_t2 {α : Type u} [uniform_space α] :

separated_space α ↔ t2_space α

@[protected, instance]

def separated_regular {α : Type u} [uniform_space α] [separated_space α] :

regular_space α

theorem is_closed_of_spaced_out {α : Type u} [uniform_space α] [separated_space α] {V₀ : set (α × α)} (V₀_in : V₀ ∈ 𝓤 α) {s : set α} (hs : s.pairwise (λ (x y : α), (x, y) ∉ V₀)) :

theorem is_closed_range_of_spaced_out {α : Type u} [uniform_space α] {ι : Type u_1} [separated_space α] {V₀ : set (α × α)} (V₀_in : V₀ ∈ 𝓤 α) {f : ι → α} (hf : pairwise (λ (x y : ι), (f x, f y) ∉ V₀)) :

is_closed (set.range f)

Separated sets #

def is_separated {α : Type u} [uniform_space α] (s : set α) :

Prop

A set s in a uniform space α is separated if the separation relation 𝓢 α induces the trivial relation on s.

Equations

is_separated s = ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (x, y) ∈ 𝓢 α → x = y

theorem is_separated_def {α : Type u} [uniform_space α] (s : set α) :

is_separated s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → (x, y) ∈ 𝓢 α → x = y

theorem is_separated_def' {α : Type u} [uniform_space α] (s : set α) :

is_separated s ↔ s ×ˢ s ∩ 𝓢 α ⊆ id_rel

theorem is_separated.mono {α : Type u} [uniform_space α] {s t : set α} (hs : is_separated s) (hts : t ⊆ s) :

theorem univ_separated_iff {α : Type u} [uniform_space α] :

is_separated set.univ ↔ separated_space α

theorem is_separated_of_separated_space {α : Type u} [uniform_space α] [separated_space α] (s : set α) :

theorem is_separated_iff_induced {α : Type u} [uniform_space α] {s : set α} :

is_separated s ↔ separated_space ↥s

theorem eq_of_uniformity_inf_nhds_of_is_separated {α : Type u} [uniform_space α] {s : set α} (hs : is_separated s) {x y : α} :

x ∈ s → y ∈ s → cluster_pt (x, y) (𝓤 α) → x = y

theorem eq_of_uniformity_inf_nhds {α : Type u} [uniform_space α] [separated_space α] {x y : α} :

cluster_pt (x, y) (𝓤 α) → x = y

Separation quotient #

def uniform_space.separation_setoid (α : Type u) [uniform_space α] :

The separation relation of a uniform space seen as a setoid.

Equations

uniform_space.separation_setoid α = {r := λ (x y : α), (x, y) ∈ 𝓢 α, iseqv := _}

@[protected, instance]

def uniform_space.separation_setoid.uniform_space {α : Type u} [u : uniform_space α] :

uniform_space (quotient (uniform_space.separation_setoid α))

Equations

uniform_space.separation_setoid.uniform_space = {to_topological_space := topological_space.coinduced (λ (x : α), ⟦x⟧) uniform_space.to_topological_space, to_core := {uniformity := filter.map (λ (p : α × α), (⟦p.fst ⟧, ⟦p.snd ⟧)) uniform_space.to_core.uniformity, refl := _, symm := _, comp := _}, is_open_uniformity := _}

theorem uniform_space.uniformity_quotient {α : Type u} [uniform_space α] :

𝓤 (quotient (uniform_space.separation_setoid α)) = filter.map (λ (p : α × α), (⟦p.fst ⟧, ⟦p.snd ⟧)) (𝓤 α)

theorem uniform_space.uniform_continuous_quotient_mk {α : Type u} [uniform_space α] :

uniform_continuous quotient.mk

theorem uniform_space.uniform_continuous_quotient {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : quotient (uniform_space.separation_setoid α) → β} (hf : uniform_continuous (λ (x : α), f ⟦x⟧)) :

uniform_continuous f

theorem uniform_space.uniform_continuous_quotient_lift {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : α → β} {h : ∀ (a b : α), (a, b) ∈ 𝓢 α → f a = f b} (hf : uniform_continuous f) :

uniform_continuous (λ (a : quotient (uniform_space.separation_setoid α)), quotient.lift f h a)

theorem uniform_space.uniform_continuous_quotient_lift₂ {α : Type u} {β : Type v} {γ : Type w} [uniform_space α] [uniform_space β] [uniform_space γ] {f : α → β → γ} {h : ∀ (a : α) (c : β) (b : α) (d : β), (a, b) ∈ 𝓢 α → (c, d) ∈ 𝓢 β → f a c = f b d} (hf : uniform_continuous (λ (p : α × β), f p.fst p.snd)) :

uniform_continuous (λ (p : quotient (uniform_space.separation_setoid α) × quotient (uniform_space.separation_setoid β)), quotient.lift₂ f h p.fst p.snd)

theorem uniform_space.comap_quotient_le_uniformity {α : Type u} [uniform_space α] :

filter.comap (λ (p : α × α), (⟦p.fst ⟧, ⟦p.snd ⟧)) (𝓤 (quotient (uniform_space.separation_setoid α))) ≤ 𝓤 α

theorem uniform_space.comap_quotient_eq_uniformity {α : Type u} [uniform_space α] :

filter.comap (λ (p : α × α), (⟦p.fst ⟧, ⟦p.snd ⟧)) (𝓤 (quotient (uniform_space.separation_setoid α))) = 𝓤 α

@[protected, instance]

def uniform_space.separated_separation {α : Type u} [uniform_space α] :

separated_space (quotient (uniform_space.separation_setoid α))

theorem uniform_space.separated_of_uniform_continuous {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : α → β} {x y : α} (H : uniform_continuous f) (h : x ≈ y) :

f x ≈ f y

theorem uniform_space.eq_of_separated_of_uniform_continuous {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] [separated_space β] {f : α → β} {x y : α} (H : uniform_continuous f) (h : x ≈ y) :

f x = f y

theorem is_separated.eq_of_uniform_continuous {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : α → β} {x y : α} {s : set β} (hs : is_separated s) (hxs : f x ∈ s) (hys : f y ∈ s) (H : uniform_continuous f) (h : x ≈ y) :

f x = f y

def uniform_space.separation_quotient (α : Type u_1) [uniform_space α] :

Type u_1

The maximal separated quotient of a uniform space α.

Equations

uniform_space.separation_quotient α = quotient (uniform_space.separation_setoid α)

@[protected, instance]

def uniform_space.separation_quotient.uniform_space {α : Type u} [uniform_space α] :

uniform_space (uniform_space.separation_quotient α)

Equations

uniform_space.separation_quotient.uniform_space = uniform_space.separation_setoid.uniform_space

@[protected, instance]

def uniform_space.separation_quotient.separated_space {α : Type u} [uniform_space α] :

separated_space (uniform_space.separation_quotient α)

@[protected, instance]

def uniform_space.separation_quotient.inhabited {α : Type u} [uniform_space α] [inhabited α] :

inhabited (uniform_space.separation_quotient α)

Equations

uniform_space.separation_quotient.inhabited = quotient.inhabited (uniform_space.separation_setoid α)

noncomputable def uniform_space.separation_quotient.lift {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] [separated_space β] (f : α → β) :

uniform_space.separation_quotient α → β

Factoring functions to a separated space through the separation quotient.

Equations

uniform_space.separation_quotient.lift f = dite (uniform_continuous f) (λ (h : uniform_continuous f), quotient.lift f _) (λ (h : ¬uniform_continuous f) (x : uniform_space.separation_quotient α), f _.some)

theorem uniform_space.separation_quotient.lift_mk {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] [separated_space β] {f : α → β} (h : uniform_continuous f) (a : α) :

uniform_space.separation_quotient.lift f ⟦a⟧ = f a

theorem uniform_space.separation_quotient.uniform_continuous_lift {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] [separated_space β] (f : α → β) :

uniform_continuous (uniform_space.separation_quotient.lift f)

noncomputable def uniform_space.separation_quotient.map {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] (f : α → β) :

uniform_space.separation_quotient α → uniform_space.separation_quotient β

The separation quotient functor acting on functions.

Equations

uniform_space.separation_quotient.map f = uniform_space.separation_quotient.lift (quotient.mk ∘ f)

theorem uniform_space.separation_quotient.map_mk {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : α → β} (h : uniform_continuous f) (a : α) :

uniform_space.separation_quotient.map f ⟦a⟧ = ⟦f a⟧

theorem uniform_space.separation_quotient.uniform_continuous_map {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] (f : α → β) :

uniform_continuous (uniform_space.separation_quotient.map f)

theorem uniform_space.separation_quotient.map_unique {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : α → β} (hf : uniform_continuous f) {g : uniform_space.separation_quotient α → uniform_space.separation_quotient β} (comm : quotient.mk ∘ f = g ∘ quotient.mk) :

uniform_space.separation_quotient.map f = g

theorem uniform_space.separation_quotient.map_id {α : Type u} [uniform_space α] :

uniform_space.separation_quotient.map id = id

theorem uniform_space.separation_quotient.map_comp {α : Type u} {β : Type v} {γ : Type w} [uniform_space α] [uniform_space β] [uniform_space γ] {f : α → β} {g : β → γ} (hf : uniform_continuous f) (hg : uniform_continuous g) :

uniform_space.separation_quotient.map g ∘ uniform_space.separation_quotient.map f = uniform_space.separation_quotient.map (g ∘ f)

theorem uniform_space.separation_prod {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {a₁ a₂ : α} {b₁ b₂ : β} :

(a₁, b₁) ≈ (a₂, b₂) ↔ a₁ ≈ a₂ ∧ b₁ ≈ b₂

@[protected, instance]

def uniform_space.separated.prod {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] [separated_space α] [separated_space β] :

separated_space (α × β)

theorem is_separated.prod {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {s : set α} {t : set β} (hs : is_separated s) (ht : is_separated t) :

is_separated (s ×ˢ t)