Mathlib.Topology.UniformSpace.AbstractCompletion

Module docstring

{"# 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 "}

AbstractCompletion structure

(α : Type u) [UniformSpace α]

Full source

/-- 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 `α`. -/
structure AbstractCompletion (α : Type u) [UniformSpace α] where
  /-- The underlying space of the completion. -/
  space : Type u
  /-- A map from a space to its completion. -/
  coe : α → space
  /-- The completion carries a uniform structure. -/
  uniformStruct : UniformSpace space
  /-- The completion is complete. -/
  complete : CompleteSpace space
  /-- The completion is a T₀ space. -/
  separation : T0Space space
  /-- The map into the completion is uniform-inducing. -/
  isUniformInducing : IsUniformInducing coe
  /-- The map into the completion has dense range. -/
  dense : DenseRange coe

Abstract Completion of a Uniform Space

Informal description

An abstract completion of a uniform space $\alpha$ consists of a complete Hausdorff uniform space (from the same universe) together with a map from $\alpha$ that has dense range and induces the original uniform structure on $\alpha$.

AbstractCompletion.ofComplete definition

[T0Space α] [CompleteSpace α] : AbstractCompletion α

Full source

/-- If `α` is complete, then it is an abstract completion of itself. -/
def ofComplete [T0Space α] [CompleteSpace α] : AbstractCompletion α :=
  mk α id inferInstance inferInstance inferInstance .id denseRange_id

Identity as Abstract Completion of a Complete Space

Informal description

Given a complete Hausdorff uniform space $\alpha$, the identity map $\text{id} \colon \alpha \to \alpha$ equips $\alpha$ with the structure of an abstract completion of itself. This means that $\alpha$ satisfies the universal property of being its own completion, with the identity map serving as the canonical embedding.

AbstractCompletion.closure_range theorem

: closure (range ι) = univ

Full source

theorem closure_range : closure (range ι) = univ :=
  pkg.dense.closure_range

Density of the Inclusion Map in Abstract Completion

Informal description

The closure of the range of the inclusion map $\iota \colon \alpha \to \hat{\alpha}$ from a uniform space $\alpha$ to its abstract completion $\hat{\alpha}$ is equal to the entire space $\hat{\alpha}$.

AbstractCompletion.isDenseInducing theorem

: IsDenseInducing ι

Full source

theorem isDenseInducing : IsDenseInducing ι :=
  ⟨pkg.isUniformInducing.isInducing, pkg.dense⟩

Dense Inducing Property of Completion Inclusion Map

Informal description

The inclusion map $\iota$ from a uniform space $\alpha$ to its abstract completion $\hat{\alpha}$ is a dense inducing map, meaning that the image of $\alpha$ under $\iota$ is dense in $\hat{\alpha}$ and the topology on $\alpha$ is induced by $\iota$.

AbstractCompletion.uniformContinuous_coe theorem

: UniformContinuous ι

Full source

theorem uniformContinuous_coe : UniformContinuous ι :=
  IsUniformInducing.uniformContinuous pkg.isUniformInducing

Uniform Continuity of the Completion Inclusion Map

Informal description

The inclusion map $\iota$ from a uniform space $\alpha$ to its abstract completion $\hat{\alpha}$ is uniformly continuous.

AbstractCompletion.continuous_coe theorem

: Continuous ι

Full source

theorem continuous_coe : Continuous ι :=
  pkg.uniformContinuous_coe.continuous

Continuity of the Completion Inclusion Map

Informal description

The inclusion map $\iota$ from a uniform space $\alpha$ to its abstract completion $\hat{\alpha}$ is continuous.

AbstractCompletion.induction_on theorem

{p : hatα → Prop} (a : hatα) (hp : IsClosed {a | p a}) (ih : ∀ a, p (ι a)) : p a

Full source

@[elab_as_elim]
theorem induction_on {p : hatα → Prop} (a : hatα) (hp : IsClosed { a | p a }) (ih : ∀ a, p (ι a)) :
    p a :=
  isClosed_property pkg.dense hp ih a

Induction Principle for Abstract Completion

Informal description

