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 }
Instances For
Equations
- ⋯ = ⋯
The pairs of Cauchy filters generated by a set.
Equations
- CauchyFilter.gen s = {p : CauchyFilter α × CauchyFilter α | s ∈ ↑p.1 ×ˢ ↑p.2}
Instances For
Equations
- CauchyFilter.instUniformSpace = UniformSpace.ofCore { uniformity := (uniformity α).lift' CauchyFilter.gen, refl := ⋯, symm := ⋯, comp := ⋯ }
Embedding of α
into its completion CauchyFilter α
Equations
- CauchyFilter.pureCauchy a = ⟨pure a, ⋯⟩
Instances For
Alias of CauchyFilter.isDenseEmbedding_pureCauchy
.
Equations
- ⋯ = ⋯
Equations
- CauchyFilter.instInhabited = { default := CauchyFilter.pureCauchy default }
Equations
- ⋯ = ⋯
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
Instances For
Hausdorff completion of α
Equations
Instances For
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.
Instances For
Automatic coercion from α
to its completion. Not always injective.
Equations
- UniformSpace.Completion.instCoe α = { coe := ↑α }
The Haudorff completion as an abstract completion.
Equations
- UniformSpace.Completion.cPkg = { space := UniformSpace.Completion α, coe := ↑α, uniformStruct := inferInstance, complete := ⋯, separation := ⋯, uniformInducing := ⋯, dense := ⋯ }
Instances For
Equations
- UniformSpace.Completion.AbstractCompletion.inhabited α = { default := UniformSpace.Completion.cPkg }
The uniform bijection between a complete space and its uniform completion.
Equations
- UniformSpace.Completion.UniformCompletion.completeEquivSelf = UniformSpace.Completion.cPkg.compareEquiv AbstractCompletion.ofComplete
Instances For
Equations
- ⋯ = ⋯
"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
Instances For
Completion functor acting on morphisms
Equations
- UniformSpace.Completion.map f = UniformSpace.Completion.cPkg.map UniformSpace.Completion.cPkg f
Instances For
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
Extend a two variable map to the Hausdorff completions.
Equations
- UniformSpace.Completion.extension₂ f = UniformSpace.Completion.cPkg.extend₂ UniformSpace.Completion.cPkg f
Instances For
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