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 α] : 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

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

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 α] : Monotone gen

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 α)

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)