Documentation

Mathlib.Topology.UniformSpace.AbstractCompletion

Abstract theory of Hausdorff completions of uniform spaces #

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

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

Implementation notes #

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

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 α.

  • space : Type u

    The underlying space of the completion.

  • coe : αself.space

    A map from a space to its completion.

  • uniformStruct : UniformSpace self.space

    The completion carries a uniform structure.

  • complete : CompleteSpace self.space

    The completion is complete.

  • separation : T0Space self.space

    The completion is a T₀ space.

  • uniformInducing : UniformInducing self.coe

    The map into the completion is uniform-inducing.

  • dense : DenseRange self.coe

    The map into the completion has dense range.

Instances For
    theorem AbstractCompletion.complete {α : Type u} [UniformSpace α] (self : AbstractCompletion α) :
    CompleteSpace self.space

    The completion is complete.

    theorem AbstractCompletion.separation {α : Type u} [UniformSpace α] (self : AbstractCompletion α) :
    T0Space self.space

    The completion is a T₀ space.

    The map into the completion is uniform-inducing.

    theorem AbstractCompletion.dense {α : Type u} [UniformSpace α] (self : AbstractCompletion α) :
    DenseRange self.coe

    The map into the completion has dense range.

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

    Equations
    • AbstractCompletion.ofComplete = { space := α, coe := id, uniformStruct := inferInstance, complete := , separation := , uniformInducing := , dense := }
    Instances For
      theorem AbstractCompletion.closure_range {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) :
      closure (Set.range pkg.coe) = Set.univ
      theorem AbstractCompletion.induction_on {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {p : pkg.spaceProp} (a : pkg.space) (hp : IsClosed {a : pkg.space | p a}) (ih : ∀ (a : α), p (pkg.coe a)) :
      p a
      theorem AbstractCompletion.funext {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [TopologicalSpace β] [T2Space β] {f : pkg.spaceβ} {g : pkg.spaceβ} (hf : Continuous f) (hg : Continuous g) (h : ∀ (a : α), f (pkg.coe a) = g (pkg.coe a)) :
      f = g
      def AbstractCompletion.extend {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (f : αβ) :
      pkg.spaceβ

      Extension of maps to completions

      Equations
      • pkg.extend f = if UniformContinuous f then .extend f else fun (x : pkg.space) => f (.some x)
      Instances For
        theorem AbstractCompletion.extend_def {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] {f : αβ} (hf : UniformContinuous f) :
        pkg.extend f = .extend f
        theorem AbstractCompletion.extend_coe {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] {f : αβ} [T2Space β] (hf : UniformContinuous f) (a : α) :
        pkg.extend f (pkg.coe a) = f a
        theorem AbstractCompletion.uniformContinuous_extend {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] {f : αβ} [CompleteSpace β] :
        UniformContinuous (pkg.extend f)
        theorem AbstractCompletion.continuous_extend {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] {f : αβ} [CompleteSpace β] :
        Continuous (pkg.extend f)
        theorem AbstractCompletion.extend_unique {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] {f : αβ} [CompleteSpace β] [T0Space β] (hf : UniformContinuous f) {g : pkg.spaceβ} (hg : UniformContinuous g) (h : ∀ (a : α), f a = g (pkg.coe a)) :
        pkg.extend f = g
        @[simp]
        theorem AbstractCompletion.extend_comp_coe {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] [CompleteSpace β] [T0Space β] {f : pkg.spaceβ} (hf : UniformContinuous f) :
        pkg.extend (f pkg.coe) = f
        def AbstractCompletion.map {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) (f : αβ) :
        pkg.spacepkg'.space

        Lifting maps to completions

        Equations
        • pkg.map pkg' f = pkg.extend (pkg'.coe f)
        Instances For
          theorem AbstractCompletion.uniformContinuous_map {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) (f : αβ) :
          UniformContinuous (pkg.map pkg' f)
          theorem AbstractCompletion.continuous_map {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) (f : αβ) :
          Continuous (pkg.map pkg' f)
          @[simp]
          theorem AbstractCompletion.map_coe {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {f : αβ} (hf : UniformContinuous f) (a : α) :
          pkg.map pkg' f (pkg.coe a) = pkg'.coe (f a)
          theorem AbstractCompletion.map_unique {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {f : αβ} {g : pkg.spacepkg'.space} (hg : UniformContinuous g) (h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)) :
          pkg.map pkg' f = g
          @[simp]
          theorem AbstractCompletion.map_id {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) :
          pkg.map pkg id = id
          theorem AbstractCompletion.extend_map {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {γ : Type u_3} [UniformSpace γ] [CompleteSpace γ] [T0Space γ] {f : βγ} {g : αβ} (hf : UniformContinuous f) (hg : UniformContinuous g) :
          pkg'.extend f pkg.map pkg' g = pkg.extend (f g)
          theorem AbstractCompletion.map_comp {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {γ : Type u_3} [UniformSpace γ] (pkg'' : AbstractCompletion γ) {g : βγ} {f : αβ} (hg : UniformContinuous g) (hf : UniformContinuous f) :
          pkg'.map pkg'' g pkg.map pkg' f = pkg.map pkg'' (g f)
          def AbstractCompletion.compare {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) (pkg' : AbstractCompletion α) :
          pkg.spacepkg'.space

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

          Equations
          • pkg.compare pkg' = pkg.extend pkg'.coe
          Instances For
            theorem AbstractCompletion.compare_coe {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) (pkg' : AbstractCompletion α) (a : α) :
            pkg.compare pkg' (pkg.coe a) = pkg'.coe a
            theorem AbstractCompletion.inverse_compare {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) (pkg' : AbstractCompletion α) :
            pkg.compare pkg' pkg'.compare pkg = id
            def AbstractCompletion.compareEquiv {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) (pkg' : AbstractCompletion α) :
            pkg.space ≃ᵤ pkg'.space

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

            Equations
            • pkg.compareEquiv pkg' = { toFun := pkg.compare pkg', invFun := pkg'.compare pkg, left_inv := , right_inv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
            Instances For
              theorem AbstractCompletion.compare_comp_eq_compare {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) (pkg' : AbstractCompletion α) (γ : Type u_3) [TopologicalSpace γ] [T3Space γ] {f : αγ} (cont_f : Continuous f) :
              (∀ (a : pkg.space), Filter.Tendsto f (Filter.comap pkg.coe (nhds a)) (nhds (.extend f a))).extend f pkg'.compare pkg = .extend f
              def AbstractCompletion.prod {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) :

              Products of completions

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def AbstractCompletion.extend₂ {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {γ : Type u_3} [UniformSpace γ] (f : αβγ) :
                pkg.spacepkg'.spaceγ

                Extend two variable map to completions.

                Equations
                Instances For
                  theorem AbstractCompletion.extension₂_coe_coe {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {γ : Type u_3} [UniformSpace γ] [T0Space γ] {f : αβγ} (hf : UniformContinuous (Function.uncurry f)) (a : α) (b : β) :
                  pkg.extend₂ pkg' f (pkg.coe a) (pkg'.coe b) = f a b
                  theorem AbstractCompletion.uniformContinuous_extension₂ {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {γ : Type u_3} [UniformSpace γ] (f : αβγ) [CompleteSpace γ] :
                  UniformContinuous₂ (pkg.extend₂ pkg' f)
                  def AbstractCompletion.map₂ {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {γ : Type u_3} [UniformSpace γ] (pkg'' : AbstractCompletion γ) (f : αβγ) :
                  pkg.spacepkg'.spacepkg''.space

                  Lift two variable maps to completions.

                  Equations
                  Instances For
                    theorem AbstractCompletion.uniformContinuous_map₂ {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {γ : Type u_3} [UniformSpace γ] (pkg'' : AbstractCompletion γ) (f : αβγ) :
                    UniformContinuous₂ (pkg.map₂ pkg' pkg'' f)
                    theorem AbstractCompletion.continuous_map₂ {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {γ : Type u_3} [UniformSpace γ] (pkg'' : AbstractCompletion γ) {δ : Type u_4} [TopologicalSpace δ] {f : αβγ} {a : δpkg.space} {b : δpkg'.space} (ha : Continuous a) (hb : Continuous b) :
                    Continuous fun (d : δ) => pkg.map₂ pkg' pkg'' f (a d) (b d)
                    theorem AbstractCompletion.map₂_coe_coe {α : Type u_1} [UniformSpace α] (pkg : AbstractCompletion α) {β : Type u_2} [UniformSpace β] (pkg' : AbstractCompletion β) {γ : Type u_3} [UniformSpace γ] (pkg'' : AbstractCompletion γ) (a : α) (b : β) (f : αβγ) (hf : UniformContinuous₂ f) :
                    pkg.map₂ pkg' pkg'' f (pkg.coe a) (pkg'.coe b) = pkg''.coe (f a b)