Let $\hat{\alpha}$ be an abstract completion of a uniform space $\alpha$ with inclusion map $\iota : \alpha \to \hat{\alpha}$. For any predicate $p : \hat{\alpha} \to \text{Prop}$ such that the set $\{a \in \hat{\alpha} \mid p(a)\}$ is closed, and for any $a \in \hat{\alpha}$, if $p(\iota(b))$ holds for all $b \in \alpha$, then $p(a)$ holds.

AbstractCompletion.funext theorem

 [TopologicalSpace β] [T2Space β] {f g : hatα → β} (hf : Continuous f) (hg : Continuous g)
  (h : ∀ a, f (ι a) = g (ι a)) : f = g

Full source

protected theorem funext [TopologicalSpace β] [T2Space β] {f g : hatα → β} (hf : Continuous f)
    (hg : Continuous g) (h : ∀ a, f (ι a) = g (ι a)) : f = g :=
  funext fun a => pkg.induction_on a (isClosed_eq hf hg) h

Uniqueness of Continuous Extensions from Abstract Completion to Hausdorff Space

Informal description

Let $\hat{\alpha}$ be an abstract completion of a uniform space $\alpha$ with inclusion map $\iota : \alpha \to \hat{\alpha}$. Let $\beta$ be a Hausdorff topological space, and let $f, g : \hat{\alpha} \to \beta$ be continuous functions. If $f \circ \iota = g \circ \iota$, then $f = g$.

AbstractCompletion.extend definition

(f : α → β) : hatα → β

Full source

/-- Extension of maps to completions -/
protected def extend (f : α → β) : hatα → β :=
  open scoped Classical in
  if UniformContinuous f then pkg.isDenseInducing.extend f else fun x => f (pkg.dense.some x)

Extension of maps to completions

Informal description

Given a uniform space $\alpha$ with an abstract completion $\hat{\alpha}$ and a map $f : \alpha \to \beta$, the function `AbstractCompletion.extend` extends $f$ to a map $\hat{\alpha} \to \beta$. If $f$ is uniformly continuous, the extension is constructed using the dense inducing property of the inclusion map $\iota : \alpha \to \hat{\alpha}$. Otherwise, the extension is defined pointwise by choosing a preimage in $\alpha$ for each point in $\hat{\alpha}$ using the axiom of choice (since $\iota$ has dense range).

AbstractCompletion.extend_def theorem

(hf : UniformContinuous f) : pkg.extend f = pkg.isDenseInducing.extend f

Full source

theorem extend_def (hf : UniformContinuous f) : pkg.extend f = pkg.isDenseInducing.extend f :=
  if_pos hf

Extension of Uniformly Continuous Maps via Dense Inducing Property

Informal description

Let $\alpha$ be a uniform space with an abstract completion $\hat{\alpha}$ and inclusion map $\iota : \alpha \to \hat{\alpha}$. Given a uniformly continuous map $f : \alpha \to \beta$, the extension $\text{extend}(f) : \hat{\alpha} \to \beta$ coincides with the extension obtained via the dense inducing property of $\iota$.

AbstractCompletion.extend_coe theorem

[T2Space β] (hf : UniformContinuous f) (a : α) : (pkg.extend f) (ι a) = f a

Full source

theorem extend_coe [T2Space β] (hf : UniformContinuous f) (a : α) : (pkg.extend f) (ι a) = f a := by
  rw [pkg.extend_def hf]
  exact pkg.isDenseInducing.extend_eq hf.continuous a

Extension of Uniformly Continuous Maps Preserves Values on Original Space

Informal description

Let $\alpha$ be a uniform space with an abstract completion $\hat{\alpha}$ and inclusion map $\iota : \alpha \to \hat{\alpha}$. Given a Hausdorff space $\beta$ and a uniformly continuous map $f : \alpha \to \beta$, the extension $\text{extend}(f) : \hat{\alpha} \to \beta$ satisfies $\text{extend}(f)(\iota(a)) = f(a)$ for every $a \in \alpha$.

AbstractCompletion.uniformContinuous_extend theorem

: UniformContinuous (pkg.extend f)

Full source

theorem uniformContinuous_extend : UniformContinuous (pkg.extend f) := by
  by_cases hf : UniformContinuous f
  · rw [pkg.extend_def hf]
    exact uniformContinuous_uniformly_extend pkg.isUniformInducing pkg.dense hf
  · unfold AbstractCompletion.extend
    rw [if_neg hf]
    exact uniformContinuous_of_const fun a b => by congr 1

