Abstract theory of Hausdorff completions of uniform spaces

This file characterizes Hausdorff completions of a uniform space α as complete Hausdorff spaces equipped with a map from α which has dense image and induce the original uniform structure on α. Assuming these properties we "extend" uniformly continuous maps from α to complete Hausdorff spaces to the completions of α. This is the universal property expected from a completion. It is then used to extend uniformly continuous maps from α to α' to maps between completions of α and α'.

This file does not construct any such completion, it only study consequences of their existence. The first advantage is that formal properties are clearly highlighted without interference from construction details. The second advantage is that this framework can then be used to compare different completion constructions. See Topology/UniformSpace/CompareReals for an example. Of course the comparison comes from the universal property as usual.

A general explicit construction of completions is done in UniformSpace/Completion, leading to a functor from uniform spaces to complete Hausdorff uniform spaces that is left adjoint to the inclusion, see UniformSpace/UniformSpaceCat for the category packaging.

Implementation notes

A tiny technical advantage of using a characteristic predicate such as the properties listed in AbstractCompletion instead of stating the universal property is that the universal property derived from the predicate is more universe polymorphic.

References

We don't know any traditional text discussing this. Real world mathematics simply silently identify the results of any two constructions that lead to something one could reasonably call a completion.

Tags

uniform spaces, completion, universal property

structure AbstractCompletion (α : Type u) [UniformSpace α] : Type (max u (v + 1))

A completion of α is the data of a complete separated uniform space and a map from α with dense range and inducing the original uniform structure on α.

• space : Type v

  The underlying space of the completion.

• coe : α → self.space

  A map from a space to its completion.

• uniformStruct : UniformSpace self.space

  The completion carries a uniform structure.

• complete : CompleteSpace self.space

  The completion is complete.

• separation : T0Space self.space

  The completion is a T₀ space.

• isUniformInducing : IsUniformInducing self.coe

  The map into the completion is uniform-inducing.

• dense : DenseRange self.coe

  The map into the completion has dense range.

def AbstractCompletion.ofComplete {α : Type uα} [UniformSpace α] [T0Space α] [CompleteSpace α] : AbstractCompletion.{uα, uα} α

If α is complete, then it is an abstract completion of itself.

theorem AbstractCompletion.closure_range {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) : closure (Set.range pkg.coe) = Set.univ

theorem AbstractCompletion.isDenseInducing {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) : IsDenseInducing pkg.coe

theorem AbstractCompletion.uniformContinuous_coe {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) : UniformContinuous pkg.coe

theorem AbstractCompletion.continuous_coe {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) : Continuous pkg.coe

