Hausdorff properties of uniform spaces. Separation quotient.

Two points of a topological space are called Inseparable, if their neighborhoods filter are equal. Equivalently, Inseparable x y means that any open set that contains x must contain y and vice versa.

In a uniform space, points x and y are inseparable if and only if (x, y) belongs to all entourages, see inseparable_iff_ker_uniformity.

A uniform space is a regular topological space, hence separation axioms T0Space, T1Space, T2Space, and T3Space are equivalent for uniform spaces, and Lean typeclass search can automatically convert from one assumption to another. We say that a uniform space is separated, if it satisfies these axioms. If you need an Iff statement (e.g., to rewrite), then see R1Space.t0Space_iff_t2Space and RegularSpace.t0Space_iff_t3Space.

In this file we prove several facts that relate Inseparable and Specializes to the uniformity filter. Most of them are simple corollaries of Filter.HasBasis.inseparable_iff_uniformity for different filter bases of 𝓤 α.

Then we study the Kolmogorov quotient SeparationQuotient X of a uniform space. For a general topological space, this quotient is defined as the quotient by Inseparable equivalence relation. It is the maximal T₀ quotient of a topological space.

In case of a uniform space, we equip this quotient with a UniformSpace structure that agrees with the quotient topology. We also prove that the quotient map induces uniformity on the original space.

Finally, we turn SeparationQuotient into a functor (not in terms of CategoryTheory.Functor to avoid extra imports) by defining SeparationQuotient.lift' and SeparationQuotient.map operations.

Main definitions

• SeparationQuotient.instUniformSpace: uniform space structure on SeparationQuotient α, where α is a uniform space;

• SeparationQuotient.lift': given a map f : α → β from a uniform space to a separated uniform space, lift it to a map SeparationQuotient α → β; if the original map is not uniformly continuous, then returns a constant map.

• SeparationQuotient.map: given a map f : α → β between uniform spaces, returns a map SeparationQuotient α → SeparationQuotient β. If the original map is not uniformly continuous, then returns a constant map. Otherwise, SeparationQuotient.map f (SeparationQuotient.mk x) = SeparationQuotient.mk (f x).

Main results

• SeparationQuotient.uniformity_eq: the uniformity filter on SeparationQuotient α is the push forward of the uniformity filter on α.
• SeparationQuotient.comap_mk_uniformity: the quotient map α → SeparationQuotient α induces uniform space structure on the original space.
• SeparationQuotient.uniformContinuous_lift': factoring a uniformly continuous map through the separation quotient gives a uniformly continuous map.
• SeparationQuotient.uniformContinuous_map: maps induced between separation quotients are uniformly continuous.

Implementation notes

This files used to contain definitions of separationRel α and UniformSpace.SeparationQuotient α. These definitions were equal (but not definitionally equal) to {x : α × α | Inseparable x.1 x.2} and SeparationQuotient α, respectively, and were added to the library before their geneeralizations to topological spaces.

In #10644, we migrated from these definitions to more general Inseparable and SeparationQuotient.

TODO

Definitions SeparationQuotient.lift' and SeparationQuotient.map rely on UniformSpace structures in the domain and in the codomain. We should generalize them to topological spaces. This generalization will drop UniformContinuous assumptions in some lemmas, and add these assumptions in other lemmas, so it was not done in #10644 to keep it reasonably sized.

Keywords

uniform space, separated space, Hausdorff space, separation quotient

Separated uniform spaces

@[instance 100]

instance UniformSpace.to_regularSpace {α : Type u} [UniformSpace α] : RegularSpace α

Equations

• ⋯ = ⋯

theorem Filter.HasBasis.specializes_iff_uniformity {α : Type u} [UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)} (h : (uniformity α).HasBasis p s) {x : α} {y : α} : x ⤳ y ↔ ∀ (i : ι), p i → (x, y) ∈ s i

theorem Filter.HasBasis.inseparable_iff_uniformity {α : Type u} [UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)} (h : (uniformity α).HasBasis p s) {x : α} {y : α} : Inseparable x y ↔ ∀ (i : ι), p i → (x, y) ∈ s i

theorem inseparable_iff_ker_uniformity {α : Type u} [UniformSpace α] {x : α} {y : α} : Inseparable x y ↔ (x, y) ∈ (uniformity α).ker

theorem Inseparable.nhds_le_uniformity {α : Type u} [UniformSpace α] {x : α} {y : α} (h : Inseparable x y) : nhds (x, y) ≤ uniformity α

theorem inseparable_iff_clusterPt_uniformity {α : Type u} [UniformSpace α] {x : α} {y : α} : Inseparable x y ↔ ClusterPt (x, y) (uniformity α)

theorem t0Space_iff_uniformity {α : Type u} [UniformSpace α] : T0Space α ↔ ∀ (x y : α), (∀ r ∈ uniformity α, (x, y) ∈ r) → x = y

theorem t0Space_iff_uniformity' {α : Type u} [UniformSpace α] : T0Space α ↔ Pairwise fun (x y : α) => ∃ r ∈ uniformity α, (x, y) ∉ r

theorem t0Space_iff_ker_uniformity {α : Type u} [UniformSpace α] : T0Space α ↔ (uniformity α).ker = Set.diagonal α

theorem eq_of_uniformity {α : Type u_1} [UniformSpace α] [T0Space α] {x : α} {y : α} (h : ∀ {V : Set (α × α)}, V ∈ uniformity α → (x, y) ∈ V) : x = y