Uniform Continuity of the Extension Map

Informal description

The extension map $\text{extend}(f) : \hat{\alpha} \to \beta$ is uniformly continuous when $f : \alpha \to \beta$ is uniformly continuous.

AbstractCompletion.continuous_extend theorem

: Continuous (pkg.extend f)

Full source

theorem continuous_extend : Continuous (pkg.extend f) :=
  pkg.uniformContinuous_extend.continuous

Continuity of the Extension Map from a Uniform Space Completion

Informal description

The extension map $\text{extend}(f) : \hat{\alpha} \to \beta$ is continuous when $f : \alpha \to \beta$ is uniformly continuous.

AbstractCompletion.extend_unique theorem

 (hf : UniformContinuous f) {g : hatα → β} (hg : UniformContinuous g) (h : ∀ a : α, f a = g (ι a)) : pkg.extend f = g

Full source

theorem extend_unique (hf : UniformContinuous f) {g : hatα → β} (hg : UniformContinuous g)
    (h : ∀ a : α, f a = g (ι a)) : pkg.extend f = g := by
  apply pkg.funext pkg.continuous_extend hg.continuous
  simpa only [pkg.extend_coe hf] using h

Uniqueness of Uniformly Continuous Extensions to Completion

Informal description

Let $\alpha$ be a uniform space with an abstract completion $\hat{\alpha}$ and inclusion map $\iota : \alpha \to \hat{\alpha}$. Let $\beta$ be a complete Hausdorff uniform space, and let $f : \alpha \to \beta$ be a uniformly continuous map. If $g : \hat{\alpha} \to \beta$ is a uniformly continuous extension of $f$ (i.e., $f(a) = g(\iota(a))$ for all $a \in \alpha$), then the canonical extension $\text{extend}(f)$ equals $g$.

AbstractCompletion.extend_comp_coe theorem

{f : hatα → β} (hf : UniformContinuous f) : pkg.extend (f ∘ ι) = f

Full source

@[simp]
theorem extend_comp_coe {f : hatα → β} (hf : UniformContinuous f) : pkg.extend (f ∘ ι) = f :=
  funext fun x =>
    pkg.induction_on x (isClosed_eq pkg.continuous_extend hf.continuous) fun y =>
      pkg.extend_coe (hf.comp <| pkg.uniformContinuous_coe) y

Extension of Composition with Inclusion Map Equals Original Function

Informal description

Let $\hat{\alpha}$ be an abstract completion of a uniform space $\alpha$ with inclusion map $\iota : \alpha \to \hat{\alpha}$. For any uniformly continuous function $f : \hat{\alpha} \to \beta$, the extension of the composition $f \circ \iota$ equals $f$, i.e., $\text{extend}(f \circ \iota) = f$.

AbstractCompletion.map definition

(f : α → β) : hatα → hatβ

Full source

/-- Lifting maps to completions -/
protected def map (f : α → β) : hatα → hatβ :=
  pkg.extend (ι'ι' ∘ f)

Lifting of maps between uniform spaces to their completions

Informal description

Given uniform spaces $\alpha$ and $\beta$ with their respective abstract completions $\hat{\alpha}$ and $\hat{\beta}$, and given a map $f: \alpha \to \beta$, the function `AbstractCompletion.map` lifts $f$ to a map between completions $\hat{\alpha} \to \hat{\beta}$. This is constructed by extending the composition of $f$ with the inclusion map $\iota': \beta \to \hat{\beta}$.

AbstractCompletion.uniformContinuous_map theorem

: UniformContinuous (map f)

Full source

theorem uniformContinuous_map : UniformContinuous (map f) :=
  pkg.uniformContinuous_extend

Uniform Continuity of the Completion Lift

Informal description

For any uniformly continuous map $f \colon \alpha \to \beta$ between uniform spaces, the lifted map $\hat{f} \colon \hat{\alpha} \to \hat{\beta}$ between their Hausdorff completions is also uniformly continuous.

AbstractCompletion.continuous_map theorem

: Continuous (map f)

Full source

