doc-next-gen

Mathlib.Topology.UniformSpace.Separation

Module docstring

{"# 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 https://github.com/leanprover-community/mathlib4/pull/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 https://github.com/leanprover-community/mathlib4/pull/10644 to keep it reasonably sized.

Keywords

uniform space, separated space, Hausdorff space, separation quotient ","### Separated uniform spaces ","### Separation quotient "}

Filter.HasBasis.specializes_iff_uniformity theorem
{ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) {x y : α} : x ⤳ y ↔ ∀ i, p i → (x, y) ∈ s i
Full source 
theorem Filter.HasBasis.specializes_iff_uniformity {ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)}
    (h : (𝓤 α).HasBasis p s) {x y : α} : x ⤳ yx ⤳ y ↔ ∀ i, p i → (x, y) ∈ s i :=
  (nhds_basis_uniformity h).specializes_iff
Specialization Relation Characterization via Uniformity Basis
Informal description
Let $\alpha$ be a uniform space with a uniformity filter $\mathfrak{U}(\alpha)$ that has a basis $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. For any two points $x, y \in \alpha$, the specialization relation $x \rightsquigarrow y$ holds if and only if for every index $i$, whenever $p(i)$ is true, the pair $(x, y)$ belongs to the set $s_i$.
Filter.HasBasis.inseparable_iff_uniformity theorem
{ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) {x y : α} : Inseparable x y ↔ ∀ i, p i → (x, y) ∈ s i
Full source 
theorem Filter.HasBasis.inseparable_iff_uniformity {ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)}
    (h : (𝓤 α).HasBasis p s) {x y : α} : InseparableInseparable x y ↔ ∀ i, p i → (x, y) ∈ s i :=
  specializes_iff_inseparable.symm.trans h.specializes_iff_uniformity
Characterization of inseparable points via uniformity basis
Informal description
Let $\alpha$ be a uniform space with a basis $\{s_i\}_{i \in \iota}$ for its uniformity filter $\mathfrak{U}(\alpha)$, indexed by a type $\iota$ with a predicate $p : \iota \to \mathrm{Prop}$. For any two points $x, y \in \alpha$, the following are equivalent: 1. $x$ and $y$ are topologically inseparable (i.e., they have the same neighborhood filter); 2. For every index $i$, if $p(i)$ holds, then $(x, y) \in s_i$.
inseparable_iff_ker_uniformity theorem
{x y : α} : Inseparable x y ↔ (x, y) ∈ (𝓤 α).ker
Full source 
theorem inseparable_iff_ker_uniformity {x y : α} : InseparableInseparable x y ↔ (x, y) ∈ (𝓤 α).ker :=
  (𝓤 α).basis_sets.inseparable_iff_uniformity
Characterization of inseparable points via uniformity kernel
Informal description
For any two points $x$ and $y$ in a uniform space $\alpha$, the following are equivalent: 1. $x$ and $y$ are topologically inseparable (i.e., they have the same neighborhood filters); 2. The pair $(x, y)$ belongs to the kernel of the uniformity filter $\mathfrak{U}(\alpha)$, meaning $(x, y)$ is contained in every entourage of the uniformity.
Inseparable.nhds_le_uniformity theorem
{x y : α} (h : Inseparable x y) : 𝓝 (x, y) ≤ 𝓤 α
Full source 
protected theorem Inseparable.nhds_le_uniformity {x y : α} (h : Inseparable x y) :
    𝓝 (x, y) ≤ 𝓤 α := by
  rw [h.prod rfl]
  apply nhds_le_uniformity
