Mathlib.Topology.UniformSpace.Completion

CauchyFilter definition

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

Full source

/-- 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.
-/
def CauchyFilter (α : Type u) [UniformSpace α] : Type u :=
  { f : Filter α // Cauchy f }

Space of Cauchy Filters

Informal description

The space of Cauchy filters on a uniform space $\alpha$ consists of all filters $f$ on $\alpha$ that satisfy the Cauchy condition. This construction serves as a completion of the uniform space, where the embeddings are given by neighborhood filters. Note that this space is not minimal - to obtain the minimal completion, one needs to take the separated quotient (by identifying points whose neighborhoods are indistinguishable under the uniformity).

CauchyFilter.instNeBotValFilterCauchy instance

(f : CauchyFilter α) : NeBot f.1

Full source

instance (f : CauchyFilter α) : NeBot f.1 := f.2.1

Non-triviality of Cauchy Filters

Informal description

For any Cauchy filter $f$ on a uniform space $\alpha$, the underlying filter $f.1$ is non-trivial (i.e., it does not contain the empty set).

CauchyFilter.gen definition

(s : Set (α × α)) : Set (CauchyFilter α × CauchyFilter α)

Full source

/-- The pairs of Cauchy filters generated by a set. -/
def gen (s : Set (α × α)) : Set (CauchyFilterCauchyFilter α × CauchyFilter α) :=
  { p | s ∈ p.1.val ×ˢ p.2.val }

Set of Cauchy filter pairs containing a given set

Informal description

For a uniform space $\alpha$ and a set $s \subseteq \alpha \times \alpha$, the function `CauchyFilter.gen` maps $s$ to the set of pairs $(F, G)$ of Cauchy filters on $\alpha$ such that $s$ belongs to the product filter $F \times G$.

CauchyFilter.monotone_gen theorem

: Monotone (gen : Set (α × α) → _)

Full source

theorem monotone_gen : Monotone (gen : Set (α × α) → _) :=
  monotone_setOf fun p => @Filter.monotone_mem _ (p.1.val ×ˢ p.2.val)

Monotonicity of the Cauchy Filter Generator Function

Informal description

The function `gen : \mathcal{P}(\alpha \times \alpha) \to \mathcal{P}(\text{CauchyFilter } \alpha \times \text{CauchyFilter } \alpha)` is monotone with respect to the subset order. That is, for any sets $s_1, s_2 \subseteq \alpha \times \alpha$, if $s_1 \subseteq s_2$, then $\text{gen}(s_1) \subseteq \text{gen}(s_2)$.

CauchyFilter.instUniformSpace instance

: UniformSpace (CauchyFilter α)

Full source

instance : UniformSpace (CauchyFilter α) :=
  UniformSpace.ofCore
    { uniformity := (𝓤 α).lift' gen
      refl := principal_le_lift'.2 fun _s hs ⟨a, b⟩ =>
        fun (a_eq_b : a = b) => a_eq_b ▸ a.property.right hs
      symm := symm_gen
      comp := comp_gen }

Uniform Space Structure on Cauchy Filters

Informal description

The space of Cauchy filters on a uniform space $\alpha$ can be equipped with a natural uniform space structure, where the uniformity is generated by the entourages of $\alpha$.

CauchyFilter.mem_uniformity theorem

{s : Set (CauchyFilter α × CauchyFilter α)} : s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, gen t ⊆ s

Full source

theorem mem_uniformity {s : Set (CauchyFilterCauchyFilter α × CauchyFilter α)} :
    s ∈ 𝓤 (CauchyFilter α)s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, gen t ⊆ s :=
  mem_lift'_sets monotone_gen

Characterization of Uniformity in Cauchy Filter Space: $s \in \mathfrak{U}(\text{CauchyFilter}(\alpha)) \leftrightarrow \exists t \in \mathfrak{U}(\alpha), \text{gen}(t) \subseteq s$

Informal description

For any set $s \subseteq \text{CauchyFilter}(\alpha) \times \text{CauchyFilter}(\alpha)$, $s$ belongs to the uniformity of $\text{CauchyFilter}(\alpha)$ if and only if there exists an entourage $t$ in the uniformity of $\alpha$ such that $\text{gen}(t) \subseteq s$, where $\text{gen}(t)$ is the set of pairs of Cauchy filters $(F, G)$ for which $t$ belongs to the product filter $F \times G$.

CauchyFilter.basis_uniformity theorem

 {ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) : (𝓤 (CauchyFilter α)).HasBasis p (gen ∘ s)

Full source

theorem basis_uniformity {ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) :
    (𝓤 (CauchyFilter α)).HasBasis p (gengen ∘ s) :=
  h.lift' monotone_gen

Uniformity Basis Correspondence for Cauchy Filter Completion

Informal description

Let $\alpha$ be a uniform space with a basis $\{s_i\}_{i \in \iota}$ for its uniformity $\mathfrak{U}(\alpha)$, indexed by a type $\iota$ with a predicate $p$. Then the uniformity $\mathfrak{U}(\text{CauchyFilter } \alpha)$ on the space of Cauchy filters has a basis consisting of the sets $\text{gen}(s_i)$ for $i \in \iota$ satisfying $p(i)$, where $\text{gen}(s)$ is the set of pairs $(F, G)$ of Cauchy filters such that $s \in F \times G$.

CauchyFilter.mem_uniformity' theorem

 {s : Set (CauchyFilter α × CauchyFilter α)} :
  s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, ∀ f g : CauchyFilter α, t ∈ f.1 ×ˢ g.1 → (f, g) ∈ s

Full source

theorem mem_uniformity' {s : Set (CauchyFilterCauchyFilter α × CauchyFilter α)} :
    s ∈ 𝓤 (CauchyFilter α)s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t ∈ 𝓤 α, ∀ f g : CauchyFilter α, t ∈ f.1 ×ˢ g.1 → (f, g) ∈ s := by
  refine mem_uniformity.trans (exists_congr (fun t => and_congr_right_iff.mpr (fun _h => ?_)))
  exact ⟨fun h _f _g ht => h ht, fun h _p hp => h _ _ hp⟩

Characterization of Uniformity in Cauchy Filter Space via Entourages

Informal description

For any set $s$ of pairs of Cauchy filters on a uniform space $\alpha$, $s$ belongs to the uniformity of the Cauchy filter space $\text{CauchyFilter}(\alpha)$ if and only if there exists an entourage $t$ in the uniformity of $\alpha$ such that for any two Cauchy filters $f$ and $g$ on $\alpha$, if $t$ belongs to the product filter $f \times g$, then the pair $(f, g)$ belongs to $s$.

CauchyFilter.pureCauchy definition

(a : α) : CauchyFilter α

Full source

/-- Embedding of `α` into its completion `CauchyFilter α` -/
def pureCauchy (a : α) : CauchyFilter α :=
  ⟨pure a, cauchy_pure⟩

Canonical embedding into Cauchy filter completion

Informal description

The function maps an element $a$ of a uniform space $\alpha$ to the Cauchy filter generated by the principal filter of $a$ (i.e., the collection of all subsets of $\alpha$ containing $a$). This serves as the canonical embedding of $\alpha$ into its completion `CauchyFilter α`.

CauchyFilter.isUniformInducing_pureCauchy theorem

: IsUniformInducing (pureCauchy : α → CauchyFilter α)

Full source

theorem isUniformInducing_pureCauchy : IsUniformInducing (pureCauchy : α → CauchyFilter α) :=
  ⟨have : (preimage fun x : α × α => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen = id :=
      funext fun s =>
        Set.ext fun ⟨a₁, a₂⟩ => by simp [preimage, gen, pureCauchy, prod_principal_principal]
    calc
      comap (fun x : α × α => (pureCauchy x.fst, pureCauchy x.snd)) ((𝓤 α).lift' gen) =
          (𝓤 α).lift' ((preimage fun x : α × α => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen) :=
        comap_lift'_eq
      _ = 𝓤 α := by simp [this]
      ⟩

Uniform Inducing Property of the Canonical Embedding into Cauchy Filter Completion

Informal description

The canonical embedding $\text{pureCauchy} : \alpha \to \text{CauchyFilter}(\alpha)$, which maps each element $a \in \alpha$ to the principal Cauchy filter generated by $a$, is a uniform inducing map. This means the uniformity filter on $\alpha$ is exactly the pullback of the uniformity filter on $\text{CauchyFilter}(\alpha)$ under the product map $\text{Prod.map pureCauchy pureCauchy}$.

CauchyFilter.isUniformEmbedding_pureCauchy theorem

: IsUniformEmbedding (pureCauchy : α → CauchyFilter α)

Full source

theorem isUniformEmbedding_pureCauchy : IsUniformEmbedding (pureCauchy : α → CauchyFilter α) where
  __ := isUniformInducing_pureCauchy
  injective _a₁ _a₂ h := pure_injective <| Subtype.ext_iff_val.1 h

Uniform Embedding Property of the Canonical Map to Cauchy Filter Completion

Informal description

The canonical embedding $\text{pureCauchy} : \alpha \to \text{CauchyFilter}(\alpha)$, which maps each element $a \in \alpha$ to the principal Cauchy filter generated by $a$, is a uniform embedding. This means it is injective, uniformly continuous, and the uniformity on $\alpha$ is induced by the uniformity on $\text{CauchyFilter}(\alpha)$ via $\text{pureCauchy}$.

CauchyFilter.denseRange_pureCauchy theorem

: DenseRange (pureCauchy : α → CauchyFilter α)

Full source

theorem denseRange_pureCauchy : DenseRange (pureCauchy : α → CauchyFilter α) := fun f => by
  have h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y : α, (f, pureCauchy y) ∈ s := fun s hs =>
    let ⟨t'', ht''₁, (ht''₂ : gen t'' ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs
    let ⟨t', ht'₁, ht'₂⟩ := comp_mem_uniformity_sets ht''₁
    have : t' ∈ f.val ×ˢ f.val := f.property.right ht'₁
    let ⟨t, ht, (h : t ×ˢ t ⊆ t')⟩ := mem_prod_same_iff.mp this
    let ⟨x, (hx : x ∈ t)⟩ := f.property.left.nonempty_of_mem ht
    have : t'' ∈ f.val ×ˢ pure x :=
      mem_prod_iff.mpr
        ⟨t, ht, { y : α | (x, y) ∈ t' }, h <| mk_mem_prod hx hx,
          fun ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩ =>
          ht'₂ <| prodMk_mem_compRel (@h (a, x) ⟨h₁, hx⟩) h₂⟩
    ⟨x, ht''₂ <| by dsimp [gen]; exact this⟩
  simp only [closure_eq_cluster_pts, ClusterPt, nhds_eq_uniformity, lift'_inf_principal_eq,
    Set.inter_comm _ (range pureCauchy), mem_setOf_eq]
  refine (lift'_neBot_iff ?_).mpr (fun s hs => ?_)
  · exact monotone_const.inter monotone_preimage
  · let ⟨y, hy⟩ := h_ex s hs
    have : pureCauchypureCauchy y ∈ range pureCauchy ∩ { y : CauchyFilter α | (f, y) ∈ s } :=
      ⟨mem_range_self y, hy⟩
    exact ⟨_, this⟩

Density of the Canonical Embedding in the Cauchy Filter Completion

Informal description

The image of the canonical embedding $\text{pureCauchy} : \alpha \to \text{CauchyFilter}(\alpha)$, which maps each element $a \in \alpha$ to the principal Cauchy filter generated by $a$, is dense in the space of Cauchy filters on $\alpha$.

CauchyFilter.isDenseInducing_pureCauchy theorem

: IsDenseInducing (pureCauchy : α → CauchyFilter α)

Full source

theorem isDenseInducing_pureCauchy : IsDenseInducing (pureCauchy : α → CauchyFilter α) :=
  isUniformInducing_pureCauchy.isDenseInducing denseRange_pureCauchy

Dense Inducing Property of the Canonical Embedding into Cauchy Filter Completion

Informal description

The canonical embedding $\text{pureCauchy} : \alpha \to \text{CauchyFilter}(\alpha)$, which maps each element $a \in \alpha$ to the principal Cauchy filter generated by $a$, is a dense inducing map. This means that the image of $\alpha$ under $\text{pureCauchy}$ is dense in $\text{CauchyFilter}(\alpha)$, and the topology on $\alpha$ is induced by the topology on $\text{CauchyFilter}(\alpha)$ via $\text{pureCauchy}$.

CauchyFilter.isDenseEmbedding_pureCauchy theorem

: IsDenseEmbedding (pureCauchy : α → CauchyFilter α)

Full source

theorem isDenseEmbedding_pureCauchy : IsDenseEmbedding (pureCauchy : α → CauchyFilter α) :=
  isUniformEmbedding_pureCauchy.isDenseEmbedding denseRange_pureCauchy

Dense Embedding Property of the Canonical Map to Cauchy Filter Completion

Informal description

The canonical embedding $\text{pureCauchy} : \alpha \to \text{CauchyFilter}(\alpha)$, which maps each element $a \in \alpha$ to the principal Cauchy filter generated by $a$, is a dense embedding. This means it is a topological embedding (i.e., a homeomorphism onto its image) and its image is dense in $\text{CauchyFilter}(\alpha)$.

CauchyFilter.nonempty_cauchyFilter_iff theorem

: Nonempty (CauchyFilter α) ↔ Nonempty α

Full source

theorem nonempty_cauchyFilter_iff : NonemptyNonempty (CauchyFilter α) ↔ Nonempty α := by
  constructor <;> rintro ⟨c⟩
  · have := eq_univ_iff_forall.1 isDenseEmbedding_pureCauchy.isDenseInducing.closure_range c
    obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial
    exact ⟨a⟩
  · exact ⟨pureCauchy c⟩

Nonempty Cauchy Filter Space iff Nonempty Base Space

Informal description

The space of Cauchy filters on a uniform space $\alpha$ is nonempty if and only if $\alpha$ itself is nonempty.

CauchyFilter.instCompleteSpace instance

: CompleteSpace (CauchyFilter α)

Full source

instance : CompleteSpace (CauchyFilter α) :=
  completeSpace_extension isUniformInducing_pureCauchy denseRange_pureCauchy fun f hf =>
    let f' : CauchyFilter α := ⟨f, hf⟩
    have : map pureCauchy f ≤ (𝓤 <| CauchyFilter α).lift' (preimage (Prod.mk f')) :=
      le_lift'.2 fun _ hs =>
        let ⟨t, ht₁, ht₂⟩ := (mem_lift'_sets monotone_gen).mp hs
        let ⟨t', ht', (h : t' ×ˢ t' ⊆ t)⟩ := mem_prod_same_iff.mp (hf.right ht₁)
        have : t' ⊆ { y : α | (f', pureCauchy y) ∈ gen t } := fun x hx =>
          (f ×ˢ pure x).sets_of_superset (prod_mem_prod ht' hx) h
        f.sets_of_superset ht' <| Subset.trans this (preimage_mono ht₂)
    ⟨f', by simpa [nhds_eq_uniformity]⟩

Completeness of the Cauchy Filter Space

Informal description

The space of Cauchy filters on a uniform space $\alpha$ is complete.

CauchyFilter.instInhabited instance

[Inhabited α] : Inhabited (CauchyFilter α)

Full source

instance [Inhabited α] : Inhabited (CauchyFilter α) :=
  ⟨pureCauchy default⟩

Inhabited Cauchy Filter Space for Inhabited Uniform Spaces

Informal description

For any inhabited uniform space $\alpha$, the space of Cauchy filters on $\alpha$ is also inhabited.

CauchyFilter.instNonempty instance

[h : Nonempty α] : Nonempty (CauchyFilter α)

Full source

instance [h : Nonempty α] : Nonempty (CauchyFilter α) :=
  h.recOn fun a => Nonempty.intro <| CauchyFilter.pureCauchy a

Nonempty Cauchy Filter Space for Nonempty Uniform Spaces

Informal description

For any nonempty uniform space $\alpha$, the space of Cauchy filters on $\alpha$ is also nonempty.

CauchyFilter.extend definition

(f : α → β) : CauchyFilter α → β

Full source

/-- Extend a uniformly continuous function `α → β` to a function `CauchyFilter α → β`.
Outputs junk when `f` is not uniformly continuous. -/
def extend (f : α → β) : CauchyFilter α → β :=
  if UniformContinuous f then isDenseInducing_pureCauchy.extend f
  else fun x => f (nonempty_cauchyFilter_iff.1 ⟨x⟩).some

Extension of a function to the Cauchy filter completion

Informal description

Given a function $ f \colon \alpha \to \beta $ between uniform spaces, the function $ \text{CauchyFilter.extend} \, f $ extends $ f $ to a function $ \text{CauchyFilter} \, \alpha \to \beta $. If $ f $ is uniformly continuous, this extension is constructed using the dense embedding $ \text{pureCauchy} \colon \alpha \to \text{CauchyFilter} \, \alpha $. Otherwise, the extension outputs an arbitrary value $ f(x) $ for some $ x \in \alpha $ (which exists since $ \text{CauchyFilter} \, \alpha $ is nonempty when $ \alpha $ is nonempty).

CauchyFilter.extend_pureCauchy theorem

{f : α → β} (hf : UniformContinuous f) (a : α) : extend f (pureCauchy a) = f a

Full source

theorem extend_pureCauchy {f : α → β} (hf : UniformContinuous f) (a : α) :
    extend f (pureCauchy a) = f a := by
  rw [extend, if_pos hf]
  exact uniformly_extend_of_ind isUniformInducing_pureCauchy denseRange_pureCauchy hf _

Extension Property of Uniformly Continuous Functions on Cauchy Filter Completion

Informal description

Let $\alpha$ and $\beta$ be uniform spaces, and let $f : \alpha \to \beta$ be a uniformly continuous function. Then for any $a \in \alpha$, the extension of $f$ to the Cauchy filter completion evaluated at the canonical embedding of $a$ equals $f(a)$, i.e., \[ \text{extend}\, f (\text{pureCauchy}\, a) = f(a). \]

CauchyFilter.uniformContinuous_extend theorem

{f : α → β} : UniformContinuous (extend f)

Full source

theorem uniformContinuous_extend {f : α → β} : UniformContinuous (extend f) := by
  by_cases hf : UniformContinuous f
  · rw [extend, if_pos hf]
    exact uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy hf
  · rw [extend, if_neg hf]
    exact uniformContinuous_of_const fun a _b => by congr

Uniform Continuity of the Extension to Cauchy Filter Completion

Informal description

For any function $f \colon \alpha \to \beta$ between uniform spaces, the extension $\text{extend}\, f \colon \text{CauchyFilter}\,\alpha \to \beta$ is uniformly continuous.

CauchyFilter.inseparable_iff theorem

{f g : CauchyFilter α} : Inseparable f g ↔ f.1 ×ˢ g.1 ≤ 𝓤 α

Full source

theorem inseparable_iff {f g : CauchyFilter α} : InseparableInseparable f g ↔ f.1 ×ˢ g.1 ≤ 𝓤 α :=
  (basis_uniformity (basis_sets _)).inseparable_iff_uniformity

Characterization of inseparable Cauchy filters via uniformity

Informal description

For any two Cauchy filters $f$ and $g$ on a uniform space $\alpha$, the following are equivalent: 1. $f$ and $g$ are topologically inseparable (i.e., they have the same neighborhood filter); 2. The product filter $f \times g$ is contained in the uniformity $\mathfrak{U}(\alpha)$ of $\alpha$.

CauchyFilter.inseparable_iff_of_le_nhds theorem

{f g : CauchyFilter α} {a b : α} (ha : f.1 ≤ 𝓝 a) (hb : g.1 ≤ 𝓝 b) : Inseparable a b ↔ Inseparable f g

Full source

theorem inseparable_iff_of_le_nhds {f g : CauchyFilter α} {a b : α}
    (ha : f.1 ≤ 𝓝 a) (hb : g.1 ≤ 𝓝 b) : InseparableInseparable a b ↔ Inseparable f g := by
  rw [← tendsto_id'] at ha hb
  rw [inseparable_iff, (ha.comp tendsto_fst).inseparable_iff_uniformity (hb.comp tendsto_snd)]
  simp only [Function.comp_apply, id_eq, Prod.mk.eta, ← Function.id_def, tendsto_id']

Inseparability of Points vs Cauchy Filters in Uniform Spaces

Informal description

For any two Cauchy filters $f$ and $g$ on a uniform space $\alpha$ and points $a, b \in \alpha$ such that $f$ converges to $a$ and $g$ converges to $b$, the following are equivalent: 1. The points $a$ and $b$ are topologically inseparable in $\alpha$; 2. The Cauchy filters $f$ and $g$ are topologically inseparable in the space of Cauchy filters.

CauchyFilter.inseparable_lim_iff theorem

 [CompleteSpace α] {f g : CauchyFilter α} :
  haveI := f.2.1.nonempty;
  Inseparable (lim f.1) (lim g.1) ↔ Inseparable f g

Full source

theorem inseparable_lim_iff [CompleteSpace α] {f g : CauchyFilter α} :
    haveI := f.2.1.nonempty; InseparableInseparable (lim f.1) (lim g.1) ↔ Inseparable f g :=
  inseparable_iff_of_le_nhds f.2.le_nhds_lim g.2.le_nhds_lim

Equivalence of Limit Inseparability and Cauchy Filter Inseparability in Complete Uniform Spaces

Informal description

Let $\alpha$ be a complete uniform space. For any two Cauchy filters $f$ and $g$ on $\alpha$ (with $f$ nonempty), the limits of $f$ and $g$ are topologically inseparable if and only if the filters $f$ and $g$ themselves are topologically inseparable.

CauchyFilter.cauchyFilter_eq theorem

 {α : Type*} [UniformSpace α] [CompleteSpace α] [T0Space α] {f g : CauchyFilter α} :
  haveI := f.2.1.nonempty;
  lim f.1 = lim g.1 ↔ Inseparable f g

Full source

theorem cauchyFilter_eq {α : Type*} [UniformSpace α] [CompleteSpace α] [T0Space α]
    {f g : CauchyFilter α} :
    haveI := f.2.1.nonempty; limlim f.1 = lim g.1 ↔ Inseparable f g := by
  rw [← inseparable_iff_eq, inseparable_lim_iff]

Equality of Limits vs Inseparability of Cauchy Filters in Complete T₀ Uniform Spaces

Informal description

Let $\alpha$ be a complete uniform space that is also a T₀ space. For any two nonempty Cauchy filters $f$ and $g$ on $\alpha$, the limits of $f$ and $g$ are equal if and only if $f$ and $g$ are topologically inseparable.

CauchyFilter.separated_pureCauchy_injective theorem

{α : Type*} [UniformSpace α] [T0Space α] : Function.Injective fun a : α => SeparationQuotient.mk (pureCauchy a)

Full source

theorem separated_pureCauchy_injective {α : Type*} [UniformSpace α] [T0Space α] :
    Function.Injective fun a : α => SeparationQuotient.mk (pureCauchy a) := fun a b h ↦
  Inseparable.eq <| (inseparable_iff_of_le_nhds (pure_le_nhds a) (pure_le_nhds b)).2 <|
    SeparationQuotient.mk_eq_mk.1 h

Injectivity of the Canonical Embedding into the Hausdorff Completion for T₀ Uniform Spaces

Informal description

Let $\alpha$ be a uniform space that is also a T₀ space. The canonical embedding $a \mapsto \text{SeparationQuotient.mk}(\text{pureCauchy}(a))$ from $\alpha$ into the separated quotient of its Cauchy filter completion is injective.

UniformSpace.Completion definition

Full source

/-- Hausdorff completion of `α` -/
def Completion := SeparationQuotient (CauchyFilter α)

Hausdorff completion of a uniform space

Informal description

The Hausdorff completion of a uniform space $\alpha$ is defined as the quotient of the space of Cauchy filters on $\alpha$ by the separation relation, which identifies Cauchy filters that are inseparable under the uniformity. This construction yields a complete Hausdorff uniform space that serves as the universal completion of $\alpha$.

UniformSpace.Completion.inhabited instance

[Inhabited α] : Inhabited (Completion α)

Full source

instance inhabited [Inhabited α] : Inhabited (Completion α) :=
  inferInstanceAs <| Inhabited (Quotient _)

Inhabitedness of Hausdorff Completion for Inhabited Uniform Spaces

Informal description

For any inhabited uniform space $\alpha$, its Hausdorff completion $\text{Completion}(\alpha)$ is also inhabited.

UniformSpace.Completion.uniformSpace instance

: UniformSpace (Completion α)

Full source

instance uniformSpace : UniformSpace (Completion α) :=
  SeparationQuotient.instUniformSpace

Uniform Space Structure on Hausdorff Completion

Informal description

The Hausdorff completion $\text{Completion}(\alpha)$ of a uniform space $\alpha$ carries a natural uniform space structure, which is induced by the original uniformity on $\alpha$. This structure makes the completion a complete Hausdorff uniform space and ensures that the canonical embedding $\alpha \to \text{Completion}(\alpha)$ is uniformly continuous.

UniformSpace.Completion.completeSpace instance

: CompleteSpace (Completion α)

Full source

instance completeSpace : CompleteSpace (Completion α) :=
  SeparationQuotient.instCompleteSpace

Completeness of the Hausdorff Completion

Informal description

The Hausdorff completion $\text{Completion}(\alpha)$ of a uniform space $\alpha$ is a complete uniform space.

UniformSpace.Completion.t0Space instance

: T0Space (Completion α)

Full source

instance t0Space : T0Space (Completion α) := SeparationQuotient.instT0Space

Hausdorff Completion is T₀

Informal description

The Hausdorff completion $\text{Completion}(\alpha)$ of a uniform space $\alpha$ is a $T_0$ space.

UniformSpace.Completion.coe' definition

: α → Completion α

Full source

/-- The map from a uniform space to its completion. -/
@[coe] def coe' : α → Completion α := SeparationQuotient.mkSeparationQuotient.mk ∘ pureCauchy

Canonical embedding into Hausdorff completion

Informal description

The canonical embedding from a uniform space $\alpha$ to its Hausdorff completion $\text{Completion } \alpha$, defined as the composition of the quotient map $\text{SeparationQuotient.mk}$ with the embedding $\text{pureCauchy}$ that maps each point to its corresponding Cauchy filter.

UniformSpace.Completion.instCoe instance

: Coe α (Completion α)

Full source

/-- Automatic coercion from `α` to its completion. Not always injective. -/
instance : Coe α (Completion α) :=
  ⟨coe'⟩

Canonical Embedding into Hausdorff Completion

Informal description

There is a canonical embedding from a uniform space $\alpha$ to its Hausdorff completion $\text{Completion } \alpha$, which maps each point $x \in \alpha$ to its equivalence class in the completion. This embedding is uniformly continuous and satisfies the universal property of completions.

UniformSpace.Completion.coe_eq theorem

: ((↑) : α → Completion α) = SeparationQuotient.mk ∘ pureCauchy

Full source

protected theorem coe_eq : ((↑) : α → Completion α) = SeparationQuotient.mkSeparationQuotient.mk ∘ pureCauchy := rfl

Canonical Embedding Decomposition for Hausdorff Completion

Informal description

The canonical embedding $(↑) : \alpha \to \text{Completion } \alpha$ from a uniform space $\alpha$ to its Hausdorff completion is equal to the composition of the quotient map $\text{SeparationQuotient.mk}$ with the embedding $\text{pureCauchy}$ that maps each point to its corresponding Cauchy filter.

UniformSpace.Completion.isUniformInducing_coe theorem

: IsUniformInducing ((↑) : α → Completion α)

Full source

theorem isUniformInducing_coe : IsUniformInducing ((↑) : α → Completion α) :=
  SeparationQuotient.isUniformInducing_mk.comp isUniformInducing_pureCauchy

Canonical Embedding into Hausdorff Completion is Uniform Inducing

Informal description

The canonical embedding $(↑) \colon \alpha \to \text{Completion}(\alpha)$ from a uniform space $\alpha$ to its Hausdorff completion is a uniform inducing map. This means the uniformity on $\alpha$ is the pullback of the uniformity on $\text{Completion}(\alpha)$ under the product map $(↑) \times (↑) \colon \alpha \times \alpha \to \text{Completion}(\alpha) \times \text{Completion}(\alpha)$.

UniformSpace.Completion.comap_coe_eq_uniformity theorem

: ((𝓤 _).comap fun p : α × α => ((p.1 : Completion α), (p.2 : Completion α))) = 𝓤 α

Full source

theorem comap_coe_eq_uniformity :
    ((𝓤 _).comap fun p : α × α => ((p.1 : Completion α), (p.2 : Completion α))) = 𝓤 α :=
  (isUniformInducing_coe _).1

Uniformity Preservation under Canonical Embedding into Hausdorff Completion

Informal description

The pullback of the uniformity on the Hausdorff completion $\text{Completion}(\alpha)$ under the canonical embedding $(↑) \times (↑) \colon \alpha \times \alpha \to \text{Completion}(\alpha) \times \text{Completion}(\alpha)$ is equal to the original uniformity $\mathfrak{U}(\alpha)$ on $\alpha$.

UniformSpace.Completion.denseRange_coe theorem

: DenseRange ((↑) : α → Completion α)

Full source

theorem denseRange_coe : DenseRange ((↑) : α → Completion α) :=
  SeparationQuotient.surjective_mk.denseRange.comp denseRange_pureCauchy
    SeparationQuotient.continuous_mk

Density of the Canonical Embedding in the Hausdorff Completion

Informal description

The canonical embedding $(↑) : \alpha \to \text{Completion}(\alpha)$ from a uniform space $\alpha$ to its Hausdorff completion has dense range. That is, the image of $\alpha$ under this embedding is dense in $\text{Completion}(\alpha)$.

UniformSpace.Completion.cPkg definition

{α : Type*} [UniformSpace α] : AbstractCompletion α

Full source

/-- The Haudorff completion as an abstract completion. -/
def cPkg {α : Type*} [UniformSpace α] : AbstractCompletion α where
  space := Completion α
  coe := (↑)
  uniformStruct := by infer_instance
  complete := by infer_instance
  separation := by infer_instance
  isUniformInducing := Completion.isUniformInducing_coe α
  dense := Completion.denseRange_coe

Abstract completion package for uniform spaces

Informal description

The abstract completion package for a uniform space $\alpha$ consists of the Hausdorff completion $\text{Completion}(\alpha)$ equipped with the canonical embedding $(↑) \colon \alpha \to \text{Completion}(\alpha)$. This package satisfies the following properties: 1. The completion $\text{Completion}(\alpha)$ is a complete Hausdorff uniform space. 2. The canonical embedding $(↑)$ has dense range in $\text{Completion}(\alpha)$. 3. The embedding $(↑)$ is uniform inducing, meaning it preserves the uniform structure of $\alpha$.

UniformSpace.Completion.AbstractCompletion.inhabited instance

: Inhabited (AbstractCompletion α)

Full source

instance AbstractCompletion.inhabited : Inhabited (AbstractCompletion α) :=
  ⟨cPkg⟩

Nonemptiness of Abstract Completions of Uniform Spaces

Informal description

For any uniform space $\alpha$, the abstract completion of $\alpha$ is inhabited (i.e., nonempty).

UniformSpace.Completion.nonempty_completion_iff theorem

: Nonempty (Completion α) ↔ Nonempty α

Full source

theorem nonempty_completion_iff : NonemptyNonempty (Completion α) ↔ Nonempty α :=
  cPkg.dense.nonempty_iff.symm

Nonempty Completion iff Nonempty Space

Informal description

The Hausdorff completion $\text{Completion}(\alpha)$ of a uniform space $\alpha$ is nonempty if and only if $\alpha$ is nonempty.

UniformSpace.Completion.uniformContinuous_coe theorem

: UniformContinuous ((↑) : α → Completion α)

Full source

theorem uniformContinuous_coe : UniformContinuous ((↑) : α → Completion α) :=
  cPkg.uniformContinuous_coe

Uniform Continuity of the Canonical Embedding into Hausdorff Completion

Informal description

The canonical embedding $(↑) \colon \alpha \to \text{Completion}(\alpha)$ from a uniform space $\alpha$ to its Hausdorff completion is uniformly continuous.

UniformSpace.Completion.continuous_coe theorem

: Continuous ((↑) : α → Completion α)

Full source

theorem continuous_coe : Continuous ((↑) : α → Completion α) :=
  cPkg.continuous_coe

Continuity of the Canonical Embedding into Hausdorff Completion

Informal description

The canonical embedding $(↑) \colon \alpha \to \text{Completion}(\alpha)$ from a uniform space $\alpha$ to its Hausdorff completion is continuous.

UniformSpace.Completion.isUniformEmbedding_coe theorem

[T0Space α] : IsUniformEmbedding ((↑) : α → Completion α)

Full source

theorem isUniformEmbedding_coe [T0Space α] : IsUniformEmbedding ((↑) : α → Completion α) :=
  { comap_uniformity := comap_coe_eq_uniformity α
    injective := separated_pureCauchy_injective }

Canonical Embedding into Hausdorff Completion is Uniform Embedding for T₀ Spaces

Informal description

For a uniform space $\alpha$ that is also a T₀ space, the canonical embedding $(↑) \colon \alpha \to \text{Completion}(\alpha)$ into its Hausdorff completion is a uniform embedding. That is: 1. The map is injective. 2. It is uniformly continuous. 3. The uniformity on $\alpha$ is induced by the uniformity on $\text{Completion}(\alpha)$ via this embedding.

UniformSpace.Completion.coe_injective theorem

[T0Space α] : Function.Injective ((↑) : α → Completion α)

Full source

theorem coe_injective [T0Space α] : Function.Injective ((↑) : α → Completion α) :=
  IsUniformEmbedding.injective (isUniformEmbedding_coe _)

Injectivity of the Canonical Embedding into Hausdorff Completion for T₀ Spaces

Informal description

For a uniform space $\alpha$ that is a T₀ space, the canonical embedding $(↑) \colon \alpha \to \text{Completion}(\alpha)$ into its Hausdorff completion is injective. That is, for any $x, y \in \alpha$, if $x = y$ in $\text{Completion}(\alpha)$, then $x = y$ in $\alpha$.

UniformSpace.Completion.isDenseInducing_coe theorem

: IsDenseInducing ((↑) : α → Completion α)

Full source

theorem isDenseInducing_coe : IsDenseInducing ((↑) : α → Completion α) :=
  { (isUniformInducing_coe α).isInducing with dense := denseRange_coe }

Canonical Embedding into Hausdorff Completion is Dense and Inducing

Informal description

The canonical embedding $(↑) \colon \alpha \to \text{Completion}(\alpha)$ from a uniform space $\alpha$ to its Hausdorff completion is both dense and inducing with respect to the topology. This means: 1. The image of $\alpha$ under $(↑)$ is dense in $\text{Completion}(\alpha)$. 2. The topology on $\alpha$ coincides with the subspace topology induced by the embedding into $\text{Completion}(\alpha)$.

UniformSpace.Completion.UniformCompletion.completeEquivSelf definition

[CompleteSpace α] [T0Space α] : Completion α ≃ᵤ α

Full source

/-- The uniform bijection between a complete space and its uniform completion. -/
def UniformCompletion.completeEquivSelf [CompleteSpace α] [T0Space α] : CompletionCompletion α ≃ᵤ α :=
  AbstractCompletion.compareEquiv Completion.cPkg AbstractCompletion.ofComplete

Uniform isomorphism between completion and complete space

Informal description

When $\alpha$ is a complete Hausdorff uniform space, there exists a uniform isomorphism between its Hausdorff completion $\text{Completion}(\alpha)$ and $\alpha$ itself. This isomorphism is constructed by comparing the abstract completion package of $\alpha$ with the identity completion structure on $\alpha$.

UniformSpace.Completion.separableSpace_completion instance

[SeparableSpace α] : SeparableSpace (Completion α)

Full source

instance separableSpace_completion [SeparableSpace α] : SeparableSpace (Completion α) :=
  Completion.isDenseInducing_coe.separableSpace

Separability of the Hausdorff Completion

Informal description

If a uniform space $\alpha$ is separable, then its Hausdorff completion $\text{Completion}(\alpha)$ is also separable.

UniformSpace.Completion.isDenseEmbedding_coe theorem

[T0Space α] : IsDenseEmbedding ((↑) : α → Completion α)

Full source

theorem isDenseEmbedding_coe [T0Space α] : IsDenseEmbedding ((↑) : α → Completion α) :=
  { isDenseInducing_coe with injective := separated_pureCauchy_injective }

Dense Embedding Property of the Canonical Map into Hausdorff Completion for T₀ Uniform Spaces

Informal description

For a uniform space $\alpha$ that is also a T₀ space, the canonical embedding $(↑) \colon \alpha \to \text{Completion}(\alpha)$ into its Hausdorff completion is a dense embedding. This means: 1. The map is injective and induces the original topology on $\alpha$. 2. The image of $\alpha$ under $(↑)$ is dense in $\text{Completion}(\alpha)$.

UniformSpace.Completion.denseRange_coe₂ theorem

: DenseRange fun x : α × β => ((x.1 : Completion α), (x.2 : Completion β))

Full source

theorem denseRange_coe₂ :
    DenseRange fun x : α × β => ((x.1 : Completion α), (x.2 : Completion β)) :=
  denseRange_coe.prodMap denseRange_coe

Density of the Canonical Embedding in the Product of Completions

Informal description

The image of the map $(x,y) \mapsto (x, y)$, where $x \in \alpha$ and $y \in \beta$, under the canonical embeddings into the completions $\text{Completion}(\alpha)$ and $\text{Completion}(\beta)$ respectively, is dense in the product space $\text{Completion}(\alpha) \times \text{Completion}(\beta)$.

UniformSpace.Completion.denseRange_coe₃ theorem

: DenseRange fun x : α × β × γ => ((x.1 : Completion α), ((x.2.1 : Completion β), (x.2.2 : Completion γ)))

Full source

theorem denseRange_coe₃ :
    DenseRange fun x : α × β × γ =>
      ((x.1 : Completion α), ((x.2.1 : Completion β), (x.2.2 : Completion γ))) :=
  denseRange_coe.prodMap denseRange_coe₂

Density of the Canonical Embedding in the Triple Product of Completions

Informal description

The image of the map $(x,y,z) \mapsto (x, y, z)$, where $x \in \alpha$, $y \in \beta$, and $z \in \gamma$, under the canonical embeddings into the completions $\text{Completion}(\alpha)$, $\text{Completion}(\beta)$, and $\text{Completion}(\gamma)$ respectively, is dense in the product space $\text{Completion}(\alpha) \times \text{Completion}(\beta) \times \text{Completion}(\gamma)$.

UniformSpace.Completion.induction_on theorem

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

Full source

@[elab_as_elim]
theorem induction_on {p : Completion α → Prop} (a : Completion α) (hp : IsClosed { a | p a })
    (ih : ∀ a : α, p a) : p a :=
  isClosed_property denseRange_coe hp ih a

Induction Principle for Hausdorff Completion of Uniform Spaces

Informal description

Let $\alpha$ be a uniform space and $\text{Completion}(\alpha)$ its Hausdorff completion. For any predicate $p : \text{Completion}(\alpha) \to \text{Prop}$ and any element $a \in \text{Completion}(\alpha)$, if the set $\{a \mid p a\}$ is closed and $p$ holds for all elements in the image of the canonical embedding $\alpha \to \text{Completion}(\alpha)$, then $p$ holds for $a$.

UniformSpace.Completion.induction_on₂ theorem

 {p : Completion α → Completion β → Prop} (a : Completion α) (b : Completion β)
  (hp : IsClosed {x : Completion α × Completion β | p x.1 x.2}) (ih : ∀ (a : α) (b : β), p a b) : p a b

Full source

@[elab_as_elim]
theorem induction_on₂ {p : Completion α → Completion β → Prop} (a : Completion α) (b : Completion β)
    (hp : IsClosed { x : Completion α × Completion β | p x.1 x.2 })
    (ih : ∀ (a : α) (b : β), p a b) : p a b :=
  have : ∀ x : CompletionCompletion α × Completion β, p x.1 x.2 :=
    isClosed_property denseRange_coe₂ hp fun ⟨a, b⟩ => ih a b
  this (a, b)

Induction Principle for Pairs in Hausdorff Completions of Uniform Spaces

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with their Hausdorff completions $\text{Completion}(\alpha)$ and $\text{Completion}(\beta)$. For any predicate $p : \text{Completion}(\alpha) \times \text{Completion}(\beta) \to \text{Prop}$ and any elements $a \in \text{Completion}(\alpha)$, $b \in \text{Completion}(\beta)$, if the set $\{(x,y) \mid p\,x\,y\}$ is closed and $p$ holds for all pairs $(a,b)$ in the image of the canonical embeddings $\alpha \to \text{Completion}(\alpha)$ and $\beta \to \text{Completion}(\beta)$, then $p$ holds for $(a,b)$.

UniformSpace.Completion.induction_on₃ theorem

 {p : Completion α → Completion β → Completion γ → Prop} (a : Completion α) (b : Completion β) (c : Completion γ)
  (hp : IsClosed {x : Completion α × Completion β × Completion γ | p x.1 x.2.1 x.2.2})
  (ih : ∀ (a : α) (b : β) (c : γ), p a b c) : p a b c

Full source

@[elab_as_elim]
theorem induction_on₃ {p : Completion α → Completion β → Completion γ → Prop} (a : Completion α)
    (b : Completion β) (c : Completion γ)
    (hp : IsClosed { x : Completion α × Completion β × Completion γ | p x.1 x.2.1 x.2.2 })
    (ih : ∀ (a : α) (b : β) (c : γ), p a b c) : p a b c :=
  have : ∀ x : CompletionCompletion α × Completion β × Completion γ, p x.1 x.2.1 x.2.2 :=
    isClosed_property denseRange_coe₃ hp fun ⟨a, b, c⟩ => ih a b c
  this (a, b, c)

Triple Induction Principle for Hausdorff Completions of Uniform Spaces

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces with their Hausdorff completions $\text{Completion}(\alpha)$, $\text{Completion}(\beta)$, and $\text{Completion}(\gamma)$. For any predicate $p : \text{Completion}(\alpha) \times \text{Completion}(\beta) \times \text{Completion}(\gamma) \to \text{Prop}$ and any elements $a \in \text{Completion}(\alpha)$, $b \in \text{Completion}(\beta)$, $c \in \text{Completion}(\gamma)$, if the set $\{(x,y,z) \mid p\,x\,y\,z\}$ is closed and $p$ holds for all triples $(a,b,c)$ in the image of the canonical embeddings $\alpha \to \text{Completion}(\alpha)$, $\beta \to \text{Completion}(\beta)$, and $\gamma \to \text{Completion}(\gamma)$, then $p$ holds for $(a,b,c)$.

UniformSpace.Completion.ext theorem

 {Y : Type*} [TopologicalSpace Y] [T2Space Y] {f g : Completion α → Y} (hf : Continuous f) (hg : Continuous g)
  (h : ∀ a : α, f a = g a) : f = g

Full source

theorem ext {Y : Type*} [TopologicalSpace Y] [T2Space Y] {f g : Completion α → Y}
    (hf : Continuous f) (hg : Continuous g) (h : ∀ a : α, f a = g a) : f = g :=
  cPkg.funext hf hg h

Uniqueness of Continuous Extensions from Completion to Hausdorff Space

Informal description

Let $Y$ be a Hausdorff topological space, and let $f, g \colon \text{Completion}(\alpha) \to Y$ be continuous functions. If $f$ and $g$ agree on the image of $\alpha$ in its completion (i.e., $f(a) = g(a)$ for all $a \in \alpha$), then $f = g$.

UniformSpace.Completion.ext' theorem

 {Y : Type*} [TopologicalSpace Y] [T2Space Y] {f g : Completion α → Y} (hf : Continuous f) (hg : Continuous g)
  (h : ∀ a : α, f a = g a) (a : Completion α) : f a = g a

Full source

theorem ext' {Y : Type*} [TopologicalSpace Y] [T2Space Y] {f g : Completion α → Y}
    (hf : Continuous f) (hg : Continuous g) (h : ∀ a : α, f a = g a) (a : Completion α) :
    f a = g a :=
  congr_fun (ext hf hg h) a

Pointwise Uniqueness of Continuous Extensions from Completion to Hausdorff Space

Informal description

Let $Y$ be a Hausdorff topological space, and let $f, g \colon \text{Completion}(\alpha) \to Y$ be continuous functions. If $f$ and $g$ agree on the image of $\alpha$ in its completion (i.e., $f(a) = g(a)$ for all $a \in \alpha$), then $f$ and $g$ agree at every point of $\text{Completion}(\alpha)$, i.e., $f(a) = g(a)$ for all $a \in \text{Completion}(\alpha)$.

UniformSpace.Completion.extension definition

(f : α → β) : Completion α → β

Full source

/-- "Extension" to the completion. It is defined for any map `f` but
returns an arbitrary constant value if `f` is not uniformly continuous -/
protected def extension (f : α → β) : Completion α → β :=
  cPkg.extend f

Extension of maps to the Hausdorff completion

Informal description

The function `UniformSpace.Completion.extension` extends any map $f \colon \alpha \to \beta$ to a map $\text{Completion}(\alpha) \to \beta$, where $\text{Completion}(\alpha)$ is the Hausdorff completion of the uniform space $\alpha$. If $f$ is uniformly continuous, the extension is constructed canonically; otherwise, the extension is defined arbitrarily (using the axiom of choice).

UniformSpace.Completion.uniformContinuous_extension theorem

: UniformContinuous (Completion.extension f)

Full source

theorem uniformContinuous_extension : UniformContinuous (Completion.extension f) :=
  cPkg.uniformContinuous_extend

Uniform Continuity of the Extension to Hausdorff Completion

Informal description

The extension map $\text{Completion.extension}(f) \colon \text{Completion}(\alpha) \to \beta$ is uniformly continuous when $f \colon \alpha \to \beta$ is uniformly continuous.

UniformSpace.Completion.continuous_extension theorem

: Continuous (Completion.extension f)

Full source

@[continuity, fun_prop]
theorem continuous_extension : Continuous (Completion.extension f) :=
  cPkg.continuous_extend

Continuity of the Extension Map to the Hausdorff Completion

Informal description

The extension map $\text{Completion.extension}(f) : \text{Completion}(\alpha) \to \beta$ is continuous for any map $f : \alpha \to \beta$.

UniformSpace.Completion.extension_coe theorem

[T0Space β] (hf : UniformContinuous f) (a : α) : (Completion.extension f) a = f a

Full source

theorem extension_coe [T0Space β] (hf : UniformContinuous f) (a : α) :
    (Completion.extension f) a = f a :=
  cPkg.extend_coe hf a

Extension of Uniformly Continuous Maps Preserves Values on Original Space

Informal description

Let $\alpha$ be a uniform space and $\beta$ a T₀ space. For any uniformly continuous function $f \colon \alpha \to \beta$ and any point $a \in \alpha$, the extension $\overline{f} \colon \text{Completion}(\alpha) \to \beta$ satisfies $\overline{f}(a) = f(a)$, where $a$ is viewed as an element of $\text{Completion}(\alpha)$ via the canonical embedding.

UniformSpace.Completion.extension_unique theorem

 (hf : UniformContinuous f) {g : Completion α → β} (hg : UniformContinuous g)
  (h : ∀ a : α, f a = g (a : Completion α)) : Completion.extension f = g

Full source

theorem extension_unique (hf : UniformContinuous f) {g : Completion α → β}
    (hg : UniformContinuous g) (h : ∀ a : α, f a = g (a : Completion α)) :
    Completion.extension f = g :=
  cPkg.extend_unique hf hg h

Uniqueness of Uniformly Continuous Extensions to Hausdorff Completion

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with $\beta$ complete and Hausdorff. Given a uniformly continuous function $f \colon \alpha \to \beta$, if $g \colon \text{Completion}(\alpha) \to \beta$ is another uniformly continuous function such that $f(a) = g(a)$ for all $a \in \alpha$ (where $a$ is identified with its image in $\text{Completion}(\alpha)$), then the canonical extension $\text{Completion.extension}(f)$ equals $g$.

UniformSpace.Completion.extension_comp_coe theorem

{f : Completion α → β} (hf : UniformContinuous f) : Completion.extension (f ∘ (↑)) = f

Full source

@[simp]
theorem extension_comp_coe {f : Completion α → β} (hf : UniformContinuous f) :
    Completion.extension (f ∘ (↑)) = f :=
  cPkg.extend_comp_coe hf

Extension of Composition with Embedding Equals Original Function

Informal description

For any uniformly continuous function $f \colon \text{Completion}(\alpha) \to \beta$, the extension of the composition $f \circ \iota$ equals $f$, where $\iota \colon \alpha \to \text{Completion}(\alpha)$ is the canonical embedding. That is, $\text{extension}(f \circ \iota) = f$.

UniformSpace.Completion.map definition

(f : α → β) : Completion α → Completion β

Full source

/-- Completion functor acting on morphisms -/
protected def map (f : α → β) : Completion α → Completion β :=
  cPkg.map cPkg f

Completion functor on maps between uniform spaces

Informal description

Given a uniformly continuous map $ f \colon \alpha \to \beta $ between uniform spaces, the function `UniformSpace.Completion.map` lifts $ f $ to a uniformly continuous map between their Hausdorff completions, $ \text{Completion}(\alpha) \to \text{Completion}(\beta) $, such that the diagram commutes: \[ \begin{CD} \alpha @>{f}>> \beta \\ @VVV @VVV \\ \text{Completion}(\alpha) @>{\text{Completion.map }f}>> \text{Completion}(\beta) \end{CD} \] where the vertical maps are the canonical embeddings.

UniformSpace.Completion.uniformContinuous_map theorem

: UniformContinuous (Completion.map f)

Full source

theorem uniformContinuous_map : UniformContinuous (Completion.map f) :=
  cPkg.uniformContinuous_map cPkg f

Uniform Continuity of the Completion Functor

Informal description

For any uniformly continuous map $f \colon \alpha \to \beta$ between uniform spaces, the induced map $\text{Completion}(f) \colon \text{Completion}(\alpha) \to \text{Completion}(\beta)$ between their Hausdorff completions is uniformly continuous.

UniformSpace.Completion.continuous_map theorem

: Continuous (Completion.map f)

Full source

@[continuity]
theorem continuous_map : Continuous (Completion.map f) :=
  cPkg.continuous_map cPkg f

Continuity of the Completion Map

Informal description

For any uniformly continuous map $f \colon \alpha \to \beta$ between uniform spaces, the induced map $\text{Completion}(f) \colon \text{Completion}(\alpha) \to \text{Completion}(\beta)$ on their Hausdorff completions is continuous.

UniformSpace.Completion.map_coe theorem

(hf : UniformContinuous f) (a : α) : (Completion.map f) a = f a

Full source

theorem map_coe (hf : UniformContinuous f) (a : α) : (Completion.map f) a = f a :=
  cPkg.map_coe cPkg hf a

Completion Functor Commutes with Canonical Embedding

Informal description

For any uniformly continuous function $f \colon \alpha \to \beta$ between uniform spaces and any element $a \in \alpha$, the completion map $\text{Completion.map}(f)$ applied to the canonical embedding of $a$ in $\text{Completion}(\alpha)$ equals the canonical embedding of $f(a)$ in $\text{Completion}(\beta)$. In other words, the following diagram commutes: \[ \text{Completion.map}(f)((a)) = (f(a)) \] where $(a)$ denotes the canonical embedding of $a$ into $\text{Completion}(\alpha)$ and $(f(a))$ denotes the canonical embedding of $f(a)$ into $\text{Completion}(\beta)$.

UniformSpace.Completion.map_unique theorem

 {f : α → β} {g : Completion α → Completion β} (hg : UniformContinuous g) (h : ∀ a : α, ↑(f a) = g a) :
  Completion.map f = g

Full source

theorem map_unique {f : α → β} {g : Completion α → Completion β} (hg : UniformContinuous g)
    (h : ∀ a : α, ↑(f a) = g a) : Completion.map f = g :=
  cPkg.map_unique cPkg hg h

Uniqueness of Uniformly Continuous Extension from Completion

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with Hausdorff completions $\text{Completion}(\alpha)$ and $\text{Completion}(\beta)$, respectively. Let $f \colon \alpha \to \beta$ be a map and $g \colon \text{Completion}(\alpha) \to \text{Completion}(\beta)$ be a uniformly continuous map such that for every $a \in \alpha$, the canonical embedding of $f(a)$ in $\text{Completion}(\beta)$ equals $g$ applied to the canonical embedding of $a$ in $\text{Completion}(\alpha)$. Then the completion map $\text{Completion.map}(f)$ coincides with $g$.

UniformSpace.Completion.map_id theorem

: Completion.map (@id α) = id

Full source

@[simp]
theorem map_id : Completion.map (@id α) = id :=
  cPkg.map_id

Completion Functor Preserves Identity: $\text{Completion.map}(\text{id}) = \text{id}$

Informal description

The completion functor applied to the identity map $\text{id} \colon \alpha \to \alpha$ on a uniform space $\alpha$ yields the identity map $\text{id} \colon \text{Completion}(\alpha) \to \text{Completion}(\alpha)$ on its Hausdorff completion.

UniformSpace.Completion.extension_map theorem

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

Full source

theorem extension_map [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β}
    (hf : UniformContinuous f) (hg : UniformContinuous g) :
    Completion.extensionCompletion.extension f ∘ Completion.map g = Completion.extension (f ∘ g) :=
  Completion.ext (continuous_extension.comp continuous_map) continuous_extension <| by
    simp [hf, hg, hf.comp hg, map_coe, extension_coe]

Commutativity of Extension and Completion for Uniformly Continuous Maps

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces, with $\gamma$ complete and T₀. For any uniformly continuous maps $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$, the extension of $f$ composed with the completion map of $g$ equals the extension of the composition $f \circ g$. That is, \[ \overline{f} \circ \widehat{g} = \overline{f \circ g}, \] where $\overline{f} \colon \text{Completion}(\beta) \to \gamma$ is the extension of $f$, $\widehat{g} \colon \text{Completion}(\alpha) \to \text{Completion}(\beta)$ is the completion map of $g$, and $\overline{f \circ g} \colon \text{Completion}(\alpha) \to \gamma$ is the extension of $f \circ g$.

UniformSpace.Completion.map_comp theorem

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

Full source

theorem map_comp {g : β → γ} {f : α → β} (hg : UniformContinuous g) (hf : UniformContinuous f) :
    Completion.mapCompletion.map g ∘ Completion.map f = Completion.map (g ∘ f) :=
  extension_map ((uniformContinuous_coe _).comp hg) hf

Functoriality of Completion: $\widehat{g} \circ \widehat{f} = \widehat{g \circ f}$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces. For any uniformly continuous maps $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the composition of their completion maps equals the completion map of their composition. That is, \[ \widehat{g} \circ \widehat{f} = \widehat{g \circ f}, \] where $\widehat{f} \colon \text{Completion}(\alpha) \to \text{Completion}(\beta)$ and $\widehat{g} \colon \text{Completion}(\beta) \to \text{Completion}(\gamma)$ are the completion maps of $f$ and $g$ respectively, and $\widehat{g \circ f} \colon \text{Completion}(\alpha) \to \text{Completion}(\gamma)$ is the completion map of $g \circ f$.

UniformSpace.Completion.completionSeparationQuotientEquiv definition

(α : Type u) [UniformSpace α] : Completion (SeparationQuotient α) ≃ Completion α

Full source

/-- The isomorphism between the completion of a uniform space and the completion of its separation
quotient. -/
def completionSeparationQuotientEquiv (α : Type u) [UniformSpace α] :
    CompletionCompletion (SeparationQuotient α) ≃ Completion α := by
  refine ⟨Completion.extension (lift' ((↑) : α → Completion α)),
    Completion.map SeparationQuotient.mk, fun a ↦ ?_, fun a ↦ ?_⟩
  · refine induction_on a (isClosed_eq (continuous_map.comp continuous_extension) continuous_id) ?_
    refine SeparationQuotient.surjective_mk.forall.2 fun a ↦ ?_
    rw [extension_coe (uniformContinuous_lift' _), lift'_mk (uniformContinuous_coe α),
      map_coe uniformContinuous_mk]
  · refine induction_on a
      (isClosed_eq (continuous_extension.comp continuous_map) continuous_id) fun a ↦ ?_
    rw [map_coe uniformContinuous_mk, extension_coe (uniformContinuous_lift' _),
      lift'_mk (uniformContinuous_coe _)]

Isomorphism between completions of a uniform space and its separation quotient

Informal description

The isomorphism between the Hausdorff completion of a uniform space $\alpha$ and the Hausdorff completion of its separation quotient $\text{SeparationQuotient}(\alpha)$. More precisely, there exists a bijection $\text{Completion}(\text{SeparationQuotient}(\alpha)) \simeq \text{Completion}(\alpha)$ that is uniformly continuous in both directions. This isomorphism is constructed using the canonical maps: - $\text{Completion.extension}$ applied to the lift of the embedding $\alpha \to \text{Completion}(\alpha)$ - $\text{Completion.map}$ applied to the quotient map $\alpha \to \text{SeparationQuotient}(\alpha)$

UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv theorem

: UniformContinuous (completionSeparationQuotientEquiv α)

Full source

theorem uniformContinuous_completionSeparationQuotientEquiv :
    UniformContinuous (completionSeparationQuotientEquiv α) :=
  uniformContinuous_extension

Uniform Continuity of the Completion-Separation Quotient Isomorphism

Informal description

The isomorphism $\text{Completion}(\text{SeparationQuotient}(\alpha)) \simeq \text{Completion}(\alpha)$ is uniformly continuous.

UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv_symm theorem

: UniformContinuous (completionSeparationQuotientEquiv α).symm

Full source

theorem uniformContinuous_completionSeparationQuotientEquiv_symm :
    UniformContinuous (completionSeparationQuotientEquiv α).symm :=
  uniformContinuous_map

Uniform Continuity of the Inverse Completion-Separation Quotient Isomorphism

Informal description

The inverse of the isomorphism $\text{Completion}(\text{SeparationQuotient}(\alpha)) \simeq \text{Completion}(\alpha)$ is uniformly continuous.

UniformSpace.Completion.extension₂ definition

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

Full source

/-- Extend a two variable map to the Hausdorff completions. -/
protected def extension₂ (f : α → β → γ) : Completion α → Completion β → γ :=
  cPkg.extend₂ cPkg f

Extension of a two-variable map to Hausdorff completions

Informal description

The function extends a two-variable map $ f : \alpha \to \beta \to \gamma $ to the Hausdorff completions of $\alpha$ and $\beta$, yielding a map $ \text{Completion}(\alpha) \to \text{Completion}(\beta) \to \gamma $. This extension is constructed by first uncurrying $ f $ to $ \alpha \times \beta \to \gamma $, extending it to the completion $ \widehat{\alpha \times \beta} $, and then currying back to $ \text{Completion}(\alpha) \to \text{Completion}(\beta) \to \gamma $.

UniformSpace.Completion.extension₂_coe_coe theorem

(hf : UniformContinuous₂ f) (a : α) (b : β) : Completion.extension₂ f a b = f a b

Full source

theorem extension₂_coe_coe (hf : UniformContinuous₂ f) (a : α) (b : β) :
    Completion.extension₂ f a b = f a b :=
  cPkg.extension₂_coe_coe cPkg hf a b

Extension of Uniformly Continuous Bivariate Function Preserves Values on Original Space

Informal description

Let $\alpha$ and $\beta$ be uniform spaces with Hausdorff completions $\text{Completion}(\alpha)$ and $\text{Completion}(\beta)$, respectively. Let $f : \alpha \to \beta \to \gamma$ be a uniformly continuous function in two variables. Then for any $a \in \alpha$ and $b \in \beta$, the extension of $f$ to the completions satisfies: \[ \text{extension}_2(f)(a, b) = f(a, b), \] where $a$ and $b$ are identified with their images under the canonical embeddings into their respective completions.

UniformSpace.Completion.uniformContinuous_extension₂ theorem

: UniformContinuous₂ (Completion.extension₂ f)

Full source

theorem uniformContinuous_extension₂ : UniformContinuous₂ (Completion.extension₂ f) :=
  cPkg.uniformContinuous_extension₂ cPkg f

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

Informal description

The extension of a two-variable function $f \colon \alpha \to \beta \to \gamma$ to the Hausdorff completions $\text{Completion}(\alpha) \to \text{Completion}(\beta) \to \gamma$ is uniformly continuous in both variables.

UniformSpace.Completion.map₂ definition

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

Full source

/-- Lift a two variable map to the Hausdorff completions. -/
protected def map₂ (f : α → β → γ) : Completion α → Completion β → Completion γ :=
  cPkg.map₂ cPkg cPkg f

Extension of a two-variable map to Hausdorff completions

Informal description

Given a function $ f : \alpha \to \beta \to \gamma $, the function `UniformSpace.Completion.map₂` extends $ f $ to a function $ \text{Completion}(\alpha) \to \text{Completion}(\beta) \to \text{Completion}(\gamma) $ on the Hausdorff completions of $ \alpha $, $ \beta $, and $ \gamma $. This extension preserves the uniform structure and is constructed using the abstract completion package for uniform spaces.

UniformSpace.Completion.uniformContinuous_map₂ theorem

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

Full source

theorem uniformContinuous_map₂ (f : α → β → γ) : UniformContinuous₂ (Completion.map₂ f) :=
  cPkg.uniformContinuous_map₂ cPkg cPkg f

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

Informal description

For any function $f \colon \alpha \to \beta \to \gamma$ between uniform spaces, the extension $\text{Completion.map}_2 f \colon \text{Completion}(\alpha) \to \text{Completion}(\beta) \to \text{Completion}(\gamma)$ is uniformly continuous in both arguments.

UniformSpace.Completion.continuous_map₂ theorem

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

Full source

theorem continuous_map₂ {δ} [TopologicalSpace δ] {f : α → β → γ} {a : δ → Completion α}
    {b : δ → Completion β} (ha : Continuous a) (hb : Continuous b) :
    Continuous fun d : δ => Completion.map₂ f (a d) (b d) :=
  cPkg.continuous_map₂ cPkg cPkg ha hb

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

Informal description

Let $\delta$ be a topological space and $f \colon \alpha \to \beta \to \gamma$ be a function. Given continuous maps $a \colon \delta \to \text{Completion}(\alpha)$ and $b \colon \delta \to \text{Completion}(\beta)$, the function $d \mapsto \text{Completion.map₂} f (a(d)) (b(d))$ is continuous from $\delta$ to $\text{Completion}(\gamma)$.

UniformSpace.Completion.map₂_coe_coe theorem

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

Full source

theorem map₂_coe_coe (a : α) (b : β) (f : α → β → γ) (hf : UniformContinuous₂ f) :
    Completion.map₂ f (a : Completion α) (b : Completion β) = f a b :=
  cPkg.map₂_coe_coe cPkg cPkg a b f hf

Extension of Uniformly Continuous Bivariate Function Preserves Values on Original Space

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be uniform spaces with Hausdorff completions $\text{Completion}(\alpha)$, $\text{Completion}(\beta)$, and $\text{Completion}(\gamma)$ respectively. Let $f \colon \alpha \to \beta \to \gamma$ be a uniformly continuous function in two variables. Then for any $a \in \alpha$ and $b \in \beta$, the extension of $f$ to the completions satisfies: \[ \text{map}_2(f)(a, b) = f(a, b), \] where $a$ and $b$ are interpreted as elements of their respective completions via the canonical embedding.

References