@[continuity]
theorem continuous_map : Continuous (map f) :=
  pkg.continuous_extend

Continuity of the Completion Lift

Informal description

For any uniformly continuous map $f \colon \alpha \to \beta$ between uniform spaces, the lifted map $\hat{f} \colon \hat{\alpha} \to \hat{\beta}$ between their Hausdorff completions is continuous.

AbstractCompletion.map_coe theorem

(hf : UniformContinuous f) (a : α) : map f (ι a) = ι' (f a)

Full source

@[simp]
theorem map_coe (hf : UniformContinuous f) (a : α) : map f (ι a) = ι' (f a) :=
  pkg.extend_coe (pkg'.uniformContinuous_coe.comp hf) a

Commutativity of Completion Lift with Inclusion Maps

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with abstract completions $\hat{\alpha}$ and $\hat{\beta}$ respectively, equipped with inclusion maps $\iota \colon \alpha \to \hat{\alpha}$ and $\iota' \colon \beta \to \hat{\beta}$. For any uniformly continuous map $f \colon \alpha \to \beta$ and any $a \in \alpha$, the lifted map $\text{map}(f) \colon \hat{\alpha} \to \hat{\beta}$ satisfies $\text{map}(f)(\iota(a)) = \iota'(f(a))$.

AbstractCompletion.map_unique theorem

{f : α → β} {g : hatα → hatβ} (hg : UniformContinuous g) (h : ∀ a, ι' (f a) = g (ι a)) : map f = g

Full source

theorem map_unique {f : α → β} {g : hatα → hatβ} (hg : UniformContinuous g)
    (h : ∀ a, ι' (f a) = g (ι a)) : map f = g :=
  pkg.funext (pkg.continuous_map _ _) hg.continuous <| by
    intro a
    change pkg.extend (ι'ι' ∘ f) _ = _
    simp_rw [Function.comp_def, h, ← comp_apply (f := g)]
    rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]

Uniqueness of Uniformly Continuous Extension from Completion

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with Hausdorff completions $\hat{\alpha}$ and $\hat{\beta}$ respectively, and let $\iota \colon \alpha \to \hat{\alpha}$ and $\iota' \colon \beta \to \hat{\beta}$ be the inclusion maps. Given a map $f \colon \alpha \to \beta$ and a uniformly continuous map $g \colon \hat{\alpha} \to \hat{\beta}$ such that for every $a \in \alpha$, $\iota'(f(a)) = g(\iota(a))$, then the lifted map $\text{map}(f) \colon \hat{\alpha} \to \hat{\beta}$ equals $g$.

AbstractCompletion.map_id theorem

: pkg.map pkg id = id

Full source

@[simp]
theorem map_id : pkg.map pkg id = id :=
  pkg.map_unique pkg uniformContinuous_id fun _ => rfl

Identity Map Lifts to Identity on Completion

Informal description

For any abstract completion $\hat{\alpha}$ of a uniform space $\alpha$ with inclusion map $\iota \colon \alpha \to \hat{\alpha}$, the lifted identity map $\text{map}(\text{id})$ on $\hat{\alpha}$ is equal to the identity function $\text{id}$ on $\hat{\alpha}$.

AbstractCompletion.extend_map theorem

 [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β} (hf : UniformContinuous f) (hg : UniformContinuous g) :
  pkg'.extend f ∘ map g = pkg.extend (f ∘ g)

Full source

theorem extend_map [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β}
    (hf : UniformContinuous f) (hg : UniformContinuous g) :
    pkg'.extend f ∘ map g = pkg.extend (f ∘ g) :=
  pkg.funext (pkg'.continuous_extend.comp (pkg.continuous_map pkg' _)) pkg.continuous_extend
    fun a => by
    rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]
    rfl

Commutativity of Extension and Lifting for Uniformly Continuous Maps on Completions

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces, where $\gamma$ is complete and T₀. Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be uniformly continuous maps. Then, the composition of the extension of $f$ to the completion of $\beta$ with the lifting of $g$ to completions equals the extension of the composition $f \circ g$ to the completion of $\alpha$. In other words, the following diagram commutes: \[ \begin{CD} \hat{\alpha} @>{\text{map}(g)}>> \hat{\beta} \\ @V{\text{extend}(f \circ g)}VV @VV{\text{extend}(f)}V \\ \gamma @= \gamma \end{CD} \]

