Documentation

Mathlib.Topology.UniformSpace.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) (↑) : α → 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 ∘ (↑). 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 (↑) 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 (↑) ∘ f = (Completion.map f) ∘ (↑) provided f is uniformly continuous. This construction is compatible with composition.

In this file we introduce the following concepts:

CauchyFilter α the uniform completion of the uniform space α (using Cauchy filters). These are not minimal filters.
Completion α := Quotient (separationSetoid (CauchyFilter α)) 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.UniformSpace.Basic.

def CauchyFilter (α : Type u) [UniformSpace α] :

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

CauchyFilter α = { f : Filter α // Cauchy f }

Instances For

instance CauchyFilter.instNeBotValFilterCauchy {α : Type u} [UniformSpace α] (f : CauchyFilter α) :

(↑f).NeBot

def CauchyFilter.gen {α : Type u} [UniformSpace α] (s : Set (α × α)) :

Set (CauchyFilter α × CauchyFilter α)

The pairs of Cauchy filters generated by a set.

Equations

CauchyFilter.gen s = {p : CauchyFilter α × CauchyFilter α | s ∈ ↑p.1 ×ˢ ↑p.2}

theorem CauchyFilter.monotone_gen {α : Type u} [UniformSpace α] :

instance CauchyFilter.instUniformSpace {α : Type u} [UniformSpace α] :

UniformSpace (CauchyFilter α)

Equations

CauchyFilter.instUniformSpace = UniformSpace.ofCore { uniformity := (uniformity α).lift' CauchyFilter.gen, refl := ⋯, symm := ⋯, comp := ⋯ }

theorem CauchyFilter.mem_uniformity {α : Type u} [UniformSpace α] {s : Set (CauchyFilter α × CauchyFilter α)} :

s ∈ uniformity (CauchyFilter α) ↔ ∃ t ∈ uniformity α, gen t ⊆ s

theorem CauchyFilter.basis_uniformity {α : Type u} [UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)} (h : (uniformity α).HasBasis p s) :

(uniformity (CauchyFilter α)).HasBasis p (gen ∘ s)

theorem CauchyFilter.mem_uniformity' {α : Type u} [UniformSpace α] {s : Set (CauchyFilter α × CauchyFilter α)} :

s ∈ uniformity (CauchyFilter α) ↔ ∃ t ∈ uniformity α, ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s

def CauchyFilter.pureCauchy {α : Type u} [UniformSpace α] (a : α) :

CauchyFilter α

Embedding of α into its completion CauchyFilter α

Equations

CauchyFilter.pureCauchy a = ⟨pure a, ⋯⟩

theorem CauchyFilter.isUniformInducing_pureCauchy {α : Type u} [UniformSpace α] :

IsUniformInducing pureCauchy

@[deprecated CauchyFilter.isUniformInducing_pureCauchy (since := "2024-10-05")]

theorem CauchyFilter.uniformInducing_pureCauchy {α : Type u} [UniformSpace α] :

IsUniformInducing pureCauchy

Alias of CauchyFilter.isUniformInducing_pureCauchy.

theorem CauchyFilter.isUniformEmbedding_pureCauchy {α : Type u} [UniformSpace α] :

IsUniformEmbedding pureCauchy

@[deprecated CauchyFilter.isUniformEmbedding_pureCauchy (since := "2024-10-01")]

theorem CauchyFilter.uniformEmbedding_pureCauchy {α : Type u} [UniformSpace α] :

IsUniformEmbedding pureCauchy

Alias of CauchyFilter.isUniformEmbedding_pureCauchy.

theorem CauchyFilter.denseRange_pureCauchy {α : Type u} [UniformSpace α] :

DenseRange pureCauchy

theorem CauchyFilter.isDenseInducing_pureCauchy {α : Type u} [UniformSpace α] :

IsDenseInducing pureCauchy

theorem CauchyFilter.isDenseEmbedding_pureCauchy {α : Type u} [UniformSpace α] :

IsDenseEmbedding pureCauchy

@[deprecated CauchyFilter.isDenseEmbedding_pureCauchy (since := "2024-09-30")]

theorem CauchyFilter.denseEmbedding_pureCauchy {α : Type u} [UniformSpace α] :

IsDenseEmbedding pureCauchy

Alias of CauchyFilter.isDenseEmbedding_pureCauchy.

theorem CauchyFilter.nonempty_cauchyFilter_iff {α : Type u} [UniformSpace α] :

Nonempty (CauchyFilter α) ↔ Nonempty α

instance CauchyFilter.instCompleteSpace {α : Type u} [UniformSpace α] :

CompleteSpace (CauchyFilter α)

instance CauchyFilter.instInhabited {α : Type u} [UniformSpace α] [Inhabited α] :

Inhabited (CauchyFilter α)

Equations

CauchyFilter.instInhabited = { default := CauchyFilter.pureCauchy default }

instance CauchyFilter.instNonempty {α : Type u} [UniformSpace α] [h : Nonempty α] :

Nonempty (CauchyFilter α)

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

CauchyFilter α → β

Extend a uniformly continuous function α → β to a function CauchyFilter α → β. Outputs junk when f is not uniformly continuous.

Equations

CauchyFilter.extend f = if UniformContinuous f then ⋯.extend f else fun (x : CauchyFilter α) => f ⋯.some

theorem CauchyFilter.extend_pureCauchy {α : Type u} [UniformSpace α] {β : Type v} [UniformSpace β] [T0Space β] {f : α → β} (hf : UniformContinuous f) (a : α) :

extend f (pureCauchy a) = f a

theorem CauchyFilter.uniformContinuous_extend {α : Type u} [UniformSpace α] {β : Type v} [UniformSpace β] [CompleteSpace β] {f : α → β} :

UniformContinuous (extend f)

theorem CauchyFilter.inseparable_iff {α : Type u} [UniformSpace α] {f g : CauchyFilter α} :

Inseparable f g ↔ ↑f ×ˢ ↑g ≤ uniformity α

theorem CauchyFilter.inseparable_iff_of_le_nhds {α : Type u} [UniformSpace α] {f g : CauchyFilter α} {a b : α} (ha : ↑f ≤ nhds a) (hb : ↑g ≤ nhds b) :

Inseparable a b ↔ Inseparable f g

theorem CauchyFilter.inseparable_lim_iff {α : Type u} [UniformSpace α] [CompleteSpace α] {f g : CauchyFilter α} :

Inseparable (lim ↑f) (lim ↑g) ↔ Inseparable f g

theorem CauchyFilter.cauchyFilter_eq {α : Type u_1} [UniformSpace α] [CompleteSpace α] [T0Space α] {f g : CauchyFilter α} :

lim ↑f = lim ↑g ↔ Inseparable f g

theorem CauchyFilter.separated_pureCauchy_injective {α : Type u_1} [UniformSpace α] [T0Space α] :

Function.Injective fun (a : α) => SeparationQuotient.mk (pureCauchy a)

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

Type u_1

Hausdorff completion of α

Equations

UniformSpace.Completion α = SeparationQuotient (CauchyFilter α)

Instances For

instance UniformSpace.Completion.inhabited (α : Type u_1) [UniformSpace α] [Inhabited α] :

Inhabited (Completion α)

Equations

UniformSpace.Completion.inhabited α = inferInstanceAs (Inhabited (Quotient (inseparableSetoid (CauchyFilter α))))

instance UniformSpace.Completion.uniformSpace (α : Type u_1) [UniformSpace α] :

UniformSpace (Completion α)

Equations

UniformSpace.Completion.uniformSpace α = SeparationQuotient.instUniformSpace

instance UniformSpace.Completion.completeSpace (α : Type u_1) [UniformSpace α] :

CompleteSpace (Completion α)

instance UniformSpace.Completion.t0Space (α : Type u_1) [UniformSpace α] :

T0Space (Completion α)

def UniformSpace.Completion.coe' {α : Type u_1} [UniformSpace α] :

α → Completion α

The map from a uniform space to its completion.

Equations

UniformSpace.Completion.coe' = SeparationQuotient.mk ∘ CauchyFilter.pureCauchy

instance UniformSpace.Completion.instCoe (α : Type u_1) [UniformSpace α] :

Coe α (Completion α)

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

Equations

UniformSpace.Completion.instCoe α = { coe := UniformSpace.Completion.coe' }

theorem UniformSpace.Completion.coe_eq (α : Type u_1) [UniformSpace α] :

coe' = SeparationQuotient.mk ∘ CauchyFilter.pureCauchy

theorem UniformSpace.Completion.isUniformInducing_coe (α : Type u_1) [UniformSpace α] :

IsUniformInducing coe'

@[deprecated UniformSpace.Completion.isUniformInducing_coe (since := "2024-10-05")]

theorem UniformSpace.Completion.uniformInducing_coe (α : Type u_1) [UniformSpace α] :

IsUniformInducing coe'

Alias of UniformSpace.Completion.isUniformInducing_coe.

theorem UniformSpace.Completion.comap_coe_eq_uniformity (α : Type u_1) [UniformSpace α] :

Filter.comap (fun (p : α × α) => (↑p.1, ↑p.2)) (uniformity (Completion α)) = uniformity α

theorem UniformSpace.Completion.denseRange_coe {α : Type u_1} [UniformSpace α] :

DenseRange coe'

def UniformSpace.Completion.cPkg {α : Type u_4} [UniformSpace α] :

AbstractCompletion α

The Haudorff completion as an abstract completion.

Equations

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

instance UniformSpace.Completion.AbstractCompletion.inhabited (α : Type u_1) [UniformSpace α] :

Inhabited (AbstractCompletion α)

Equations

UniformSpace.Completion.AbstractCompletion.inhabited α = { default := UniformSpace.Completion.cPkg }

theorem UniformSpace.Completion.nonempty_completion_iff (α : Type u_1) [UniformSpace α] :

Nonempty (Completion α) ↔ Nonempty α

theorem UniformSpace.Completion.uniformContinuous_coe (α : Type u_1) [UniformSpace α] :

UniformContinuous coe'

theorem UniformSpace.Completion.continuous_coe (α : Type u_1) [UniformSpace α] :

Continuous coe'

theorem UniformSpace.Completion.isUniformEmbedding_coe (α : Type u_1) [UniformSpace α] [T0Space α] :

IsUniformEmbedding coe'

@[deprecated UniformSpace.Completion.isUniformEmbedding_coe (since := "2024-10-01")]

theorem UniformSpace.Completion.uniformEmbedding_coe (α : Type u_1) [UniformSpace α] [T0Space α] :

IsUniformEmbedding coe'

Alias of UniformSpace.Completion.isUniformEmbedding_coe.

theorem UniformSpace.Completion.coe_injective (α : Type u_1) [UniformSpace α] [T0Space α] :

Function.Injective coe'

theorem UniformSpace.Completion.isDenseInducing_coe {α : Type u_1} [UniformSpace α] :

IsDenseInducing coe'

def UniformSpace.Completion.UniformCompletion.completeEquivSelf {α : Type u_1} [UniformSpace α] [CompleteSpace α] [T0Space α] :

Completion α ≃ᵤ α

The uniform bijection between a complete space and its uniform completion.

Equations

UniformSpace.Completion.UniformCompletion.completeEquivSelf = UniformSpace.Completion.cPkg.compareEquiv AbstractCompletion.ofComplete

instance UniformSpace.Completion.separableSpace_completion {α : Type u_1} [UniformSpace α] [TopologicalSpace.SeparableSpace α] :

TopologicalSpace.SeparableSpace (Completion α)

theorem UniformSpace.Completion.isDenseEmbedding_coe {α : Type u_1} [UniformSpace α] [T0Space α] :

IsDenseEmbedding coe'

@[deprecated UniformSpace.Completion.isDenseEmbedding_coe (since := "2024-09-30")]

theorem UniformSpace.Completion.denseEmbedding_coe {α : Type u_1} [UniformSpace α] [T0Space α] :

IsDenseEmbedding coe'

Alias of UniformSpace.Completion.isDenseEmbedding_coe.

theorem UniformSpace.Completion.denseRange_coe₂ {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] :

DenseRange fun (x : α × β) => (↑x.1, ↑x.2)

theorem UniformSpace.Completion.denseRange_coe₃ {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {γ : Type u_3} [UniformSpace γ] :

DenseRange fun (x : α × β × γ) => (↑x.1, ↑x.2.1, ↑x.2.2)

theorem UniformSpace.Completion.induction_on {α : Type u_1} [UniformSpace α] {p : Completion α → Prop} (a : Completion α) (hp : IsClosed {a : Completion α | p a}) (ih : ∀ (a : α), p ↑a) :

p a

theorem UniformSpace.Completion.induction_on₂ {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {p : Completion α → Completion β → Prop} (a : Completion α) (b : Completion β) (hp : IsClosed {x : Completion α × Completion β | p x.1 x.2}) (ih : ∀ (a : α) (b : β), p ↑a ↑b) :

p a b

theorem UniformSpace.Completion.induction_on₃ {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {γ : Type u_3} [UniformSpace γ] {p : Completion α → Completion β → Completion γ → Prop} (a : Completion α) (b : Completion β) (c : Completion γ) (hp : IsClosed {x : Completion α × Completion β × Completion γ | p x.1 x.2.1 x.2.2}) (ih : ∀ (a : α) (b : β) (c : γ), p ↑a ↑b ↑c) :

p a b c

theorem UniformSpace.Completion.ext {α : Type u_1} [UniformSpace α] {Y : Type u_4} [TopologicalSpace Y] [T2Space Y] {f g : Completion α → Y} (hf : Continuous f) (hg : Continuous g) (h : ∀ (a : α), f ↑a = g ↑a) :

f = g

theorem UniformSpace.Completion.ext' {α : Type u_1} [UniformSpace α] {Y : Type u_4} [TopologicalSpace Y] [T2Space Y] {f g : Completion α → Y} (hf : Continuous f) (hg : Continuous g) (h : ∀ (a : α), f ↑a = g ↑a) (a : Completion α) :

f a = g a

def UniformSpace.Completion.extension {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] (f : α → β) :

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

UniformSpace.Completion.extension f = UniformSpace.Completion.cPkg.extend f

theorem UniformSpace.Completion.uniformContinuous_extension {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {f : α → β} [CompleteSpace β] :

UniformContinuous (Completion.extension f)

theorem UniformSpace.Completion.continuous_extension {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {f : α → β} [CompleteSpace β] :

Continuous (Completion.extension f)

theorem UniformSpace.Completion.extension_coe {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {f : α → β} [T0Space β] (hf : UniformContinuous f) (a : α) :

Completion.extension f ↑a = f a

theorem UniformSpace.Completion.extension_unique {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {f : α → β} [T0Space β] [CompleteSpace β] (hf : UniformContinuous f) {g : Completion α → β} (hg : UniformContinuous g) (h : ∀ (a : α), f a = g ↑a) :

Completion.extension f = g

@[simp]

theorem UniformSpace.Completion.extension_comp_coe {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] [T0Space β] [CompleteSpace β] {f : Completion α → β} (hf : UniformContinuous f) :

Completion.extension (f ∘ coe') = f

def UniformSpace.Completion.map {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] (f : α → β) :

Completion α → Completion β

Completion functor acting on morphisms

Equations

UniformSpace.Completion.map f = UniformSpace.Completion.cPkg.map UniformSpace.Completion.cPkg f

theorem UniformSpace.Completion.uniformContinuous_map {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {f : α → β} :

UniformContinuous (Completion.map f)

theorem UniformSpace.Completion.continuous_map {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {f : α → β} :

Continuous (Completion.map f)

theorem UniformSpace.Completion.map_coe {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {f : α → β} (hf : UniformContinuous f) (a : α) :

Completion.map f ↑a = ↑(f a)

theorem UniformSpace.Completion.map_unique {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {f : α → β} {g : Completion α → Completion β} (hg : UniformContinuous g) (h : ∀ (a : α), ↑(f a) = g ↑a) :

Completion.map f = g

@[simp]

theorem UniformSpace.Completion.map_id {α : Type u_1} [UniformSpace α] :

Completion.map id = id

theorem UniformSpace.Completion.extension_map {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {γ : Type u_3} [UniformSpace γ] [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β} (hf : UniformContinuous f) (hg : UniformContinuous g) :

Completion.extension f ∘ Completion.map g = Completion.extension (f ∘ g)

theorem UniformSpace.Completion.map_comp {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {γ : Type u_3} [UniformSpace γ] {g : β → γ} {f : α → β} (hg : UniformContinuous g) (hf : UniformContinuous f) :

Completion.map g ∘ Completion.map f = Completion.map (g ∘ f)

def UniformSpace.Completion.completionSeparationQuotientEquiv (α : Type u) [UniformSpace α] :

Completion (SeparationQuotient α) ≃ Completion α

The isomorphism between the completion of a uniform space and the completion of its separation quotient.

Equations

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

theorem UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv {α : Type u_1} [UniformSpace α] :

UniformContinuous ⇑(completionSeparationQuotientEquiv α)

theorem UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv_symm {α : Type u_1} [UniformSpace α] :

UniformContinuous ⇑(completionSeparationQuotientEquiv α).symm

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

Completion α → Completion β → γ

Extend a two variable map to the Hausdorff completions.

Equations

UniformSpace.Completion.extension₂ f = UniformSpace.Completion.cPkg.extend₂ UniformSpace.Completion.cPkg f

theorem UniformSpace.Completion.extension₂_coe_coe {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {γ : Type u_3} [UniformSpace γ] {f : α → β → γ} [T0Space γ] (hf : UniformContinuous₂ f) (a : α) (b : β) :

Completion.extension₂ f ↑a ↑b = f a b

theorem UniformSpace.Completion.uniformContinuous_extension₂ {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {γ : Type u_3} [UniformSpace γ] (f : α → β → γ) [CompleteSpace γ] :

UniformContinuous₂ (Completion.extension₂ f)

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

Completion α → Completion β → Completion γ

Lift a two variable map to the Hausdorff completions.

Equations

UniformSpace.Completion.map₂ f = UniformSpace.Completion.cPkg.map₂ UniformSpace.Completion.cPkg UniformSpace.Completion.cPkg f

theorem UniformSpace.Completion.uniformContinuous_map₂ {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {γ : Type u_3} [UniformSpace γ] (f : α → β → γ) :

UniformContinuous₂ (Completion.map₂ f)

theorem UniformSpace.Completion.continuous_map₂ {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {γ : Type u_3} [UniformSpace γ] {δ : Type u_4} [TopologicalSpace δ] {f : α → β → γ} {a : δ → Completion α} {b : δ → Completion β} (ha : Continuous a) (hb : Continuous b) :

Continuous fun (d : δ) => Completion.map₂ f (a d) (b d)

theorem UniformSpace.Completion.map₂_coe_coe {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {γ : Type u_3} [UniformSpace γ] (a : α) (b : β) (f : α → β → γ) (hf : UniformContinuous₂ f) :

Completion.map₂ f ↑a ↑b = ↑(f a b)