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 operations.

Main definitions #

Main results #

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.


Definitions SeparationQuotient.lift' and 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]
  • =
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 : α} :
theorem t0Space_iff_uniformity {α : Type u} [UniformSpace α] :
T0Space α ∀ (x y : α), (runiformity α, (x, y) r)x = y
theorem t0Space_iff_uniformity' {α : Type u} [UniformSpace α] :
T0Space α Pairwise fun (x y : α) => runiformity α, (x, y)r
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} {β : Type v} [UniformSpace α] {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₀) :
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₀) :

Separation quotient #

theorem SeparationQuotient.comap_map_mk_uniformity {α : Type u} [UniformSpace α] :
Filter.comap ( ( ( (uniformity α)) = uniformity α
theorem SeparationQuotient.uniformity_eq {α : Type u} [UniformSpace α] :
uniformity (SeparationQuotient α) = ( (uniformity α)
theorem SeparationQuotient.uniformContinuous_lift {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : αβ} (h : ∀ (a b : α), Inseparable a bf a = f b) :
theorem SeparationQuotient.uniformContinuous_uncurry_lift₂ {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : αβγ} (h : ∀ (a : α) (c : β) (b : α) (d : β), Inseparable a bInseparable c df a c = f b d) :
theorem SeparationQuotient.comap_mk_uniformity {α : Type u} [UniformSpace α] :
Filter.comap ( (uniformity (SeparationQuotient α)) = uniformity α
def SeparationQuotient.lift' {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [T0Space β] (f : αβ) :

Factoring functions to a separated space through the separation quotient.

TODO: unify with SeparationQuotient.lift.

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

    The separation quotient functor acting on functions.

    Instances For
      theorem SeparationQuotient.map_unique {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : αβ} (hf : UniformContinuous f) {g : SeparationQuotient αSeparationQuotient β} (comm : f = g :