theorem eq_of_uniformity_basis {α : Type u_1} [UniformSpace α] [T0Space α] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set (α × α)} (hs : (uniformity α).HasBasis p s) {x : α} {y : α} (h : ∀ {i : ι}, p i → (x, y) ∈ s i) : x = y

theorem eq_of_forall_symmetric {α : Type u_1} [UniformSpace α] [T0Space α] {x : α} {y : α} (h : ∀ {V : Set (α × α)}, V ∈ uniformity α → SymmetricRel V → (x, y) ∈ V) : x = y

theorem eq_of_clusterPt_uniformity {α : Type u} [UniformSpace α] [T0Space α] {x : α} {y : α} (h : ClusterPt (x, y) (uniformity α)) : x = y

theorem Filter.Tendsto.inseparable_iff_uniformity {α : Type u} [UniformSpace α] {β : Type u_1} {l : Filter β} [l.NeBot] {f : β → α} {g : β → α} {a : α} {b : α} (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) : Inseparable a b ↔ Filter.Tendsto (fun (x : β) => (f x, g x)) l (uniformity α)

theorem isClosed_of_spaced_out {α : Type u} [UniformSpace α] [T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ uniformity α) {s : Set α} (hs : s.Pairwise fun (x y : α) => (x, y) ∉ V₀) : IsClosed s

theorem isClosed_range_of_spaced_out {α : Type u} [UniformSpace α] {ι : Type u_1} [T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ uniformity α) {f : ι → α} (hf : Pairwise fun (x y : ι) => (f x, f y) ∉ V₀) : IsClosed (Set.range f)

Separation quotient

theorem SeparationQuotient.comap_map_mk_uniformity {α : Type u} [UniformSpace α] : Filter.comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity α)) = uniformity α

instance SeparationQuotient.instUniformSpace {α : Type u} [UniformSpace α] : UniformSpace (SeparationQuotient α)

Equations

• SeparationQuotient.instUniformSpace = UniformSpace.mk (Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity α)) ⋯ ⋯ ⋯

theorem SeparationQuotient.uniformity_eq {α : Type u} [UniformSpace α] : uniformity (SeparationQuotient α) = Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity α)

theorem SeparationQuotient.uniformContinuous_mk {α : Type u} [UniformSpace α] : UniformContinuous SeparationQuotient.mk

theorem SeparationQuotient.uniformContinuous_dom {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : SeparationQuotient α → β} : UniformContinuous f ↔ UniformContinuous (f ∘ SeparationQuotient.mk)

theorem SeparationQuotient.uniformContinuous_dom₂ {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : SeparationQuotient α × SeparationQuotient β → γ} : UniformContinuous f ↔ UniformContinuous fun (p : α × β) => f (SeparationQuotient.mk p.1, SeparationQuotient.mk p.2)

theorem SeparationQuotient.uniformContinuous_lift {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : α → β} (h : ∀ (a b : α), Inseparable a b → f a = f b) : UniformContinuous (SeparationQuotient.lift f h) ↔ UniformContinuous f

theorem SeparationQuotient.uniformContinuous_uncurry_lift₂ {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α → β → γ} (h : ∀ (a : α) (c : β) (b : α) (d : β), Inseparable a b → Inseparable c d → f a c = f b d) : UniformContinuous (Function.uncurry (SeparationQuotient.lift₂ f h)) ↔ UniformContinuous (Function.uncurry f)

theorem SeparationQuotient.comap_mk_uniformity {α : Type u} [UniformSpace α] : Filter.comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity (SeparationQuotient α)) = uniformity α

def SeparationQuotient.lift' {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [T0Space β] (f : α → β) : SeparationQuotient α → β

Factoring functions to a separated space through the separation quotient.

TODO: unify with SeparationQuotient.lift.

Equations

• SeparationQuotient.lift' f = if hc : UniformContinuous f then SeparationQuotient.lift f ⋯ else fun (x : SeparationQuotient α) => f ⋯.some

theorem SeparationQuotient.lift'_mk {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [T0Space β] {f : α → β} (h : UniformContinuous f) (a : α) : SeparationQuotient.lift' f (SeparationQuotient.mk a) = f a

theorem SeparationQuotient.uniformContinuous_lift' {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [T0Space β] (f : α → β) : UniformContinuous (SeparationQuotient.lift' f)

def SeparationQuotient.map {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] (f : α → β) : SeparationQuotient α → SeparationQuotient β

The separation quotient functor acting on functions.

Equations

• SeparationQuotient.map f = SeparationQuotient.lift' (SeparationQuotient.mk ∘ f)

theorem SeparationQuotient.map_mk {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : α → β} (h : UniformContinuous f) (a : α) : SeparationQuotient.map f (SeparationQuotient.mk a) = SeparationQuotient.mk (f a)

theorem SeparationQuotient.uniformContinuous_map {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] (f : α → β) : UniformContinuous (SeparationQuotient.map f)

theorem SeparationQuotient.map_unique {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : α → β} (hf : UniformContinuous f) {g : SeparationQuotient α → SeparationQuotient β} (comm : SeparationQuotient.mk ∘ f = g ∘ SeparationQuotient.mk) : SeparationQuotient.map f = g

@[simp]

theorem SeparationQuotient.map_id {α : Type u} [UniformSpace α] : SeparationQuotient.map id = id

theorem SeparationQuotient.map_comp {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α → β} {g : β → γ} (hf : UniformContinuous f) (hg : UniformContinuous g) : SeparationQuotient.map g ∘ SeparationQuotient.map f = SeparationQuotient.map (g ∘ f)