mathlib3 documentation

topology.uniform_space.abstract_completion

Abstract theory of Hausdorff completions of uniform spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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/uniform_space/compare_reals for an example. Of course the comparison comes from the universal property as usual.

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

Implementation notes #

A tiny technical advantage of using a characteristic predicate such as the properties listed in abstract_completion 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 abstract_completion (α : Type u) [uniform_space α] :

Type (u+1)

space : Type ?
coe : α → self.space
uniform_struct : uniform_space self.space
complete : complete_space self.space
separation : separated_space self.space
uniform_inducing : uniform_inducing self.coe
dense : dense_range self.coe

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

Instances for abstract_completion

abstract_completion.has_sizeof_inst
uniform_space.completion.abstract_completion.inhabited

def abstract_completion.of_complete {α : Type u_1} [uniform_space α] [separated_space α] [complete_space α] :

abstract_completion α

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

Equations

abstract_completion.of_complete = {space := α, coe := id α, uniform_struct := infer_instance _inst_1, complete := _, separation := _, uniform_inducing := _, dense := _}

theorem abstract_completion.closure_range {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) :

closure (set.range pkg.coe) = set.univ

theorem abstract_completion.dense_inducing {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) :

dense_inducing pkg.coe

theorem abstract_completion.uniform_continuous_coe {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) :

uniform_continuous pkg.coe

theorem abstract_completion.continuous_coe {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) :

continuous pkg.coe

