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.
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
Equations
- ⋯ = ⋯
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}
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 α, CauchyFilter.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 (CauchyFilter.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
Embedding of α into its completion CauchyFilter α
Equations
- CauchyFilter.pureCauchy a = ⟨pure a, ⋯⟩
theorem
CauchyFilter.isUniformInducing_pureCauchy
{α : Type u}
[UniformSpace α]
:
IsUniformInducing CauchyFilter.pureCauchy
@[deprecated CauchyFilter.isUniformInducing_pureCauchy]
theorem
CauchyFilter.uniformInducing_pureCauchy
{α : Type u}
[UniformSpace α]
:
IsUniformInducing CauchyFilter.pureCauchy
theorem
CauchyFilter.isUniformEmbedding_pureCauchy
{α : Type u}
[UniformSpace α]
:
IsUniformEmbedding CauchyFilter.pureCauchy
@[deprecated CauchyFilter.isUniformEmbedding_pureCauchy]
theorem
CauchyFilter.uniformEmbedding_pureCauchy
{α : Type u}
[UniformSpace α]
:
IsUniformEmbedding CauchyFilter.pureCauchy
theorem
CauchyFilter.denseRange_pureCauchy
{α : Type u}
[UniformSpace α]
:
DenseRange CauchyFilter.pureCauchy
theorem
CauchyFilter.isDenseInducing_pureCauchy
{α : Type u}
[UniformSpace α]
:
IsDenseInducing CauchyFilter.pureCauchy
theorem
CauchyFilter.isDenseEmbedding_pureCauchy
{α : Type u}
[UniformSpace α]
:
IsDenseEmbedding CauchyFilter.pureCauchy
@[deprecated CauchyFilter.isDenseEmbedding_pureCauchy]
theorem
CauchyFilter.denseEmbedding_pureCauchy
{α : Type u}
[UniformSpace α]
:
IsDenseEmbedding CauchyFilter.pureCauchy
Alias of CauchyFilter.isDenseEmbedding_pureCauchy.
theorem
CauchyFilter.nonempty_cauchyFilter_iff
{α : Type u}
[UniformSpace α]
:
Nonempty (CauchyFilter α) ↔ Nonempty α
Equations
- ⋯ = ⋯
Equations
- CauchyFilter.instInhabited = { default := CauchyFilter.pureCauchy default }
instance
CauchyFilter.instNonempty
{α : Type u}
[UniformSpace α]
[h : Nonempty α]
:
Nonempty (CauchyFilter α)
Equations
- ⋯ = ⋯
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 : α)
:
CauchyFilter.extend f (CauchyFilter.pureCauchy a) = f a
theorem
CauchyFilter.uniformContinuous_extend
{α : Type u}
[UniformSpace α]
{β : Type v}
[UniformSpace β]
[CompleteSpace β]
{f : α → β}
:
theorem
CauchyFilter.inseparable_iff
{α : Type u}
[UniformSpace α]
{f : CauchyFilter α}
{g : CauchyFilter α}
:
Inseparable f g ↔ ↑f ×ˢ ↑g ≤ uniformity α
theorem
CauchyFilter.inseparable_iff_of_le_nhds
{α : Type u}
[UniformSpace α]
{f : CauchyFilter α}
{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 : CauchyFilter α}
{g : CauchyFilter α}
:
Inseparable (lim ↑f) (lim ↑g) ↔ Inseparable f g
theorem
CauchyFilter.cauchyFilter_eq
{α : Type u_1}
[UniformSpace α]
[CompleteSpace α]
[T0Space α]
{f : CauchyFilter α}
{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 (CauchyFilter.pureCauchy a)
Hausdorff completion of α
Equations
Equations
Equations
- UniformSpace.Completion.uniformSpace α = SeparationQuotient.instUniformSpace
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The map from a uniform space to its completion.
porting note: this was added to create a target for the @[coe] attribute.
instance
UniformSpace.Completion.instCoe
(α : Type u_1)
[UniformSpace α]
:
Coe α (UniformSpace.Completion α)
Automatic coercion from α to its completion. Not always injective.
Equations
- UniformSpace.Completion.instCoe α = { coe := ↑α }
@[deprecated UniformSpace.Completion.isUniformInducing_coe]
theorem
UniformSpace.Completion.comap_coe_eq_uniformity
(α : Type u_1)
[UniformSpace α]
:
Filter.comap (fun (p : α × α) => (↑α p.1, ↑α p.2)) (uniformity (UniformSpace.Completion α)) = uniformity α
The Haudorff completion as an abstract completion.
Equations
- UniformSpace.Completion.cPkg = { space := UniformSpace.Completion α, coe := ↑α, uniformStruct := inferInstance, complete := ⋯, separation := ⋯, isUniformInducing := ⋯, dense := ⋯ }
Equations
- UniformSpace.Completion.AbstractCompletion.inhabited α = { default := UniformSpace.Completion.cPkg }
theorem
UniformSpace.Completion.isUniformEmbedding_coe
(α : Type u_1)
[UniformSpace α]
[T0Space α]
:
@[deprecated UniformSpace.Completion.isUniformEmbedding_coe]
def
UniformSpace.Completion.UniformCompletion.completeEquivSelf
{α : Type u_1}
[UniformSpace α]
[CompleteSpace α]
[T0Space α]
:
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 α]
:
Equations
- ⋯ = ⋯
@[deprecated 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 : UniformSpace.Completion α → Prop}
(a : UniformSpace.Completion α)
(hp : IsClosed {a : UniformSpace.Completion α | 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 : UniformSpace.Completion α × UniformSpace.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 : UniformSpace.Completion α → UniformSpace.Completion β → UniformSpace.Completion γ → Prop}
(a : UniformSpace.Completion α)
(b : UniformSpace.Completion β)
(c : UniformSpace.Completion γ)
(hp : IsClosed {x : UniformSpace.Completion α × UniformSpace.Completion β × UniformSpace.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 : 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 = UniformSpace.Completion.cPkg.extend f
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 : α → β}
[T0Space β]
(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 : α → β}
[T0Space β]
[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 β]
[T0Space β]
[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 = UniformSpace.Completion.cPkg.map UniformSpace.Completion.cPkg f
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 γ]
[T0Space γ]
{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.
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 = 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 : β)
:
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 = 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 : α → β → γ)
:
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)