AbstractCompletion.map_comp theorem

 {g : β → γ} {f : α → β} (hg : UniformContinuous g) (hf : UniformContinuous f) :
  pkg'.map pkg'' g ∘ pkg.map pkg' f = pkg.map pkg'' (g ∘ f)

Full source

theorem map_comp {g : β → γ} {f : α → β} (hg : UniformContinuous g) (hf : UniformContinuous f) :
    pkg'.map pkg'' g ∘ pkg.map pkg' f = pkg.map pkg'' (g ∘ f) :=
  pkg.extend_map pkg' (pkg''.uniformContinuous_coe.comp hg) hf

Composition of Lifted Uniformly Continuous Maps on Completions

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces with abstract completions $\hat{\alpha}$, $\hat{\beta}$, and $\hat{\gamma}$ respectively. Given uniformly continuous maps $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the composition of the lifted maps $\hat{g} \circ \hat{f}$ on the completions equals the lift of the composition $g \circ f$, i.e., $\hat{g} \circ \hat{f} = \widehat{g \circ f}$.

AbstractCompletion.compare definition

: pkg.space → pkg'.space

Full source

/-- The comparison map between two completions of the same uniform space. -/
def compare : pkg.space → pkg'.space :=
  pkg.extend pkg'.coe

Comparison map between completions

Informal description

Given two abstract completions $ \hat{\alpha} $ and $ \hat{\alpha}' $ of the same uniform space $ \alpha $, the comparison map $ \hat{\alpha} \to \hat{\alpha}' $ is the unique uniformly continuous extension of the canonical embedding $ \alpha \to \hat{\alpha}' $.

AbstractCompletion.uniformContinuous_compare theorem