theorem abstract_completion.induction_on {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {p : pkg.space → Prop} (a : pkg.space) (hp : is_closed {a : pkg.space | p a}) (ih : ∀ (a : α), p (pkg.coe a)) :

p a

@[protected]

theorem abstract_completion.funext {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [topological_space β] [t2_space β] {f g : pkg.space → β} (hf : continuous f) (hg : continuous g) (h : ∀ (a : α), f (pkg.coe a) = g (pkg.coe a)) :

f = g

@[protected]

noncomputable def abstract_completion.extend {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (f : α → β) :

pkg.space → β

Extension of maps to completions

Equations

pkg.extend f = ite (uniform_continuous f) (_.extend f) (λ (x : pkg.space), f (_.some x))

theorem abstract_completion.extend_def {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] {f : α → β} (hf : uniform_continuous f) :

pkg.extend f = _.extend f

theorem abstract_completion.extend_coe {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] {f : α → β} [t2_space β] (hf : uniform_continuous f) (a : α) :

pkg.extend f (pkg.coe a) = f a

theorem abstract_completion.uniform_continuous_extend {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] {f : α → β} [complete_space β] :

uniform_continuous (pkg.extend f)

theorem abstract_completion.continuous_extend {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] {f : α → β} [complete_space β] :

continuous (pkg.extend f)

theorem abstract_completion.extend_unique {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] {f : α → β} [complete_space β] [separated_space β] (hf : uniform_continuous f) {g : pkg.space → β} (hg : uniform_continuous g) (h : ∀ (a : α), f a = g (pkg.coe a)) :

pkg.extend f = g

@[simp]

theorem abstract_completion.extend_comp_coe {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] [complete_space β] [separated_space β] {f : pkg.space → β} (hf : uniform_continuous f) :

pkg.extend (f ∘ pkg.coe) = f

@[protected]

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

pkg.space → pkg'.space

Lifting maps to completions

Equations

pkg.map pkg' f = pkg.extend (pkg'.coe ∘ f)

theorem abstract_completion.uniform_continuous_map {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) (f : α → β) :

uniform_continuous (pkg.map pkg' f)

theorem abstract_completion.continuous_map {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) (f : α → β) :

continuous (pkg.map pkg' f)

@[simp]

theorem abstract_completion.map_coe {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) {f : α → β} (hf : uniform_continuous f) (a : α) :

pkg.map pkg' f (pkg.coe a) = pkg'.coe (f a)

theorem abstract_completion.map_unique {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) {f : α → β} {g : pkg.space → pkg'.space} (hg : uniform_continuous g) (h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)) :

pkg.map pkg' f = g

@[simp]

theorem abstract_completion.map_id {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) :

pkg.map pkg id = id

theorem abstract_completion.extend_map {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) {γ : Type u_3} [uniform_space γ] [complete_space γ] [separated_space γ] {f : β → γ} {g : α → β} (hf : uniform_continuous f) (hg : uniform_continuous g) :

pkg'.extend f ∘ pkg.map pkg' g = pkg.extend (f ∘ g)

theorem abstract_completion.map_comp {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) {γ : Type u_3} [uniform_space γ] (pkg'' : abstract_completion γ) {g : β → γ} {f : α → β} (hg : uniform_continuous g) (hf : uniform_continuous f) :

pkg'.map pkg'' g ∘ pkg.map pkg' f = pkg.map pkg'' (g ∘ f)

noncomputable def abstract_completion.compare {α : Type u_1} [uniform_space α] (pkg pkg' : abstract_completion α) :

pkg.space → pkg'.space

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

Equations

pkg.compare pkg' = pkg.extend pkg'.coe

theorem abstract_completion.uniform_continuous_compare {α : Type u_1} [uniform_space α] (pkg pkg' : abstract_completion α) :

uniform_continuous (pkg.compare pkg')

theorem abstract_completion.compare_coe {α : Type u_1} [uniform_space α] (pkg pkg' : abstract_completion α) (a : α) :

pkg.compare pkg' (pkg.coe a) = pkg'.coe a

theorem abstract_completion.inverse_compare {α : Type u_1} [uniform_space α] (pkg pkg' : abstract_completion α) :

pkg.compare pkg' ∘ pkg'.compare pkg = id

noncomputable def abstract_completion.compare_equiv {α : Type u_1} [uniform_space α] (pkg pkg' : abstract_completion α) :

pkg.space ≃ᵤ pkg'.space

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

Equations

pkg.compare_equiv pkg' = {to_equiv := {to_fun := pkg.compare pkg', inv_fun := pkg'.compare pkg, left_inv := _, right_inv := _}, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}

theorem abstract_completion.uniform_continuous_compare_equiv {α : Type u_1} [uniform_space α] (pkg pkg' : abstract_completion α) :

uniform_continuous ⇑(pkg.compare_equiv pkg')

theorem abstract_completion.uniform_continuous_compare_equiv_symm {α : Type u_1} [uniform_space α] (pkg pkg' : abstract_completion α) :

uniform_continuous ⇑((pkg.compare_equiv pkg').symm)

@[protected]

def abstract_completion.prod {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) :

abstract_completion (α × β)

Products of completions

Equations

pkg.prod pkg' = {space := pkg.space × pkg'.space, coe := λ (p : α × β), (pkg.coe p.fst, pkg'.coe p.snd), uniform_struct := prod.uniform_space pkg'.uniform_struct, complete := _, separation := _, uniform_inducing := _, dense := _}

@[protected]

noncomputable def abstract_completion.extend₂ {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) {γ : Type u_3} [uniform_space γ] (f : α → β → γ) :

pkg.space → pkg'.space → γ

Extend two variable map to completions.

Equations

pkg.extend₂ pkg' f = function.curry ((pkg.prod pkg').extend (function.uncurry f))

theorem abstract_completion.extension₂_coe_coe {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) {γ : Type u_3} [uniform_space γ] [separated_space γ] {f : α → β → γ} (hf : uniform_continuous (function.uncurry f)) (a : α) (b : β) :

pkg.extend₂ pkg' f (pkg.coe a) (pkg'.coe b) = f a b

theorem abstract_completion.uniform_continuous_extension₂ {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) {γ : Type u_3} [uniform_space γ] (f : α → β → γ) [complete_space γ] :

uniform_continuous₂ (pkg.extend₂ pkg' f)

@[protected]

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

pkg.space → pkg'.space → pkg''.space

Lift two variable maps to completions.

Equations

pkg.map₂ pkg' pkg'' f = pkg.extend₂ pkg' (function.bicompr pkg''.coe f)

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

uniform_continuous₂ (pkg.map₂ pkg' pkg'' f)

theorem abstract_completion.continuous_map₂ {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) {γ : Type u_3} [uniform_space γ] (pkg'' : abstract_completion γ) {δ : Type u_4} [topological_space δ] {f : α → β → γ} {a : δ → pkg.space} {b : δ → pkg'.space} (ha : continuous a) (hb : continuous b) :

continuous (λ (d : δ), pkg.map₂ pkg' pkg'' f (a d) (b d))

theorem abstract_completion.map₂_coe_coe {α : Type u_1} [uniform_space α] (pkg : abstract_completion α) {β : Type u_2} [uniform_space β] (pkg' : abstract_completion β) {γ : Type u_3} [uniform_space γ] (pkg'' : abstract_completion γ) (a : α) (b : β) (f : α → β → γ) (hf : uniform_continuous₂ f) :

pkg.map₂ pkg' pkg'' f (pkg.coe a) (pkg'.coe b) = pkg''.coe (f a b)