Neighborhood Filter of Inseparable Points is Contained in Uniformity Filter
Informal description
For any two points $x$ and $y$ in a uniform space $\alpha$, if $x$ and $y$ are inseparable (i.e., they cannot be separated by any open set), then the neighborhood filter of the pair $(x, y)$ is contained in the uniformity filter of $\alpha$. In other words, $\mathcal{N}(x, y) \leq \mathcal{U}(\alpha)$.
inseparable_iff_clusterPt_uniformity theorem
{x y : α} : Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)
Full source 
theorem inseparable_iff_clusterPt_uniformity {x y : α} :
    InseparableInseparable x y ↔ ClusterPt (x, y) (𝓤 α) := by
  refine ⟨fun h ↦ .of_nhds_le h.nhds_le_uniformity, fun h ↦ ?_⟩
  simp_rw [uniformity_hasBasis_closed.inseparable_iff_uniformity, isClosed_iff_clusterPt]
  exact fun U ⟨hU, hUc⟩ ↦ hUc _ <| h.mono <| le_principal_iff.2 hU
Characterization of Inseparable Points via Uniformity Cluster Points
Informal description
For any two points $x$ and $y$ in a uniform space $\alpha$, the following are equivalent: 1. $x$ and $y$ are inseparable (i.e., they cannot be separated by any open set); 2. The pair $(x, y)$ is a cluster point of the uniformity filter $\mathcal{U}(\alpha)$.
t0Space_iff_uniformity theorem
: T0Space α ↔ ∀ x y, (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y
Full source 
theorem t0Space_iff_uniformity :
    T0SpaceT0Space α ↔ ∀ x y, (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y := by
  simp only [t0Space_iff_inseparable, inseparable_iff_ker_uniformity, mem_ker, id]
Characterization of $T_0$ Uniform Spaces via Uniformity Filter
Informal description
A uniform space $\alpha$ is a $T_0$ space if and only if for any two points $x, y \in \alpha$, whenever $(x, y)$ belongs to every entourage in the uniformity $\mathcal{U}(\alpha)$, then $x = y$.
t0Space_iff_uniformity' theorem
: T0Space α ↔ Pairwise fun x y ↦ ∃ r ∈ 𝓤 α, (x, y) ∉ r
Full source 
theorem t0Space_iff_uniformity' :
    T0SpaceT0Space α ↔ Pairwise fun x y ↦ ∃ r ∈ 𝓤 α, (x, y) ∉ r := by
  simp [t0Space_iff_not_inseparable, inseparable_iff_ker_uniformity]
Characterization of $T_0$ Uniform Spaces via Entourage Separation
Informal description
A uniform space $\alpha$ is a $T_0$ space if and only if for every pair of distinct points $x, y \in \alpha$, there exists an entourage $r$ in the uniformity $\mathcal{U}(\alpha)$ such that $(x, y) \notin r$.
t0Space_iff_ker_uniformity theorem
: T0Space α ↔ (𝓤 α).ker = diagonal α
Full source 
theorem t0Space_iff_ker_uniformity : T0SpaceT0Space α ↔ (𝓤 α).ker = diagonal α := by
  simp_rw [t0Space_iff_uniformity, subset_antisymm_iff, diagonal_subset_iff, subset_def,
    Prod.forall, Filter.mem_ker, mem_diagonal_iff, iff_self_and]
  exact fun _ x s hs ↦ refl_mem_uniformity hs
Characterization of $T_0$ Uniform Spaces via Uniformity Kernel
Informal description
A uniform space $\alpha$ is a $T_0$ space if and only if the kernel of its uniformity filter $\mathcal{U}(\alpha)$ equals the diagonal $\{(x,x) | x \in \alpha\}$ of $\alpha \times \alpha$.
Filter.Tendsto.inseparable_iff_uniformity theorem
{β} {l : Filter β} [NeBot l] {f g : β → α} {a b : α} (ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b)) : Inseparable a b ↔ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)
Full source 
theorem Filter.Tendsto.inseparable_iff_uniformity {β} {l : Filter β} [NeBot l] {f g : β → α}
    {a b : α} (ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b)) :
    InseparableInseparable a b ↔ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) := by
  refine ⟨fun h ↦ (ha.prodMk_nhds hb).mono_right h.nhds_le_uniformity, fun h ↦ ?_⟩
  rw [inseparable_iff_clusterPt_uniformity]
  exact (ClusterPt.of_le_nhds (ha.prodMk_nhds hb)).mono h