: UniformContinuous (pkg.compare pkg')

Full source

theorem uniformContinuous_compare : UniformContinuous (pkg.compare pkg') :=
  pkg.uniformContinuous_extend

Uniform Continuity of the Comparison Map Between Completions

Informal description

For any two abstract completions $\hat{\alpha}$ and $\hat{\alpha}'$ of a uniform space $\alpha$, the comparison map $\hat{\alpha} \to \hat{\alpha}'$ is uniformly continuous.

AbstractCompletion.compare_coe theorem

(a : α) : pkg.compare pkg' (pkg.coe a) = pkg'.coe a

Full source

theorem compare_coe (a : α) : pkg.compare pkg' (pkg.coe a) = pkg'.coe a :=
  pkg.extend_coe pkg'.uniformContinuous_coe a

Commutativity of Comparison Map on Original Space Elements

Informal description

For any element $a$ in a uniform space $\alpha$ and any two abstract completions $\hat{\alpha}$ and $\hat{\alpha}'$ of $\alpha$, the comparison map $\hat{\alpha} \to \hat{\alpha}'$ applied to the image of $a$ in $\hat{\alpha}$ equals the image of $a$ in $\hat{\alpha}'$. In other words, the diagram commutes on the elements of $\alpha$.

AbstractCompletion.inverse_compare theorem

: pkg.compare pkg' ∘ pkg'.compare pkg = id

Full source

theorem inverse_compare : pkg.compare pkg' ∘ pkg'.compare pkg = id := by
  have uc := pkg.uniformContinuous_compare pkg'
  have uc' := pkg'.uniformContinuous_compare pkg
  apply pkg'.funext (uc.comp uc').continuous continuous_id
  intro a
  rw [comp_apply, pkg'.compare_coe pkg, pkg.compare_coe pkg']
  rfl

Inverse Property of Completion Comparison Maps: $f \circ g = \text{id}$

Informal description

For any two abstract completions $\hat{\alpha}$ and $\hat{\alpha}'$ of a uniform space $\alpha$, the composition of the comparison maps $\hat{\alpha} \to \hat{\alpha}'$ and $\hat{\alpha}' \to \hat{\alpha}$ is the identity map on $\hat{\alpha}$.

AbstractCompletion.compareEquiv definition

: pkg.space ≃ᵤ pkg'.space

Full source

/-- The uniform bijection between two completions of the same uniform space. -/
def compareEquiv : pkg.space ≃ᵤ pkg'.space where
  toFun := pkg.compare pkg'
  invFun := pkg'.compare pkg
  left_inv := congr_fun (pkg'.inverse_compare pkg)
  right_inv := congr_fun (pkg.inverse_compare pkg')
  uniformContinuous_toFun := uniformContinuous_compare _ _
  uniformContinuous_invFun := uniformContinuous_compare _ _

Uniform equivalence between completions of a uniform space

Informal description

Given two abstract completions $ \hat{\alpha} $ and $ \hat{\alpha}' $ of the same uniform space $ \alpha $, the uniform equivalence $ \hat{\alpha} \simeq \hat{\alpha}' $ is defined by the comparison maps between the completions, which are uniformly continuous and inverse to each other.

AbstractCompletion.uniformContinuous_compareEquiv theorem

: UniformContinuous (pkg.compareEquiv pkg')

Full source

theorem uniformContinuous_compareEquiv : UniformContinuous (pkg.compareEquiv pkg') :=
  pkg.uniformContinuous_compare pkg'

Uniform Continuity of the Completion Comparison Equivalence

Informal description

For any two abstract completions $\hat{\alpha}$ and $\hat{\alpha}'$ of a uniform space $\alpha$, the uniform equivalence map $\hat{\alpha} \simeq \hat{\alpha}'$ is uniformly continuous.

AbstractCompletion.uniformContinuous_compareEquiv_symm theorem

: UniformContinuous (pkg.compareEquiv pkg').symm

Full source

theorem uniformContinuous_compareEquiv_symm : UniformContinuous (pkg.compareEquiv pkg').symm :=
  pkg'.uniformContinuous_compare pkg

Uniform Continuity of the Inverse Comparison Map Between Completions

Informal description

For any two abstract completions $\hat{\alpha}$ and $\hat{\alpha}'$ of a uniform space $\alpha$, the inverse of the uniform equivalence $\hat{\alpha} \simeq \hat{\alpha}'$ is uniformly continuous.

AbstractCompletion.compare_comp_eq_compare theorem

 (γ : Type*) [TopologicalSpace γ] [T3Space γ] {f : α → γ} (cont_f : Continuous f) :
  letI := pkg.uniformStruct.toTopologicalSpace
  letI := pkg'.uniformStruct.toTopologicalSpace
  (∀ a : pkg.space, Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.isDenseInducing.extend f) a))) →
    pkg.isDenseInducing.extend f ∘ pkg'.compare pkg = pkg'.isDenseInducing.extend f

Full source

theorem compare_comp_eq_compare (γ : Type*) [TopologicalSpace γ]
    [T3Space γ] {f : α → γ} (cont_f : Continuous f) :
    letI := pkg.uniformStruct.toTopologicalSpace
    letI := pkg'.uniformStruct.toTopologicalSpace
    (∀ a : pkg.space,
      Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.isDenseInducing.extend f) a))) →
      pkg.isDenseInducing.extend f ∘ pkg'.compare pkg = pkg'.isDenseInducing.extend f := by
  let _ := pkg'.uniformStruct
  let _ := pkg.uniformStruct
  intro h
  have (x : α) : (pkg.isDenseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by
    simp only [Function.comp_apply, compare_coe, IsDenseInducing.extend_eq _ cont_f, implies_true]
  apply (IsDenseInducing.extend_unique (AbstractCompletion.isDenseInducing _) this
    (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous )).symm
  apply IsDenseInducing.continuous_extend
  exact fun a ↦ ⟨(pkg.isDenseInducing.extend f) a, h a⟩

Compatibility of Extensions with Completion Comparison Maps

Informal description

Let $\alpha$ be a uniform space with two abstract completions $\hat{\alpha}$ and $\hat{\alpha}'$, and let $\gamma$ be a T₃ topological space. Given a continuous function $f \colon \alpha \to \gamma$ such that for every $a \in \hat{\alpha}$, the function $f$ tends to its extension at $a$ along the filter induced by the completion map, then the composition of the extension of $f$ to $\hat{\alpha}$ with the comparison map $\hat{\alpha}' \to \hat{\alpha}$ equals the extension of $f$ to $\hat{\alpha}'$. In other words, the following diagram commutes: \[ \begin{CD} \hat{\alpha}' @>{\text{compare}}>> \hat{\alpha} \\ @V{\text{extend } f}VV @VV{\text{extend } f}V \\ \gamma @= \gamma \end{CD} \]

AbstractCompletion.prod definition

: AbstractCompletion (α × β)

Full source

/-- Products of completions -/
protected def prod : AbstractCompletion (α × β) where
  space := hatαhatα × hatβ
  coe p := ⟨ι p.1, ι' p.2⟩
  uniformStruct := inferInstance
  complete := inferInstance
  separation := inferInstance
  isUniformInducing := IsUniformInducing.prod pkg.isUniformInducing pkg'.isUniformInducing
  dense := pkg.dense.prodMap pkg'.dense

Product of abstract completions

Informal description

The product of two abstract completions $\hat{\alpha}$ and $\hat{\beta}$ of uniform spaces $\alpha$ and $\beta$ respectively is an abstract completion of the product space $\alpha \times \beta$. The completion map is given by the product of the completion maps $\iota : \alpha \to \hat{\alpha}$ and $\iota' : \beta \to \hat{\beta}$.

AbstractCompletion.extend₂ definition

(f : α → β → γ) : hatα → hatβ → γ

Full source

/-- Extend two variable map to completions. -/
protected def extend₂ (f : α → β → γ) : hatα → hatβ → γ :=
  curry <| (pkg.prod pkg').extend (uncurry f)

Extension of two-variable maps to completions

Informal description

Given a uniformly continuous function $ f : \alpha \to \beta \to \gamma $, the function `AbstractCompletion.extend₂` extends $ f $ to a function $ \hat{\alpha} \to \hat{\beta} \to \gamma $ on the completions of $ \alpha $ and $ \beta $. This is done by first uncurrying $ f $ to a function $ \alpha \times \beta \to \gamma $, extending it to the completion $ \widehat{\alpha \times \beta} $, and then currying the result back to a function $ \hat{\alpha} \to \hat{\beta} \to \gamma $.

AbstractCompletion.extension₂_coe_coe theorem

(hf : UniformContinuous <| uncurry f) (a : α) (b : β) : pkg.extend₂ pkg' f (ι a) (ι' b) = f a b

Full source

theorem extension₂_coe_coe (hf : UniformContinuous <| uncurry f) (a : α) (b : β) :
    pkg.extend₂ pkg' f (ι a) (ι' b) = f a b :=
  show (pkg.prod pkg').extend (uncurry f) ((pkg.prod pkg').coe (a, b)) = uncurry f (a, b) from
    (pkg.prod pkg').extend_coe hf _

Extension of Bivariate Function Preserves Values on Original Space

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with abstract completions $\hat{\alpha}$ and $\hat{\beta}$ respectively, and let $\iota : \alpha \to \hat{\alpha}$ and $\iota' : \beta \to \hat{\beta}$ be the inclusion maps. Given a function $f : \alpha \to \beta \to \gamma$ such that the uncurried function $(a, b) \mapsto f(a, b)$ is uniformly continuous, then for any $a \in \alpha$ and $b \in \beta$, the extended function satisfies: \[ \text{extend}_2(f)(\iota(a), \iota'(b)) = f(a, b). \]