theorem AbstractCompletion.induction_on {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {p : pkg.space → Prop} (a : pkg.space) (hp : IsClosed {a : pkg.space | p a}) (ih : ∀ (a : α), p (pkg.coe a)) : p a

theorem AbstractCompletion.funext {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [TopologicalSpace β] [T2Space β] {f g : pkg.space → β} (hf : Continuous f) (hg : Continuous g) (h : ∀ (a : α), f (pkg.coe a) = g (pkg.coe a)) : f = g

def AbstractCompletion.extend {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (f : α → β) : pkg.space → β

Extension of maps to completions

theorem AbstractCompletion.extend_def {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] {f : α → β} (hf : UniformContinuous f) : pkg.extend f = ⋯.extend f

theorem AbstractCompletion.extend_coe {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] {f : α → β} [T2Space β] (hf : UniformContinuous f) (a : α) : pkg.extend f (pkg.coe a) = f a

theorem AbstractCompletion.uniformContinuous_extend {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] {f : α → β} [CompleteSpace β] : UniformContinuous (pkg.extend f)

theorem AbstractCompletion.continuous_extend {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] {f : α → β} [CompleteSpace β] : Continuous (pkg.extend f)

theorem AbstractCompletion.extend_unique {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] {f : α → β} [CompleteSpace β] [T0Space β] (hf : UniformContinuous f) {g : pkg.space → β} (hg : UniformContinuous g) (h : ∀ (a : α), f a = g (pkg.coe a)) : pkg.extend f = g

@[simp]

theorem AbstractCompletion.extend_comp_coe {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] [CompleteSpace β] [T0Space β] {f : pkg.space → β} (hf : UniformContinuous f) : pkg.extend (f ∘ pkg.coe) = f

def AbstractCompletion.map {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) (f : α → β) : pkg.space → pkg'.space

Lifting maps to completions

theorem AbstractCompletion.uniformContinuous_map {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) (f : α → β) : UniformContinuous (pkg.map pkg' f)

theorem AbstractCompletion.continuous_map {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) (f : α → β) : Continuous (pkg.map pkg' f)

@[simp]

theorem AbstractCompletion.map_coe {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) {f : α → β} (hf : UniformContinuous f) (a : α) : pkg.map pkg' f (pkg.coe a) = pkg'.coe (f a)

theorem AbstractCompletion.map_unique {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) {f : α → β} {g : pkg.space → pkg'.space} (hg : UniformContinuous g) (h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)) : pkg.map pkg' f = g

@[simp]

theorem AbstractCompletion.map_id {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) : pkg.map pkg id = id

theorem AbstractCompletion.extend_map {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [UniformSpace γ] [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β} (hf : UniformContinuous f) (hg : UniformContinuous g) : pkg'.extend f ∘ pkg.map pkg' g = pkg.extend (f ∘ g)

theorem AbstractCompletion.map_comp {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [UniformSpace γ] (pkg'' : AbstractCompletion.{vγ, uγ} γ) {g : β → γ} {f : α → β} (hg : UniformContinuous g) (hf : UniformContinuous f) : pkg'.map pkg'' g ∘ pkg.map pkg' f = pkg.map pkg'' (g ∘ f)

def AbstractCompletion.compare {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α) : pkg.space → pkg'.space

The comparison map between two completions of the same uniform space.

theorem AbstractCompletion.uniformContinuous_compare {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α) : UniformContinuous (pkg.compare pkg')

theorem AbstractCompletion.compare_coe {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α) (a : α) : pkg.compare pkg' (pkg.coe a) = pkg'.coe a

theorem AbstractCompletion.inverse_compare {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α) : pkg.compare pkg' ∘ pkg'.compare pkg = id

def AbstractCompletion.compareEquiv {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α) : pkg.space ≃ᵤ pkg'.space

The uniform bijection between two completions of the same uniform space.

theorem AbstractCompletion.uniformContinuous_compareEquiv {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α) : UniformContinuous ⇑(pkg.compareEquiv pkg')

theorem AbstractCompletion.uniformContinuous_compareEquiv_symm {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α) : UniformContinuous ⇑(pkg.compareEquiv pkg').symm

theorem AbstractCompletion.compare_comp_eq_compare {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α) (γ : Type uγ) [TopologicalSpace γ] [T3Space γ] {f : α → γ} (cont_f : Continuous f) : (∀ (a : pkg.space), Filter.Tendsto f (Filter.comap pkg.coe (nhds a)) (nhds (⋯.extend f a))) → ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

def AbstractCompletion.prod {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) : AbstractCompletion.{max vβ vα, max uβ uα} (α × β)

Products of completions

def AbstractCompletion.extend₂ {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [UniformSpace γ] (f : α → β → γ) : pkg.space → pkg'.space → γ

Extend two variable map to completions.

theorem AbstractCompletion.extension₂_coe_coe {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [UniformSpace γ] [T0Space γ] {f : α → β → γ} (hf : UniformContinuous (Function.uncurry f)) (a : α) (b : β) : pkg.extend₂ pkg' f (pkg.coe a) (pkg'.coe b) = f a b

theorem AbstractCompletion.uniformContinuous_extension₂ {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [UniformSpace γ] (f : α → β → γ) [CompleteSpace γ] : UniformContinuous₂ (pkg.extend₂ pkg' f)

def AbstractCompletion.map₂ {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{u_1, uβ} β) {γ : Type uγ} [UniformSpace γ] (pkg'' : AbstractCompletion.{vγ, uγ} γ) (f : α → β → γ) : pkg.space → pkg'.space → pkg''.space

Lift two variable maps to completions.

theorem AbstractCompletion.uniformContinuous_map₂ {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{u_1, uβ} β) {γ : Type uγ} [UniformSpace γ] (pkg'' : AbstractCompletion.{vγ, uγ} γ) (f : α → β → γ) : UniformContinuous₂ (pkg.map₂ pkg' pkg'' f)

theorem AbstractCompletion.continuous_map₂ {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{u_2, uβ} β) {γ : Type uγ} [UniformSpace γ] (pkg'' : AbstractCompletion.{vγ, uγ} γ) {δ : Type u_1} [TopologicalSpace δ] {f : α → β → γ} {a : δ → pkg.space} {b : δ → pkg'.space} (ha : Continuous a) (hb : Continuous b) : Continuous fun (d : δ) => pkg.map₂ pkg' pkg'' f (a d) (b d)

theorem AbstractCompletion.map₂_coe_coe {α : Type uα} [UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [UniformSpace β] (pkg' : AbstractCompletion.{u_1, uβ} β) {γ : Type uγ} [UniformSpace γ] (pkg'' : AbstractCompletion.{vγ, uγ} γ) (a : α) (b : β) (f : α → β → γ) (hf : UniformContinuous₂ f) : pkg.map₂ pkg' pkg'' f (pkg.coe a) (pkg'.coe b) = pkg''.coe (f a b)