Inseparability Criterion via Uniform Convergence
Informal description
Let $\alpha$ be a uniform space, $\beta$ a type, and $l$ a non-trivial filter on $\beta$. For functions $f, g \colon \beta \to \alpha$ and points $a, b \in \alpha$ such that $f$ tends to $a$ along $l$ and $g$ tends to $b$ along $l$, the following are equivalent: 1. The points $a$ and $b$ are inseparable in $\alpha$; 2. The function $\lambda x \mapsto (f(x), g(x))$ tends to the uniformity $\mathcal{U}(\alpha)$ along $l$.
isClosed_of_spaced_out theorem
[T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ 𝓤 α) {s : Set α} (hs : s.Pairwise fun x y => (x, y) ∉ V₀) : IsClosed s
Full source 
theorem isClosed_of_spaced_out [T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ 𝓤 α) {s : Set α}
    (hs : s.Pairwise fun x y => (x, y)(x, y) ∉ V₀) : IsClosed s := by
  rcases comp_symm_mem_uniformity_sets V₀_in with ⟨V₁, V₁_in, V₁_symm, h_comp⟩
  apply isClosed_of_closure_subset
  intro x hx
  rw [mem_closure_iff_ball] at hx
  rcases hx V₁_in with ⟨y, hy, hy'⟩
  suffices x = y by rwa [this]
  apply eq_of_forall_symmetric
  intro V V_in _
  rcases hx (inter_mem V₁_in V_in) with ⟨z, hz, hz'⟩
  obtain rfl : z = y := by
    by_contra hzy
    exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball V₁_symm (ball_inter_left x _ _ hz) hy)
  exact ball_inter_right x _ _ hz
Closedness of Spaced-Out Subsets in T₀ Uniform Spaces
Informal description
Let $\alpha$ be a T₀ uniform space, and let $V_0$ be an entourage in the uniformity $\mathfrak{U}(\alpha)$. For any subset $s \subseteq \alpha$ such that for every pair of distinct points $x, y \in s$, the pair $(x, y) \notin V_0$, the subset $s$ is closed in $\alpha$.
isClosed_range_of_spaced_out theorem
{ι} [T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ 𝓤 α) {f : ι → α} (hf : Pairwise fun x y => (f x, f y) ∉ V₀) : IsClosed (range f)
Full source 
theorem isClosed_range_of_spaced_out {ι} [T0Space α] {V₀ : Set (α × α)} (V₀_in : V₀ ∈ 𝓤 α)
    {f : ι → α} (hf : Pairwise fun x y => (f x, f y)(f x, f y) ∉ V₀) : IsClosed (range f) :=
  isClosed_of_spaced_out V₀_in <| by
    rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ h
    exact hf (ne_of_apply_ne f h)
Closedness of Range for Spaced-Out Functions in T₀ Uniform Spaces
Informal description
Let $\alpha$ be a T₀ uniform space, and let $V_0$ be an entourage in the uniformity $\mathfrak{U}(\alpha)$. For any function $f \colon \iota \to \alpha$ such that for every pair of distinct indices $x, y \in \iota$, the pair $(f(x), f(y)) \notin V_0$, the range of $f$ is a closed subset of $\alpha$.
SeparationQuotient.comap_map_mk_uniformity theorem
: comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α
Full source 
theorem comap_map_mk_uniformity : comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α := by
  refine le_antisymm ?_ le_comap_map
  refine ((((𝓤 α).basis_sets.map _).comap _).le_basis_iff uniformity_hasBasis_open).2 fun U hU ↦ ?_
  refine ⟨U, hU.1, fun (x₁, x₂) ⟨(y₁, y₂), hyU, hxy⟩ ↦ ?_⟩
  simp only [Prod.map, Prod.ext_iff, mk_eq_mk] at hxy
  exact ((hxy.1.prod hxy.2).mem_open_iff hU.2).1 hyU