AbstractCompletion.uniformContinuous_extension₂ theorem

: UniformContinuous₂ (pkg.extend₂ pkg' f)

Full source

theorem uniformContinuous_extension₂ : UniformContinuous₂ (pkg.extend₂ pkg' f) := by
  rw [uniformContinuous₂_def, AbstractCompletion.extend₂, uncurry_curry]
  apply uniformContinuous_extend

Uniform Continuity of the Extended Two-Variable Function on Completions

Informal description

Given two uniform spaces $\alpha$ and $\beta$ with abstract completions $\hat{\alpha}$ and $\hat{\beta}$ respectively, and a uniformly continuous function $f : \alpha \to \beta \to \gamma$, the extended function $\text{extend}_2(f) : \hat{\alpha} \to \hat{\beta} \to \gamma$ is uniformly continuous in both arguments.

AbstractCompletion.map₂ definition

(f : α → β → γ) : hatα → hatβ → hatγ

Full source

/-- Lift two variable maps to completions. -/
protected def map₂ (f : α → β → γ) : hatα → hatβ → hatγ :=
  pkg.extend₂ pkg' (pkg''.coe ∘₂ f)

Extension of two-variable maps to completions with completion of codomain

Informal description

Given a function $ f : \alpha \to \beta \to \gamma $, the function `AbstractCompletion.map₂` extends $ f $ to a function $ \hat{\alpha} \to \hat{\beta} \to \hat{\gamma} $ on the completions of $ \alpha $, $ \beta $, and $ \gamma $. This is done by first composing $ f $ with the completion map of $ \gamma $ and then extending the resulting function to the completions of $ \alpha $ and $ \beta $.

AbstractCompletion.uniformContinuous_map₂ theorem

(f : α → β → γ) : UniformContinuous₂ (pkg.map₂ pkg' pkg'' f)

Full source

theorem uniformContinuous_map₂ (f : α → β → γ) : UniformContinuous₂ (pkg.map₂ pkg' pkg'' f) :=
  AbstractCompletion.uniformContinuous_extension₂ pkg pkg' _

Uniform Continuity of the Extension of a Two-Variable Function to Completions

Informal description

For any uniformly continuous function $f \colon \alpha \to \beta \to \gamma$, the extended function $\hat{f} \colon \hat{\alpha} \to \hat{\beta} \to \hat{\gamma}$ on the completions is uniformly continuous in both arguments.

AbstractCompletion.continuous_map₂ theorem

 {δ} [TopologicalSpace δ] {f : α → β → γ} {a : δ → hatα} {b : δ → hatβ} (ha : Continuous a) (hb : Continuous b) :
  Continuous fun d : δ => pkg.map₂ pkg' pkg'' f (a d) (b d)

Full source

theorem continuous_map₂ {δ} [TopologicalSpace δ] {f : α → β → γ} {a : δ → hatα} {b : δ → hatβ}
    (ha : Continuous a) (hb : Continuous b) :
    Continuous fun d : δ => pkg.map₂ pkg' pkg'' f (a d) (b d) :=
  (pkg.uniformContinuous_map₂ pkg' pkg'' f).continuous.comp₂ ha hb

Continuity of the Extension of a Two-Variable Function to Completions with Respect to Continuous Inputs

Informal description

Let $\delta$ be a topological space, and let $f \colon \alpha \to \beta \to \gamma$ be a function. Suppose $a \colon \delta \to \hat{\alpha}$ and $b \colon \delta \to \hat{\beta}$ are continuous maps from $\delta$ to the completions of $\alpha$ and $\beta$ respectively. Then the function $d \mapsto \hat{f}(a(d), b(d))$ is continuous, where $\hat{f} \colon \hat{\alpha} \to \hat{\beta} \to \hat{\gamma}$ is the extension of $f$ to the completions.

AbstractCompletion.map₂_coe_coe theorem

 (a : α) (b : β) (f : α → β → γ) (hf : UniformContinuous₂ f) : pkg.map₂ pkg' pkg'' f (ι a) (ι' b) = ι'' (f a b)

Full source

theorem map₂_coe_coe (a : α) (b : β) (f : α → β → γ) (hf : UniformContinuous₂ f) :
    pkg.map₂ pkg' pkg'' f (ι a) (ι' b) = ι'' (f a b) :=
  pkg.extension₂_coe_coe (f := pkg''.coe ∘₂ f) pkg' (pkg''.uniformContinuous_coe.comp hf) a b

Extension of Uniformly Continuous Bivariate Function Preserves Values on Original Space

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces with abstract completions $\hat{\alpha}$, $\hat{\beta}$, and $\hat{\gamma}$ respectively, and let $\iota \colon \alpha \to \hat{\alpha}$, $\iota' \colon \beta \to \hat{\beta}$, and $\iota'' \colon \gamma \to \hat{\gamma}$ be the inclusion maps. Given a uniformly continuous function $f \colon \alpha \to \beta \to \gamma$, then for any $a \in \alpha$ and $b \in \beta$, the extended function satisfies: \[ \text{map}_2(f)(\iota(a), \iota'(b)) = \iota''(f(a, b)). \]