Hausdorff completions of uniform spaces
The goal is to construct a left-adjoint to the inclusion of complete Hausdorff uniform spaces
into all uniform spaces. Any uniform space α gets a completion completion α and a morphism
(ie. uniformly continuous map) completion : α → completion α which solves the universal
mapping problem of factorizing morphisms from α to any complete Hausdorff uniform space β.
It means any uniformly continuous f : α → β gives rise to a unique morphism
completion.extension f : completion α → β such that f = completion.extension f ∘ completion α.
Actually completion.extension f is defined for all maps from α to β but it has the desired
properties only if f is uniformly continuous.
Beware that completion α is not injective if α is not Hausdorff. But its image is always
dense. The adjoint functor acting on morphisms is then constructed by the usual abstract nonsense.
For every uniform spaces α and β, it turns f : α → β into a morphism
completion.map f : completion α → completion β
such that
coe ∘ f = (completion.map f) ∘ coe
provided f is uniformly continuous. This construction is compatible with composition.
In this file we introduce the following concepts:
Cauchy αthe uniform completion of the uniform spaceα(using Cauchy filters). These are not minimal filters.completion α := quotient (separation_setoid (Cauchy α))the Hausdorff completion.
References
This formalization is mostly based on N. Bourbaki: General Topology I. M. James: Topologies and Uniformities From a slightly different perspective in order to reuse material in topology.uniform_space.basic.
Space of Cauchy filters
This is essentially the completion of a uniform space. The embeddings are the neighbourhood filters. This space is not minimal, the separated uniform space (i.e. quotiented on the intersection of all entourages) is necessary for this.
@[instance]
Equations
- Cauchy.uniform_space = uniform_space.of_core {uniformity := (uniformity α).lift' Cauchy.gen, refl := _, symm := _, comp := _}
theorem
Cauchy.mem_uniformity
{α : Type u}
[uniform_space α]
{s : set (Cauchy α × Cauchy α)} :
s ∈ uniformity (Cauchy α) ↔ ∃ (t : set (α × α)) (H : t ∈ uniformity α), Cauchy.gen t ⊆ s
Embedding of α into its completion
Equations
- Cauchy.pure_cauchy a = ⟨has_pure.pure a, _⟩
@[instance]
Equations
- Cauchy.complete_space = _
- _ = _
- _ = _
@[instance]
Equations
@[instance]
Equations
def
Cauchy.extend
{α : Type u}
[uniform_space α]
{β : Type v}
[uniform_space β] :
(α → β) → Cauchy α → β
Equations
- Cauchy.extend f = ite (uniform_continuous f) (Cauchy.dense_inducing_pure_cauchy.extend f) (λ (x : Cauchy α), f (inhabited.default α))
theorem
Cauchy.extend_pure_cauchy
{α : Type u}
[uniform_space α]
{β : Type v}
[uniform_space β]
[separated_space β]
{f : α → β}
(hf : uniform_continuous f)
(a : α) :
Cauchy.extend f (Cauchy.pure_cauchy a) = f a
theorem
Cauchy.uniform_continuous_extend
{α : Type u}
[uniform_space α]
{β : Type v}
[uniform_space β]
[separated_space β]
[complete_space β]
{f : α → β} :
theorem
Cauchy.Cauchy_eq
{α : Type u_1}
[inhabited α]
[uniform_space α]
[complete_space α]
[separated_space α]
{f g : Cauchy α} :
theorem
Cauchy.separated_pure_cauchy_injective
{α : Type u_1}
[uniform_space α]
[s : separated_space α] :
function.injective (λ (a : α), ⟦Cauchy.pure_cauchy a⟧)
@[instance]
def
uniform_space.complete_space_separation
(α : Type u_1)
[uniform_space α]
[h : complete_space α] :
Hausdorff completion of α
Equations
@[instance]
Equations
@[instance]
@[instance]
Equations
- _ = _
@[instance]
Equations
- _ = _
@[instance]
Equations
@[instance]
Automatic coercion from α to its completion. Not always injective.
Equations
theorem
uniform_space.completion.comap_coe_eq_uniformity
(α : Type u_1)
[uniform_space α] :
filter.comap (λ (p : α × α), (↑(p.fst), ↑(p.snd))) (uniformity (uniform_space.completion α)) = uniformity α
Equations
- uniform_space.completion.cpkg = {space := uniform_space.completion α _inst_4, coe := coe coe_to_lift, uniform_struct := uniform_space.completion.uniform_space α _inst_4, complete := _, separation := _, uniform_inducing := _, dense := _}
@[instance]
Equations
theorem
uniform_space.completion.uniform_embedding_coe
(α : Type u_1)
[uniform_space α]
[separated_space α] :
theorem
uniform_space.completion.dense_embedding_coe
{α : Type u_1}
[uniform_space α]
[separated_space α] :
theorem
uniform_space.completion.dense₂
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β] :
theorem
uniform_space.completion.dense₃
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ] :
theorem
uniform_space.completion.induction_on
{α : Type u_1}
[uniform_space α]
{p : uniform_space.completion α → Prop}
(a : uniform_space.completion α) :
is_closed {a : uniform_space.completion α | p a} → (∀ (a : α), p ↑a) → p a
theorem
uniform_space.completion.induction_on₂
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{p : uniform_space.completion α → uniform_space.completion β → Prop}
(a : uniform_space.completion α)
(b : uniform_space.completion β) :
is_closed {x : uniform_space.completion α × uniform_space.completion β | p x.fst x.snd} → (∀ (a : α) (b : β), p ↑a ↑b) → p a b
theorem
uniform_space.completion.induction_on₃
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ]
{p : uniform_space.completion α → uniform_space.completion β → uniform_space.completion γ → Prop}
(a : uniform_space.completion α)
(b : uniform_space.completion β)
(c : uniform_space.completion γ) :
is_closed {x : uniform_space.completion α × uniform_space.completion β × uniform_space.completion γ | p x.fst x.snd.fst x.snd.snd} → (∀ (a : α) (b : β) (c : γ), p ↑a ↑b ↑c) → p a b c
theorem
uniform_space.completion.ext
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
[t2_space β]
{f g : uniform_space.completion α → β} :
continuous f → continuous g → (∀ (a : α), f ↑a = g ↑a) → f = g
def
uniform_space.completion.extension
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β] :
(α → β) → uniform_space.completion α → β
"Extension" to the completion. It is defined for any map f but
returns an arbitrary constant value if f is not uniformly continuous
@[simp]
theorem
uniform_space.completion.extension_coe
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{f : α → β}
[separated_space β]
(hf : uniform_continuous f)
(a : α) :
uniform_space.completion.extension f ↑a = f a
theorem
uniform_space.completion.uniform_continuous_extension
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{f : α → β}
[separated_space β]
[complete_space β] :
theorem
uniform_space.completion.continuous_extension
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{f : α → β}
[separated_space β]
[complete_space β] :
theorem
uniform_space.completion.extension_unique
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{f : α → β}
[separated_space β]
[complete_space β]
(hf : uniform_continuous f)
{g : uniform_space.completion α → β} :
uniform_continuous g → (∀ (a : α), f a = g ↑a) → uniform_space.completion.extension f = g
@[simp]
theorem
uniform_space.completion.extension_comp_coe
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
[separated_space β]
[complete_space β]
{f : uniform_space.completion α → β} :
def
uniform_space.completion.map
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β] :
(α → β) → uniform_space.completion α → uniform_space.completion β
Completion functor acting on morphisms
theorem
uniform_space.completion.uniform_continuous_map
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{f : α → β} :
theorem
uniform_space.completion.continuous_map
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{f : α → β} :
@[simp]
theorem
uniform_space.completion.map_coe
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{f : α → β}
(hf : uniform_continuous f)
(a : α) :
uniform_space.completion.map f ↑a = ↑(f a)
theorem
uniform_space.completion.map_unique
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{f : α → β}
{g : uniform_space.completion α → uniform_space.completion β} :
uniform_continuous g → (∀ (a : α), ↑(f a) = g ↑a) → uniform_space.completion.map f = g
@[simp]
theorem
uniform_space.completion.extension_map
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ]
[complete_space γ]
[separated_space γ]
{f : β → γ}
{g : α → β} :
theorem
uniform_space.completion.map_comp
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ]
{g : β → γ}
{f : α → β} :
def
uniform_space.completion.completion_separation_quotient_equiv
(α : Type u)
[uniform_space α] :
def
uniform_space.completion.extension₂
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ] :
(α → β → γ) → uniform_space.completion α → uniform_space.completion β → γ
@[simp]
theorem
uniform_space.completion.extension₂_coe_coe
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ]
{f : α → β → γ}
[separated_space γ]
(hf : uniform_continuous₂ f)
(a : α)
(b : β) :
uniform_space.completion.extension₂ f ↑a ↑b = f a b
theorem
uniform_space.completion.uniform_continuous_extension₂
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ]
(f : α → β → γ)
[separated_space γ]
[complete_space γ] :
def
uniform_space.completion.map₂
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ] :
(α → β → γ) → uniform_space.completion α → uniform_space.completion β → uniform_space.completion γ
theorem
uniform_space.completion.uniform_continuous_map₂
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ]
(f : α → β → γ) :
theorem
uniform_space.completion.continuous_map₂
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ]
{δ : Type u_4}
[topological_space δ]
{f : α → β → γ}
{a : δ → uniform_space.completion α}
{b : δ → uniform_space.completion β} :
continuous a → continuous b → continuous (λ (d : δ), uniform_space.completion.map₂ f (a d) (b d))
theorem
uniform_space.completion.map₂_coe_coe
{α : Type u_1}
[uniform_space α]
{β : Type u_2}
[uniform_space β]
{γ : Type u_3}
[uniform_space γ]
(a : α)
(b : β)
(f : α → β → γ) :
uniform_continuous₂ f → uniform_space.completion.map₂ f ↑a ↑b = ↑(f a b)