Uniformity Preservation Under Separation Quotient Mapping
Informal description
For a uniform space $\alpha$, the preimage under the quotient map $\text{mk} \times \text{mk} : \alpha \times \alpha \to \text{SeparationQuotient}(\alpha) \times \text{SeparationQuotient}(\alpha)$ of the pushforward of the uniformity filter $\mathcal{U}(\alpha)$ equals $\mathcal{U}(\alpha)$ itself. In other words, $\text{comap}(\text{mk} \times \text{mk})(\text{map}(\text{mk} \times \text{mk})(\mathcal{U}(\alpha))) = \mathcal{U}(\alpha)$.
SeparationQuotient.instUniformSpace instance
: UniformSpace (SeparationQuotient α)
Full source 
instance instUniformSpace : UniformSpace (SeparationQuotient α) where
  uniformity := map (Prod.map mk mk) (𝓤 α)
  symm := tendsto_map' <| tendsto_map.comp tendsto_swap_uniformity
  comp := fun t ht ↦ by
    rcases comp_open_symm_mem_uniformity_sets ht with ⟨U, hU, hUo, -, hUt⟩
    refine mem_of_superset (mem_lift' <| image_mem_map hU) ?_
    simp only [subset_def, Prod.forall, mem_compRel, mem_image, Prod.ext_iff]
    rintro _ _ ⟨_, ⟨⟨x, y⟩, hxyU, rfl, rfl⟩, ⟨⟨y', z⟩, hyzU, hy, rfl⟩⟩
    have : y' ⤳ y := (mk_eq_mk.1 hy).specializes
    exact @hUt (x, z) ⟨y', this.mem_open (UniformSpace.isOpen_ball _ hUo) hxyU, hyzU⟩
  nhds_eq_comap_uniformity := surjective_mk.forall.2 fun x ↦ comap_injective surjective_mk <| by
    conv_lhs => rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity]
    simp only [Filter.comap_comap, Function.comp_def, Prod.map_apply]
Uniform Space Structure on Separation Quotient
Informal description
The separation quotient $\text{SeparationQuotient}(\alpha)$ of a uniform space $\alpha$ carries a natural uniform space structure induced by the original uniformity on $\alpha$. This structure is defined such that the quotient map $\alpha \to \text{SeparationQuotient}(\alpha)$ is uniformly continuous, and the uniformity on the quotient is the pushforward of the original uniformity along this map.
SeparationQuotient.uniformity_eq theorem
: 𝓤 (SeparationQuotient α) = (𝓤 α).map (Prod.map mk mk)
Full source 
theorem uniformity_eq : 𝓤 (SeparationQuotient α) = (𝓤 α).map (Prod.map mk mk) := rfl
Uniformity of Separation Quotient as Pushforward of Original Uniformity
Informal description
The uniformity filter on the separation quotient $\text{SeparationQuotient}(\alpha)$ is equal to the image of the uniformity filter $\mathcal{U}(\alpha)$ under the product map $\text{mk} \times \text{mk} : \alpha \times \alpha \to \text{SeparationQuotient}(\alpha) \times \text{SeparationQuotient}(\alpha)$. In other words, $\mathcal{U}(\text{SeparationQuotient}(\alpha)) = (\text{mk} \times \text{mk})_* \mathcal{U}(\alpha)$.
SeparationQuotient.uniformContinuous_mk theorem
: UniformContinuous (mk : α → SeparationQuotient α)
Full source 
theorem uniformContinuous_mk : UniformContinuous (mk : α → SeparationQuotient α) :=
  le_rfl
Uniform Continuity of the Separation Quotient Map
Informal description
The quotient map $\operatorname{mk} : \alpha \to \operatorname{SeparationQuotient}(\alpha)$ from a uniform space to its separation quotient is uniformly continuous.
SeparationQuotient.uniformContinuous_dom theorem
{f : SeparationQuotient α → β} : UniformContinuous f ↔ UniformContinuous (f ∘ mk)
Full source 
theorem uniformContinuous_dom {f : SeparationQuotient α → β} :
    UniformContinuousUniformContinuous f ↔ UniformContinuous (f ∘ mk) :=
  .rfl
