mathlib documentation

topology.uniform_space.completion

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) coe : α → 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 ∘ coe. 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 coe 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.

def Cauchy (α : Type u) [uniform_space α] :

Type u

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.

Equations

Cauchy α = {f // cauchy f}

def Cauchy.gen {α : Type u} [uniform_space α] (s : set (α × α)) :

set (Cauchy α × Cauchy α)

Equations

Cauchy.gen s = {p : Cauchy α × Cauchy α | s ∈ p.fst.val ×ᶠ p.snd.val}

theorem Cauchy.monotone_gen {α : Type u} [uniform_space α] :

monotone Cauchy.gen

@[protected, instance]

def Cauchy.uniform_space {α : Type u} [uniform_space α] :

uniform_space (Cauchy α)

Equations

Cauchy.uniform_space = uniform_space.of_core {uniformity := (𝓤 α).lift' Cauchy.gen, refl := _, symm := _, comp := _}

theorem Cauchy.mem_uniformity {α : Type u} [uniform_space α] {s : set (Cauchy α × Cauchy α)} :

s ∈ 𝓤 (Cauchy α) ↔ ∃ (t : set (α × α)) (H : t ∈ 𝓤 α), Cauchy.gen t ⊆ s

theorem Cauchy.mem_uniformity' {α : Type u} [uniform_space α] {s : set (Cauchy α × Cauchy α)} :

s ∈ 𝓤 (Cauchy α) ↔ ∃ (t : set (α × α)) (H : t ∈ 𝓤 α), ∀ (f g : Cauchy α), t ∈ f.val ×ᶠ g.val → (f, g) ∈ s

def Cauchy.pure_cauchy {α : Type u} [uniform_space α] (a : α) :

Embedding of α into its completion Cauchy α

Equations

Cauchy.pure_cauchy a = ⟨pure a, _⟩

theorem Cauchy.uniform_inducing_pure_cauchy {α : Type u} [uniform_space α] :

uniform_inducing Cauchy.pure_cauchy

theorem Cauchy.uniform_embedding_pure_cauchy {α : Type u} [uniform_space α] :

uniform_embedding Cauchy.pure_cauchy

theorem Cauchy.dense_range_pure_cauchy {α : Type u} [uniform_space α] :

dense_range Cauchy.pure_cauchy

theorem Cauchy.dense_inducing_pure_cauchy {α : Type u} [uniform_space α] :

dense_inducing Cauchy.pure_cauchy

theorem Cauchy.dense_embedding_pure_cauchy {α : Type u} [uniform_space α] :

dense_embedding Cauchy.pure_cauchy

theorem Cauchy.nonempty_Cauchy_iff {α : Type u} [uniform_space α] :

nonempty (Cauchy α) ↔ nonempty α

@[protected, instance]

def Cauchy.complete_space {α : Type u} [uniform_space α] :

complete_space (Cauchy α)

@[protected, instance]

def Cauchy.inhabited {α : Type u} [uniform_space α] [inhabited α] :

inhabited (Cauchy α)

Equations

Cauchy.inhabited = {default := Cauchy.pure_cauchy default}

@[protected, instance]

def Cauchy.nonempty {α : Type u} [uniform_space α] [h : nonempty α] :

nonempty (Cauchy α)

noncomputable def Cauchy.extend {α : Type u} [uniform_space α] {β : Type v} [uniform_space β] (f : α → β) :

Cauchy α → β

Equations

Cauchy.extend f = ite (uniform_continuous f) (Cauchy.dense_inducing_pure_cauchy.extend f) (λ (x : Cauchy α), f 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 β] [complete_space β] {f : α → β} :

uniform_continuous (Cauchy.extend f)

theorem Cauchy.Cauchy_eq {α : Type u_1} [inhabited α] [uniform_space α] [complete_space α] [separated_space α] {f g : Cauchy α} :

Lim f.val = Lim g.val ↔ (f, g) ∈ 𝓢 (Cauchy α)

theorem Cauchy.separated_pure_cauchy_injective {α : Type u_1} [uniform_space α] [s : separated_space α] :

function.injective (λ (a : α), ⟦Cauchy.pure_cauchy a⟧)

@[protected, instance]

def uniform_space.complete_space_separation (α : Type u_1) [uniform_space α] [h : complete_space α] :

complete_space (quotient (uniform_space.separation_setoid α))

def uniform_space.completion (α : Type u_1) [uniform_space α] :

Type u_1

Hausdorff completion of α

Equations

uniform_space.completion α = quotient (uniform_space.separation_setoid (Cauchy α))

@[protected, instance]

def uniform_space.completion.inhabited (α : Type u_1) [uniform_space α] [inhabited α] :

inhabited (uniform_space.completion α)

Equations

uniform_space.completion.inhabited α = quotient.inhabited (uniform_space.separation_setoid (Cauchy α))

@[protected, instance]

def uniform_space.completion.uniform_space (α : Type u_1) [uniform_space α] :

uniform_space (uniform_space.completion α)

Equations

uniform_space.completion.uniform_space α = uniform_space.separation_setoid.uniform_space

@[protected, instance]

def uniform_space.completion.complete_space (α : Type u_1) [uniform_space α] :

complete_space (uniform_space.completion α)

@[protected, instance]

def uniform_space.completion.separated_space (α : Type u_1) [uniform_space α] :

separated_space (uniform_space.completion α)

@[protected, instance]

def uniform_space.completion.regular_space (α : Type u_1) [uniform_space α] :

regular_space (uniform_space.completion α)

@[protected, instance]

def uniform_space.completion.has_coe_t (α : Type u_1) [uniform_space α] :

has_coe_t α (uniform_space.completion α)

Automatic coercion from α to its completion. Not always injective.

Equations

uniform_space.completion.has_coe_t α = {coe := quotient.mk ∘ Cauchy.pure_cauchy}

@[protected]

theorem uniform_space.completion.coe_eq (α : Type u_1) [uniform_space α] :

coe = quotient.mk ∘ Cauchy.pure_cauchy

theorem uniform_space.completion.comap_coe_eq_uniformity (α : Type u_1) [uniform_space α] :

filter.comap (λ (p : α × α), (↑(p.fst), ↑(p.snd))) (𝓤 (uniform_space.completion α)) = 𝓤 α

theorem uniform_space.completion.uniform_inducing_coe (α : Type u_1) [uniform_space α] :

uniform_inducing coe

theorem uniform_space.completion.dense_range_coe {α : Type u_1} [uniform_space α] :

dense_range coe

def uniform_space.completion.cpkg {α : Type u_1} [uniform_space α] :

abstract_completion α

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 := _}

@[protected, instance]

def uniform_space.completion.abstract_completion.inhabited (α : Type u_1) [uniform_space α] :

inhabited (abstract_completion α)

Equations

uniform_space.completion.abstract_completion.inhabited α = {default := uniform_space.completion.cpkg _inst_1}

theorem uniform_space.completion.nonempty_completion_iff (α : Type u_1) [uniform_space α] :

nonempty (uniform_space.completion α) ↔ nonempty α

theorem uniform_space.completion.uniform_continuous_coe (α : Type u_1) [uniform_space α] :

uniform_continuous coe

theorem uniform_space.completion.continuous_coe (α : Type u_1) [uniform_space α] :

theorem uniform_space.completion.uniform_embedding_coe (α : Type u_1) [uniform_space α] [separated_space α] :

uniform_embedding coe

theorem uniform_space.completion.coe_injective (α : Type u_1) [uniform_space α] [separated_space α] :

function.injective coe

theorem uniform_space.completion.dense_inducing_coe {α : Type u_1} [uniform_space α] :

dense_inducing coe

@[protected, instance]

def uniform_space.completion.separable_space_completion {α : Type u_1} [uniform_space α] [topological_space.separable_space α] :

topological_space.separable_space (uniform_space.completion α)

theorem uniform_space.completion.dense_embedding_coe {α : Type u_1} [uniform_space α] [separated_space α] :

dense_embedding coe

theorem uniform_space.completion.dense_range_coe₂ {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] :

dense_range (λ (x : α × β), (↑(x.fst), ↑(x.snd)))

theorem uniform_space.completion.dense_range_coe₃ {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] {γ : Type u_3} [uniform_space γ] :

dense_range (λ (x : α × β × γ), (↑(x.fst), ↑(x.snd.fst), ↑(x.snd.snd)))

theorem uniform_space.completion.induction_on {α : Type u_1} [uniform_space α] {p : uniform_space.completion α → Prop} (a : uniform_space.completion α) (hp : is_closed {a : uniform_space.completion α | p a}) (ih : ∀ (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 β) (hp : is_closed {x : uniform_space.completion α × uniform_space.completion β | p x.fst x.snd}) (ih : ∀ (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 γ) (hp : is_closed {x : uniform_space.completion α × uniform_space.completion β × uniform_space.completion γ | p x.fst x.snd.fst x.snd.snd}) (ih : ∀ (a : α) (b : β) (c : γ), p ↑a ↑b ↑c) :

p a b c

theorem uniform_space.completion.ext {α : Type u_1} [uniform_space α] {Y : Type u_2} [topological_space Y] [t2_space Y] {f g : uniform_space.completion α → Y} (hf : continuous f) (hg : continuous g) (h : ∀ (a : α), f ↑a = g ↑a) :

f = g

theorem uniform_space.completion.ext' {α : Type u_1} [uniform_space α] {Y : Type u_2} [topological_space Y] [t2_space Y] {f g : uniform_space.completion α → Y} (hf : continuous f) (hg : continuous g) (h : ∀ (a : α), f ↑a = g ↑a) (a : uniform_space.completion α) :

f a = g a

@[protected]

noncomputable def uniform_space.completion.extension {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] (f : α → β) :

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

Equations

uniform_space.completion.extension f = uniform_space.completion.cpkg.extend f

theorem uniform_space.completion.uniform_continuous_extension {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] {f : α → β} [complete_space β] :

uniform_continuous (uniform_space.completion.extension f)

theorem uniform_space.completion.continuous_extension {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] {f : α → β} [complete_space β] :

continuous (uniform_space.completion.extension f)

@[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.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 α → β} (hg : uniform_continuous g) (h : ∀ (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 α → β} (hf : uniform_continuous f) :

uniform_space.completion.extension (f ∘ coe) = f

@[protected]

noncomputable def uniform_space.completion.map {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] (f : α → β) :

uniform_space.completion α → uniform_space.completion β

Completion functor acting on morphisms

Equations

uniform_space.completion.map f = uniform_space.completion.cpkg.map uniform_space.completion.cpkg f

theorem uniform_space.completion.uniform_continuous_map {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] {f : α → β} :

uniform_continuous (uniform_space.completion.map f)

theorem uniform_space.completion.continuous_map {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] {f : α → β} :

continuous (uniform_space.completion.map 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 β} (hg : uniform_continuous g) (h : ∀ (a : α), ↑(f a) = g ↑a) :

uniform_space.completion.map f = g

@[simp]

theorem uniform_space.completion.map_id {α : Type u_1} [uniform_space α] :

uniform_space.completion.map id = id

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 : α → β} (hf : uniform_continuous f) (hg : uniform_continuous g) :

uniform_space.completion.extension f ∘ uniform_space.completion.map g = uniform_space.completion.extension (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 : α → β} (hg : uniform_continuous g) (hf : uniform_continuous f) :

uniform_space.completion.map g ∘ uniform_space.completion.map f = uniform_space.completion.map (g ∘ f)

noncomputable def uniform_space.completion.completion_separation_quotient_equiv (α : Type u) [uniform_space α] :

uniform_space.completion (uniform_space.separation_quotient α) ≃ uniform_space.completion α

Equations

uniform_space.completion.completion_separation_quotient_equiv α = {to_fun := uniform_space.completion.extension (uniform_space.separation_quotient.lift coe), inv_fun := uniform_space.completion.map quotient.mk, left_inv := _, right_inv := _}

theorem uniform_space.completion.uniform_continuous_completion_separation_quotient_equiv {α : Type u_1} [uniform_space α] :

uniform_continuous ⇑(uniform_space.completion.completion_separation_quotient_equiv α)

theorem uniform_space.completion.uniform_continuous_completion_separation_quotient_equiv_symm {α : Type u_1} [uniform_space α] :

uniform_continuous ⇑((uniform_space.completion.completion_separation_quotient_equiv α).symm)

@[protected]

noncomputable def uniform_space.completion.extension₂ {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] {γ : Type u_3} [uniform_space γ] (f : α → β → γ) :

uniform_space.completion α → uniform_space.completion β → γ

Equations

uniform_space.completion.extension₂ f = uniform_space.completion.cpkg.extend₂ uniform_space.completion.cpkg f

@[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 : α → β → γ) [complete_space γ] :

uniform_continuous₂ (uniform_space.completion.extension₂ f)

@[protected]

noncomputable def uniform_space.completion.map₂ {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] {γ : Type u_3} [uniform_space γ] (f : α → β → γ) :

uniform_space.completion α → uniform_space.completion β → uniform_space.completion γ

Equations

uniform_space.completion.map₂ f = uniform_space.completion.cpkg.map₂ uniform_space.completion.cpkg uniform_space.completion.cpkg f

theorem uniform_space.completion.uniform_continuous_map₂ {α : Type u_1} [uniform_space α] {β : Type u_2} [uniform_space β] {γ : Type u_3} [uniform_space γ] (f : α → β → γ) :

uniform_continuous₂ (uniform_space.completion.map₂ 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 β} (ha : continuous a) (hb : 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 : α → β → γ) (hf : uniform_continuous₂ f) :

uniform_space.completion.map₂ f ↑a ↑b = ↑(f a b)