Documentation

Mathlib.Topology.UniformSpace.Completion

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:

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.

def CauchyFilter (α : Type u) [UniformSpace α] :

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
Instances For
    Equations
    • =
    def CauchyFilter.gen {α : Type u} [UniformSpace α] (s : Set (α × α)) :

    The pairs of Cauchy filters generated by a set.

    Equations
    Instances For
      theorem CauchyFilter.monotone_gen {α : Type u} [UniformSpace α] :
      Monotone CauchyFilter.gen
      Equations
      theorem CauchyFilter.basis_uniformity {α : Type u} [UniformSpace α] {ι : Sort u_1} {p : ιProp} {s : ιSet (α × α)} (h : Filter.HasBasis (uniformity α) p s) :
      Filter.HasBasis (uniformity (CauchyFilter α)) 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
      def CauchyFilter.pureCauchy {α : Type u} [UniformSpace α] (a : α) :

      Embedding of α into its completion CauchyFilter α

      Equations
      Instances For
        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
        Equations
        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
        Instances For
          theorem CauchyFilter.extend_pureCauchy {α : Type u} [UniformSpace α] {β : Type v} [UniformSpace β] [T0Space β] {f : αβ} (hf : UniformContinuous f) (a : α) :
          theorem CauchyFilter.inseparable_iff_of_le_nhds {α : Type u} [UniformSpace α] {f : CauchyFilter α} {g : CauchyFilter α} {a : α} {b : α} (ha : f nhds a) (hb : g nhds b) :
          theorem CauchyFilter.cauchyFilter_eq {α : Type u_1} [UniformSpace α] [CompleteSpace α] [T0Space α] {f : CauchyFilter α} {g : CauchyFilter α} :
          lim f = lim g Inseparable f g

          Hausdorff completion of α

          Equations
          Instances For

            The map from a uniform space to its completion.

            porting note: this was added to create a target for the @[coe] attribute.

            Equations
            • α = SeparationQuotient.mk CauchyFilter.pureCauchy
            Instances For

              Automatic coercion from α to its completion. Not always injective.

              Equations
              theorem UniformSpace.Completion.coe_eq (α : Type u_1) [UniformSpace α] :
              α = SeparationQuotient.mk CauchyFilter.pureCauchy
              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 := , uniformInducing := , dense := }
              Instances For

                The uniform bijection between a complete space and its uniform completion.

                Equations
                Instances For
                  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 : αβ) :

                  "Extension" to the completion. It is defined for any map f but returns an arbitrary constant value if f is not uniformly continuous

                  Equations
                  Instances For
                    theorem UniformSpace.Completion.extension_coe {α : Type u_1} [UniformSpace α] {β : Type u_2} [UniformSpace β] {f : αβ} [T0Space β] (hf : UniformContinuous 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)) :

                    Completion functor acting on morphisms

                    Equations
                    Instances For
                      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)) :

                      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
                        Instances For
                          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
                          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
                          Instances For
                            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)