Uniform Continuity of Functions on Separation Quotient via Lifting
Informal description
For a function $f$ from the separation quotient $\text{SeparationQuotient}(\alpha)$ to a uniform space $\beta$, $f$ is uniformly continuous if and only if the composition $f \circ \text{mk}$ is uniformly continuous, where $\text{mk} : \alpha \to \text{SeparationQuotient}(\alpha)$ is the canonical quotient map.
SeparationQuotient.uniformContinuous_dom₂ theorem
{f : SeparationQuotient α × SeparationQuotient β → γ} : UniformContinuous f ↔ UniformContinuous fun p : α × β ↦ f (mk p.1, mk p.2)
Full source 
theorem uniformContinuous_dom₂ {f : SeparationQuotientSeparationQuotient α × SeparationQuotient β → γ} :
    UniformContinuousUniformContinuous f ↔ UniformContinuous fun p : α × β ↦ f (mk p.1, mk p.2) := by
  simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq, prod_map_map_eq,
    tendsto_map'_iff]
  rfl
Uniform Continuity Criterion for Bivariate Functions on Separation Quotients
Informal description
For a function $f \colon \text{SeparationQuotient}(\alpha) \times \text{SeparationQuotient}(\beta) \to \gamma$ between uniform spaces, $f$ is uniformly continuous if and only if the function $(x,y) \mapsto f(\text{mk}(x), \text{mk}(y))$ is uniformly continuous on $\alpha \times \beta$, where $\text{mk} \colon \alpha \to \text{SeparationQuotient}(\alpha)$ and $\text{mk} \colon \beta \to \text{SeparationQuotient}(\beta)$ are the canonical quotient maps.
SeparationQuotient.uniformContinuous_lift theorem
{f : α → β} (h : ∀ a b, Inseparable a b → f a = f b) : UniformContinuous (lift f h) ↔ UniformContinuous f
Full source 
theorem uniformContinuous_lift {f : α → β} (h : ∀ a b, Inseparable a b → f a = f b) :
    UniformContinuousUniformContinuous (lift f h) ↔ UniformContinuous f :=
  .rfl
Uniform Continuity Criterion for Lifted Functions on Separation Quotient
Informal description
Let $f \colon \alpha \to \beta$ be a function between uniform spaces that respects inseparability (i.e., $f(a) = f(b)$ whenever $a$ and $b$ are inseparable in $\alpha$). Then the lifted function $\text{lift}(f,h) \colon \text{SeparationQuotient}(\alpha) \to \beta$ is uniformly continuous if and only if $f$ is uniformly continuous.
SeparationQuotient.uniformContinuous_uncurry_lift₂ theorem
{f : α → β → γ} (h : ∀ a c b d, Inseparable a b → Inseparable c d → f a c = f b d) : UniformContinuous (uncurry <| lift₂ f h) ↔ UniformContinuous (uncurry f)
Full source 
theorem uniformContinuous_uncurry_lift₂ {f : α → β → γ}
    (h : ∀ a c b d, Inseparable a b → Inseparable c d → f a c = f b d) :
    UniformContinuousUniformContinuous (uncurry <| lift₂ f h) ↔ UniformContinuous (uncurry f) :=
  uniformContinuous_dom₂
Uniform Continuity Criterion for Bivariate Lifted Functions on Separation Quotients
Informal description
Let $f \colon \alpha \to \beta \to \gamma$ be a function between uniform spaces that respects inseparability in both arguments (i.e., for any $a, b \in \alpha$ and $c, d \in \beta$, if $a$ and $b$ are inseparable and $c$ and $d$ are inseparable, then $f(a, c) = f(b, d)$). Then the uncurried version of the lifted function $\text{lift}_2(f, h) \colon \text{SeparationQuotient}(\alpha) \to \text{SeparationQuotient}(\beta) \to \gamma$ is uniformly continuous if and only if the uncurried version of $f$ is uniformly continuous.
SeparationQuotient.comap_mk_uniformity theorem
: (𝓤 (SeparationQuotient α)).comap (Prod.map mk mk) = 𝓤 α
Full source 
theorem comap_mk_uniformity : (𝓤 (SeparationQuotient α)).comap (Prod.map mk mk) = 𝓤 α :=
  comap_map_mk_uniformity
