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.uniform_space.basic.
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 // Cauchy f }
Instances For
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 | s ∈ ↑p.fst ×ˢ ↑p.snd}
Instances For
Equations
- One or more equations did not get rendered due to their size.
theorem
CauchyFilter.mem_uniformity
{α : Type u}
[UniformSpace α]
{s : Set (CauchyFilter α × CauchyFilter α)}
:
s ∈ uniformity (CauchyFilter α) ↔ ∃ t, t ∈ uniformity α ∧ CauchyFilter.gen t ⊆ s
theorem
CauchyFilter.mem_uniformity'
{α : Type u}
[UniformSpace α]
{s : Set (CauchyFilter α × CauchyFilter α)}
:
s ∈ uniformity (CauchyFilter α) ↔ ∃ t, t ∈ uniformity α ∧ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
Embedding of α into its completion CauchyFilter α
Equations
- CauchyFilter.pureCauchy a = { val := pure a, property := (_ : Cauchy (pure a)) }
Instances For
theorem
CauchyFilter.uniformInducing_pureCauchy
{α : Type u}
[UniformSpace α]
:
UniformInducing CauchyFilter.pureCauchy
theorem
CauchyFilter.uniformEmbedding_pureCauchy
{α : Type u}
[UniformSpace α]
:
UniformEmbedding CauchyFilter.pureCauchy
theorem
CauchyFilter.denseRange_pureCauchy
{α : Type u}
[UniformSpace α]
:
DenseRange CauchyFilter.pureCauchy
theorem
CauchyFilter.denseInducing_pureCauchy
{α : Type u}
[UniformSpace α]
:
DenseInducing CauchyFilter.pureCauchy
theorem
CauchyFilter.denseEmbedding_pureCauchy
{α : Type u}
[UniformSpace α]
:
DenseEmbedding CauchyFilter.pureCauchy
theorem
CauchyFilter.nonempty_cauchyFilter_iff
{α : Type u}
[UniformSpace α]
:
Nonempty (CauchyFilter α) ↔ Nonempty α
instance
CauchyFilter.instCompleteSpaceCauchyFilterInstUniformSpaceCauchyFilter
{α : Type u}
[UniformSpace α]
:
Equations
- CauchyFilter.instInhabitedCauchyFilter = { default := CauchyFilter.pureCauchy default }
instance
CauchyFilter.instNonemptyCauchyFilter
{α : 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 DenseInducing.extend (_ : DenseInducing CauchyFilter.pureCauchy) f else fun x => f (Nonempty.some (_ : Nonempty α))
Instances For
theorem
CauchyFilter.extend_pureCauchy
{α : Type u}
[UniformSpace α]
{β : Type v}
[UniformSpace β]
[SeparatedSpace β]
{f : α → β}
(hf : UniformContinuous f)
(a : α)
:
CauchyFilter.extend f (CauchyFilter.pureCauchy a) = f a
theorem
CauchyFilter.uniformContinuous_extend
{α : Type u}
[UniformSpace α]
{β : Type v}
[UniformSpace β]
[CompleteSpace β]
{f : α → β}
:
theorem
CauchyFilter.cauchyFilter_eq
{α : Type u_1}
[Inhabited α]
[UniformSpace α]
[CompleteSpace α]
[SeparatedSpace α]
{f : CauchyFilter α}
{g : CauchyFilter α}
:
lim ↑f = lim ↑g ↔ (f, g) ∈ separationRel (CauchyFilter α)
theorem
CauchyFilter.separated_pureCauchy_injective
{α : Type u_1}
[UniformSpace α]
[s : SeparatedSpace α]
:
instance
UniformSpace.completeSpace_separation
(α : Type u_1)
[UniformSpace α]
[h : CompleteSpace α]
:
Hausdorff completion of α
Equations
Instances For
Equations
Equations
- UniformSpace.Completion.uniformSpace α = UniformSpace.separationSetoid.uniformSpace
The map from a uniform space to its completion.
porting note: this was added to create a target for the @[coe] attribute.
Instances For
instance
UniformSpace.Completion.instCoeCompletion
(α : Type u_1)
[UniformSpace α]
:
Coe α (UniformSpace.Completion α)
Automatic coercion from α to its completion. Not always injective.
Equations
- UniformSpace.Completion.instCoeCompletion α = { coe := ↑α }
theorem
UniformSpace.Completion.comap_coe_eq_uniformity
(α : Type u_1)
[UniformSpace α]
:
Filter.comap (fun p => (↑α p.fst, ↑α p.snd)) (uniformity (UniformSpace.Completion α)) = uniformity α
The Haudorff completion as an abstract completion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- UniformSpace.Completion.AbstractCompletion.inhabited α = { default := UniformSpace.Completion.cPkg }
theorem
UniformSpace.Completion.uniformEmbedding_coe
(α : Type u_1)
[UniformSpace α]
[SeparatedSpace α]
:
def
UniformSpace.Completion.UniformCompletion.completeEquivSelf
{α : Type u_1}
[UniformSpace α]
[CompleteSpace α]
[SeparatedSpace α]
:
The uniform bijection between a complete space and its uniform completion.
Equations
- UniformSpace.Completion.UniformCompletion.completeEquivSelf = AbstractCompletion.compareEquiv UniformSpace.Completion.cPkg AbstractCompletion.ofComplete
Instances For
instance
UniformSpace.Completion.separableSpace_completion
{α : Type u_1}
[UniformSpace α]
[TopologicalSpace.SeparableSpace α]
:
theorem
UniformSpace.Completion.denseEmbedding_coe
{α : Type u_1}
[UniformSpace α]
[SeparatedSpace α]
:
theorem
UniformSpace.Completion.denseRange_coe₂
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
:
DenseRange fun x => (↑α x.fst, ↑β x.snd)
theorem
UniformSpace.Completion.denseRange_coe₃
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{γ : Type u_3}
[UniformSpace γ]
:
DenseRange fun x => (↑α x.fst, ↑β x.snd.fst, ↑γ x.snd.snd)
theorem
UniformSpace.Completion.induction_on
{α : Type u_1}
[UniformSpace α]
{p : UniformSpace.Completion α → Prop}
(a : UniformSpace.Completion α)
(hp : IsClosed {a | p a})
(ih : (a : α) → p (↑α a))
:
p a
theorem
UniformSpace.Completion.induction_on₂
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{p : UniformSpace.Completion α → UniformSpace.Completion β → Prop}
(a : UniformSpace.Completion α)
(b : UniformSpace.Completion β)
(hp : IsClosed {x | p x.fst x.snd})
(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 : UniformSpace.Completion α → UniformSpace.Completion β → UniformSpace.Completion γ → Prop}
(a : UniformSpace.Completion α)
(b : UniformSpace.Completion β)
(c : UniformSpace.Completion γ)
(hp : IsClosed {x | p x.fst x.snd.fst x.snd.snd})
(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 : UniformSpace.Completion α → Y}
{g : UniformSpace.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 : UniformSpace.Completion α → Y}
{g : UniformSpace.Completion α → Y}
(hf : Continuous f)
(hg : Continuous g)
(h : ∀ (a : α), f (↑α a) = g (↑α a))
(a : UniformSpace.Completion α)
:
f a = g a
def
UniformSpace.Completion.extension
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
(f : α → β)
:
UniformSpace.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 = AbstractCompletion.extend UniformSpace.Completion.cPkg f
Instances For
theorem
UniformSpace.Completion.uniformContinuous_extension
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{f : α → β}
[CompleteSpace β]
:
theorem
UniformSpace.Completion.continuous_extension
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{f : α → β}
[CompleteSpace β]
:
theorem
UniformSpace.Completion.extension_coe
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{f : α → β}
[SeparatedSpace β]
(hf : UniformContinuous f)
(a : α)
:
UniformSpace.Completion.extension f (↑α a) = f a
theorem
UniformSpace.Completion.extension_unique
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{f : α → β}
[SeparatedSpace β]
[CompleteSpace β]
(hf : UniformContinuous f)
{g : UniformSpace.Completion α → β}
(hg : UniformContinuous g)
(h : ∀ (a : α), f a = g (↑α a))
:
@[simp]
theorem
UniformSpace.Completion.extension_comp_coe
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
[SeparatedSpace β]
[CompleteSpace β]
{f : UniformSpace.Completion α → β}
(hf : UniformContinuous f)
:
UniformSpace.Completion.extension (f ∘ ↑α) = f
def
UniformSpace.Completion.map
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
(f : α → β)
:
Completion functor acting on morphisms
Equations
- UniformSpace.Completion.map f = AbstractCompletion.map UniformSpace.Completion.cPkg UniformSpace.Completion.cPkg f
Instances For
theorem
UniformSpace.Completion.uniformContinuous_map
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{f : α → β}
:
theorem
UniformSpace.Completion.continuous_map
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{f : α → β}
:
theorem
UniformSpace.Completion.map_coe
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{f : α → β}
(hf : UniformContinuous f)
(a : α)
:
UniformSpace.Completion.map f (↑α a) = ↑β (f a)
theorem
UniformSpace.Completion.map_unique
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{f : α → β}
{g : UniformSpace.Completion α → UniformSpace.Completion β}
(hg : UniformContinuous g)
(h : ∀ (a : α), ↑β (f a) = g (↑α a))
:
@[simp]
theorem
UniformSpace.Completion.map_id
{α : Type u_1}
[UniformSpace α]
:
UniformSpace.Completion.map id = id
theorem
UniformSpace.Completion.extension_map
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{γ : Type u_3}
[UniformSpace γ]
[CompleteSpace γ]
[SeparatedSpace γ]
{f : β → γ}
{g : α → β}
(hf : UniformContinuous f)
(hg : UniformContinuous 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)
:
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.
Instances For
def
UniformSpace.Completion.extension₂
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{γ : Type u_3}
[UniformSpace γ]
(f : α → β → γ)
:
Extend a two variable map to the Hausdorff completions.
Equations
- UniformSpace.Completion.extension₂ f = AbstractCompletion.extend₂ UniformSpace.Completion.cPkg UniformSpace.Completion.cPkg f
Instances For
theorem
UniformSpace.Completion.extension₂_coe_coe
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{γ : Type u_3}
[UniformSpace γ]
{f : α → β → γ}
[SeparatedSpace γ]
(hf : UniformContinuous₂ f)
(a : α)
(b : β)
:
UniformSpace.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 γ]
:
def
UniformSpace.Completion.map₂
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{γ : Type u_3}
[UniformSpace γ]
(f : α → β → γ)
:
Lift a two variable map to the Hausdorff completions.
Equations
- UniformSpace.Completion.map₂ f = AbstractCompletion.map₂ UniformSpace.Completion.cPkg UniformSpace.Completion.cPkg UniformSpace.Completion.cPkg f
Instances For
theorem
UniformSpace.Completion.uniformContinuous_map₂
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{γ : Type u_3}
[UniformSpace γ]
(f : α → β → γ)
:
theorem
UniformSpace.Completion.continuous_map₂
{α : Type u_1}
[UniformSpace α]
{β : Type u_2}
[UniformSpace β]
{γ : Type u_3}
[UniformSpace γ]
{δ : Type u_4}
[TopologicalSpace δ]
{f : α → β → γ}
{a : δ → UniformSpace.Completion α}
{b : δ → UniformSpace.Completion β}
(ha : Continuous a)
(hb : Continuous b)
:
Continuous fun d => UniformSpace.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)
:
UniformSpace.Completion.map₂ f (↑α a) (↑β b) = ↑γ (f a b)