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 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 SeparationQuotient 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 SeparationQuotient X. As usual, this allows to turn SeparationQuotient 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

• separationRel X : Set (X × X): the separation relation
• SeparatedSpace X: a predicate class asserting that X is separated
• SeparationQuotient X: the maximal separated quotient of X.
• SeparationQuotient.lift f: factors a map f : X → Y through the separation quotient of X.
• SeparationQuotient.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.
• 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.

## Notations

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

Implementation notes

The separation setoid separationSetoid is not declared as a global instance. It is made a local instance while building the theory of SeparationQuotient. The factored map SeparationQuotient.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

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

Equations

• (_ : RegularSpace α) = (_ : RegularSpace α)

def separationRel (α : Type u) [UniformSpace α] : 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

• separationRel α = Filter.ker (uniformity α)

def Uniformity.term𝓢 : Lean.ParserDescr

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

• Uniformity.term𝓢 = Lean.ParserDescr.node `Uniformity.term𝓢 1024 (Lean.ParserDescr.symbol "𝓢")

theorem separated_equiv {α : Type u} [UniformSpace α] : Equivalence fun (x y : α) => (x, y) ∈ separationRel α

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

theorem separationRel_iff_specializes {α : Type u} [UniformSpace α] {a : α} {b : α} : (a, b) ∈ separationRel α ↔ a ⤳ b

theorem separationRel_iff_inseparable {α : Type u} [UniformSpace α] {a : α} {b : α} : (a, b) ∈ separationRel α ↔ Inseparable a b

class SeparatedSpace (α : Type u) [UniformSpace α] : Prop

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

• out : separationRel α = idRel

  The separation relation is equal to the diagonal idRel.

theorem separatedSpace_iff {α : Type u} [UniformSpace α] : SeparatedSpace α ↔ separationRel α = idRel

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

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

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

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

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

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

theorem idRel_sub_separationRel (α : Type u_1) [UniformSpace α] : idRel ⊆ separationRel α

theorem separationRel_comap {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : α → β} (h : inst✝¹ = UniformSpace.comap f inst✝) : separationRel α = Prod.map f f ⁻¹' separationRel β

theorem Filter.HasBasis.separationRel {α : Type u} [UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)} (h : Filter.HasBasis (uniformity α) p s) : separationRel α = ⋂ (i : ι), ⋂ (_ : p i), s i

theorem separationRel_eq_inter_closure {α : Type u} [UniformSpace α] : separationRel α = ⋂₀ (closure '' (uniformity α).sets)

theorem isClosed_separationRel {α : Type u} [UniformSpace α] : IsClosed (separationRel α)

theorem separated_iff_t2 {α : Type u} [UniformSpace α] : SeparatedSpace α ↔ T2Space α

instance separated_t3 {α : Type u} [UniformSpace α] [SeparatedSpace α] : T3Space α

Equations

• (_ : T3Space α) = (_ : T3Space α)

instance Subtype.separatedSpace {α : Type u} [UniformSpace α] [SeparatedSpace α] (s : Set α) : SeparatedSpace ↑s

Equations

• (_ : SeparatedSpace ↑s) = (_ : SeparatedSpace ↑s)

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

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

Separation quotient

def UniformSpace.separationSetoid (α : Type u) [UniformSpace α] : Setoid α

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

Equations

• UniformSpace.separationSetoid α = { r := fun (x y : α) => (x, y) ∈ separationRel α, iseqv := (_ : Equivalence fun (x y : α) => (x, y) ∈ separationRel α) }

instance UniformSpace.separationSetoid.uniformSpace {α : Type u} [UniformSpace α] : UniformSpace (Quotient (UniformSpace.separationSetoid α))

Equations

• One or more equations did not get rendered due to their size.

theorem UniformSpace.uniformity_quotient {α : Type u} [UniformSpace α] : uniformity (Quotient (UniformSpace.separationSetoid α)) = Filter.map (fun (p : α × α) => (⟦p.1⟧, ⟦p.2⟧)) (uniformity α)

theorem UniformSpace.uniformContinuous_quotient_mk' {α : Type u} [UniformSpace α] : UniformContinuous Quotient.mk'

theorem UniformSpace.uniformContinuous_quotient_mk {α : Type u} [UniformSpace α] : UniformContinuous (Quotient.mk (UniformSpace.separationSetoid α))

theorem UniformSpace.uniformContinuous_quotient {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : Quotient (UniformSpace.separationSetoid α) → β} (hf : UniformContinuous fun (x : α) => f ⟦x⟧) : UniformContinuous f

theorem UniformSpace.uniformContinuous_quotient_lift {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : α → β} {h : ∀ (a b : α), (a, b) ∈ separationRel α → f a = f b} (hf : UniformContinuous f) : UniformContinuous fun (a : Quotient (UniformSpace.separationSetoid α)) => Quotient.lift f h a

theorem UniformSpace.uniformContinuous_quotient_lift₂ {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α → β → γ} {h : ∀ (a : α) (c : β) (b : α) (d : β), (a, b) ∈ separationRel α → (c, d) ∈ separationRel β → f a c = f b d} (hf : UniformContinuous fun (p : α × β) => f p.1 p.2) : UniformContinuous fun (p : Quotient (UniformSpace.separationSetoid α) × Quotient (UniformSpace.separationSetoid β)) => Quotient.lift₂ f h p.1 p.2

theorem UniformSpace.comap_quotient_le_uniformity {α : Type u} [UniformSpace α] : Filter.comap (fun (p : α × α) => (⟦p.1⟧, ⟦p.2⟧)) (uniformity (Quotient (UniformSpace.separationSetoid α))) ≤ uniformity α

theorem UniformSpace.comap_quotient_eq_uniformity {α : Type u} [UniformSpace α] : Filter.comap (fun (p : α × α) => (⟦p.1⟧, ⟦p.2⟧)) (uniformity (Quotient (UniformSpace.separationSetoid α))) = uniformity α

instance UniformSpace.separated_separation {α : Type u} [UniformSpace α] : SeparatedSpace (Quotient (UniformSpace.separationSetoid α))

Equations

• (_ : SeparatedSpace (Quotient (UniformSpace.separationSetoid α))) = (_ : SeparatedSpace (Quotient (UniformSpace.separationSetoid α)))

theorem UniformSpace.separated_of_uniformContinuous {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : α → β} {x : α} {y : α} (H : UniformContinuous f) (h : x ≈ y) : f x ≈ f y

theorem UniformSpace.eq_of_separated_of_uniformContinuous {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [SeparatedSpace β] {f : α → β} {x : α} {y : α} (H : UniformContinuous f) (h : x ≈ y) : f x = f y

def UniformSpace.SeparationQuotient (α : Type u_1) [UniformSpace α] : Type u_1

The maximal separated quotient of a uniform space α.

Equations

• UniformSpace.SeparationQuotient α = Quotient (UniformSpace.separationSetoid α)

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

Equations

• UniformSpace.SeparationQuotient.instUniformSpaceSeparationQuotient = UniformSpace.separationSetoid.uniformSpace

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

Equations

• (_ : SeparatedSpace (UniformSpace.SeparationQuotient α)) = (_ : SeparatedSpace (Quotient (UniformSpace.separationSetoid α)))

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

Equations

• UniformSpace.SeparationQuotient.instInhabitedSeparationQuotient = inferInstanceAs (Inhabited (Quotient (UniformSpace.separationSetoid α)))

theorem UniformSpace.SeparationQuotient.mk_eq_mk {α : Type u} [UniformSpace α] {x : α} {y : α} : ⟦x⟧ = ⟦y⟧ ↔ Inseparable x y

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

Factoring functions to a separated space through the separation quotient.

Equations

• One or more equations did not get rendered due to their size.

theorem UniformSpace.SeparationQuotient.lift_mk {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [SeparatedSpace β] {f : α → β} (h : UniformContinuous f) (a : α) : UniformSpace.SeparationQuotient.lift f ⟦a⟧ = f a

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

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

The separation quotient functor acting on functions.

Equations

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

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

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

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

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

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

theorem UniformSpace.separation_prod {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} : (a₁, b₁) ≈ (a₂, b₂) ↔ a₁ ≈ a₂ ∧ b₁ ≈ b₂

instance UniformSpace.Separated.prod {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] [SeparatedSpace α] [SeparatedSpace β] : SeparatedSpace (α × β)

Equations

• (_ : SeparatedSpace (α × β)) = (_ : SeparatedSpace (α × β))