Uniformity Filter Preservation Under Separation Quotient Map
Informal description
For a uniform space $\alpha$, the preimage of the uniformity filter on the separation quotient $\text{SeparationQuotient}(\alpha)$ under the product map $\text{mk} \times \text{mk} : \alpha \times \alpha \to \text{SeparationQuotient}(\alpha) \times \text{SeparationQuotient}(\alpha)$ equals the original uniformity filter on $\alpha$. In other words, $(\text{mk} \times \text{mk})^{-1}(\mathcal{U}(\text{SeparationQuotient}(\alpha))) = \mathcal{U}(\alpha)$.
SeparationQuotient.lift' definition
[T0Space β] (f : α → β) : SeparationQuotient α → β
Full source 
/-- Factoring functions to a separated space through the separation quotient.

TODO: unify with `SeparationQuotient.lift`. -/
def lift' [T0Space β] (f : α → β) : SeparationQuotient α → β :=
  if hc : UniformContinuous f then lift f fun _ _ h => (h.map hc.continuous).eq
  else fun x => f (Nonempty.some ⟨x.out⟩)
Lifting a function to the separation quotient
Informal description
Given a uniform space $\alpha$ and a T₀ space $\beta$, the function `SeparationQuotient.lift'` lifts a map $f \colon \alpha \to \beta$ to a map from the separation quotient of $\alpha$ to $\beta$. If $f$ is uniformly continuous, then the lift is defined by factoring through the quotient map; otherwise, it returns a constant function determined by an arbitrary element of $\beta$ (using the nonemptyness of $\beta$ implied by the T₀ property).
SeparationQuotient.lift'_mk theorem
[T0Space β] {f : α → β} (h : UniformContinuous f) (a : α) : lift' f (mk a) = f a
Full source 
theorem lift'_mk [T0Space β] {f : α → β} (h : UniformContinuous f) (a : α) :
    lift' f (mk a) = f a := by rw [lift', dif_pos h, lift_mk]
Lift Evaluation on Quotient: $\text{lift}'\, f (\text{mk}\, a) = f(a)$ for Uniformly Continuous $f$
Informal description
Let $\alpha$ be a uniform space and $\beta$ be a T₀ space. Given a uniformly continuous function $f \colon \alpha \to \beta$, the lift of $f$ to the separation quotient satisfies $\text{lift}'\, f (\text{mk}\, a) = f(a)$ for any $a \in \alpha$, where $\text{mk} \colon \alpha \to \text{SeparationQuotient}\, \alpha$ is the quotient map.
SeparationQuotient.uniformContinuous_lift' theorem
[T0Space β] (f : α → β) : UniformContinuous (lift' f)
Full source 
theorem uniformContinuous_lift' [T0Space β] (f : α → β) : UniformContinuous (lift' f) := by
  by_cases hf : UniformContinuous f
  · rwa [lift', dif_pos hf, uniformContinuous_lift]
  · rw [lift', dif_neg hf]
    exact uniformContinuous_of_const fun a _ => rfl
Uniform Continuity of the Lifted Function on Separation Quotient
Informal description
Given a uniform space $\alpha$ and a T₀ space $\beta$, the lifted function $\text{lift}'\, f \colon \text{SeparationQuotient}(\alpha) \to \beta$ is uniformly continuous for any function $f \colon \alpha \to \beta$.
SeparationQuotient.map definition
(f : α → β) : SeparationQuotient α → SeparationQuotient β
Full source 
/-- The separation quotient functor acting on functions. -/
def map (f : α → β) : SeparationQuotient α → SeparationQuotient β := lift' (mkmk ∘ f)
Induced map on separation quotients
Informal description
The function `SeparationQuotient.map` takes a map $f \colon \alpha \to \beta$ between uniform spaces and returns the induced map $\text{SeparationQuotient}(\alpha) \to \text{SeparationQuotient}(\beta)$ between their separation quotients. If $f$ is uniformly continuous, then this map is given by $\text{map}\, f (\text{mk}\, x) = \text{mk}\, (f x)$, where $\text{mk}$ is the quotient map; otherwise, it returns a constant function.
SeparationQuotient.map_mk theorem
{f : α → β} (h : UniformContinuous f) (a : α) : map f (mk a) = mk (f a)
Full source 
theorem map_mk {f : α → β} (h : UniformContinuous f) (a : α) : map f (mk a) = mk (f a) := by
  rw [map, lift'_mk (uniformContinuous_mk.comp h)]; rfl
Commutativity of Separation Quotient Map: $\operatorname{map} f \circ \operatorname{mk} = \operatorname{mk} \circ f$ for Uniformly Continuous $f$
Informal description
For any uniformly continuous function $f \colon \alpha \to \beta$ between uniform spaces and any point $a \in \alpha$, the induced map on the separation quotients satisfies $\operatorname{map} f (\operatorname{mk} a) = \operatorname{mk} (f a)$, where $\operatorname{mk} \colon \alpha \to \operatorname{SeparationQuotient}(\alpha)$ is the quotient map.
SeparationQuotient.uniformContinuous_map theorem
(f : α → β) : UniformContinuous (map f)
Full source 
theorem uniformContinuous_map (f : α → β) : UniformContinuous (map f) :=
  uniformContinuous_lift' _
Uniform Continuity of the Induced Map on Separation Quotients
Informal description
For any map $f \colon \alpha \to \beta$ between uniform spaces, the induced map $\operatorname{map} f \colon \operatorname{SeparationQuotient}(\alpha) \to \operatorname{SeparationQuotient}(\beta)$ is uniformly continuous.
SeparationQuotient.map_unique theorem
{f : α → β} (hf : UniformContinuous f) {g : SeparationQuotient α → SeparationQuotient β} (comm : mk ∘ f = g ∘ mk) : map f = g
Full source 
theorem map_unique {f : α → β} (hf : UniformContinuous f)
    {g : SeparationQuotient α → SeparationQuotient β} (comm : mkmk ∘ f = g ∘ mk) : map f = g := by
  ext ⟨a⟩
  calc
    map f ⟦a⟧ = ⟦f a⟧ := map_mk hf a
    _ = g ⟦a⟧ := congr_fun comm a
Uniqueness of the Induced Map on Separation Quotients for Uniformly Continuous Functions
Informal description
Let $f \colon \alpha \to \beta$ be a uniformly continuous map between uniform spaces, and let $g \colon \text{SeparationQuotient}(\alpha) \to \text{SeparationQuotient}(\beta)$ be a map such that the diagram commutes, i.e., $\text{mk} \circ f = g \circ \text{mk}$, where $\text{mk}$ denotes the quotient map. Then the induced map $\text{map}\, f$ is equal to $g$.
SeparationQuotient.map_id theorem
: map (@id α) = id
Full source 
@[simp]
theorem map_id : map (@id α) = id := map_unique uniformContinuous_id rfl
Identity Map Induces Identity on Separation Quotient
Informal description
The induced map on the separation quotient of a uniform space $\alpha$ by the identity function $\text{id} \colon \alpha \to \alpha$ is equal to the identity function on $\text{SeparationQuotient}(\alpha)$.
SeparationQuotient.map_comp theorem
{f : α → β} {g : β → γ} (hf : UniformContinuous f) (hg : UniformContinuous g) : map g ∘ map f = map (g ∘ f)
Full source 
theorem map_comp {f : α → β} {g : β → γ} (hf : UniformContinuous f) (hg : UniformContinuous g) :
    mapmap g ∘ map f = map (g ∘ f) :=
  (map_unique (hg.comp hf) <| by simp only [Function.comp_def, map_mk, hf, hg]).symm
Composition of Induced Maps on Separation Quotients for Uniformly Continuous Functions
Informal description
Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be uniformly continuous maps between uniform spaces. Then the composition of the induced maps on separation quotients satisfies $\operatorname{map} g \circ \operatorname{map} f = \operatorname{map} (g \circ f)$.