Cauchy filters on metric spaces

Content created by malarbol.

Created on 2026-10-18.
Last modified on 2026-10-18.

module metric-spaces.cauchy-filters-metric-spaces where
Imports 
open import elementary-number-theory.addition-positive-rational-numbers
open import elementary-number-theory.positive-rational-numbers
open import elementary-number-theory.strict-inequality-positive-rational-numbers

open import foundation.universe-levels

open import metric-spaces.cauchy-filters-pseudometric-spaces
open import metric-spaces.local-rational-neighborhood-subtypes-pseudometric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.proper-rational-neighborhood-subtypes
open import metric-spaces.rational-neighborhood-subtypes
open import metric-spaces.saturated-rational-neighborhood-subtypes

Idea

A Cauchy filter on a metric space M is a Cauchy filter on the underlying pseudometric space.

The type of Cauchy filters is equipped with a unit map η : M → F(M); it can be equipped with a metric structure turning F(M) into a complete metric space where η is an isometry.

Definitions

The type of Cauchy filters on a metric space

module _
  {l1 l2 : Level} (l : Level) (M : Metric-Space l1 l2)
  where

  cauchy-filter-Metric-Space : UU (l1 ⊔ l2 ⊔ lsuc l)
  cauchy-filter-Metric-Space =
    cauchy-filter-Pseudometric-Space l (pseudometric-Metric-Space M)

Components of Cauchy filters

module _
  {l1 l2 l : Level} (M : Metric-Space l1 l2)
  (U : cauchy-filter-Metric-Space l M)
  where

  neighborhood-subtype-cauchy-filter-Metric-Space :
    Rational-Neighborhood-Subtype l (type-Metric-Space M)
  neighborhood-subtype-cauchy-filter-Metric-Space =
    neighborhood-subtype-cauchy-filter-Pseudometric-Space
      ( pseudometric-Metric-Space M)
      ( U)

  is-in-cauchy-filter-Metric-Space : ℚ⁺ → type-Metric-Space M → UU l
  is-in-cauchy-filter-Metric-Space =
    is-in-cauchy-filter-Pseudometric-Space
      ( pseudometric-Metric-Space M)
      ( U)

  abstract
    is-cauchy-filter-neighborhood-subtype-cauchy-filter-Metric-Space :
      is-cauchy-filter-Pseudometric-Space
        ( l)
        ( pseudometric-Metric-Space M)
        ( neighborhood-subtype-cauchy-filter-Metric-Space)
    is-cauchy-filter-neighborhood-subtype-cauchy-filter-Metric-Space =
      is-cauchy-filter-neighborhood-subtype-cauchy-filter-Pseudometric-Space
        ( pseudometric-Metric-Space M)
        ( U)

    is-proper-cauchy-filter-Metric-Space :
      is-proper-Rational-Neighborhood-Subtype
        neighborhood-subtype-cauchy-filter-Metric-Space
    is-proper-cauchy-filter-Metric-Space =
      is-proper-cauchy-filter-Pseudometric-Space
        ( pseudometric-Metric-Space M)
        ( U)

    is-saturated-cauchy-filter-Metric-Space :
      is-saturated-Rational-Neighborhood-Subtype
        neighborhood-subtype-cauchy-filter-Metric-Space
    is-saturated-cauchy-filter-Metric-Space =
      is-saturated-cauchy-filter-Pseudometric-Space
        ( pseudometric-Metric-Space M)
        ( U)

    is-local-cauchy-filter-Metric-Space :
      is-local-neighborhood-subtype-Pseudometric-Space
        ( pseudometric-Metric-Space M)
        ( neighborhood-subtype-cauchy-filter-Metric-Space)
    is-local-cauchy-filter-Metric-Space =
      is-local-cauchy-filter-Pseudometric-Space
        ( pseudometric-Metric-Space M)
        ( U)

    is-bounded-cauchy-filter-Metric-Space :
      (ε δ : ℚ⁺) (x y : type-Metric-Space M) →
      is-in-cauchy-filter-Metric-Space ε x →
      is-in-cauchy-filter-Metric-Space δ y →
      neighborhood-Metric-Space M (ε +ℚ⁺ δ) x y
    is-bounded-cauchy-filter-Metric-Space =
      is-bounded-cauchy-filter-Pseudometric-Space
        ( pseudometric-Metric-Space M)
        ( U)

    is-enclosing-cauchy-filter-Metric-Space :
      (ε δ : ℚ⁺) (x y : type-Metric-Space M) →
      is-in-cauchy-filter-Metric-Space ε x →
      neighborhood-Metric-Space M δ x y →
      is-in-cauchy-filter-Metric-Space (ε +ℚ⁺ δ) y
    is-enclosing-cauchy-filter-Metric-Space =
      is-enclosing-cauchy-filter-Pseudometric-Space
        ( pseudometric-Metric-Space M)
        ( U)

The unit map of Cauchy filters

module _
  {l1 l2 : Level} (M : Metric-Space l1 l2)
  where

  map-unit-cauchy-filter-Metric-Space :
    type-Metric-Space M → cauchy-filter-Metric-Space l2 M
  map-unit-cauchy-filter-Metric-Space =
    map-unit-cauchy-filter-Pseudometric-Space
      ( pseudometric-Metric-Space M)

Properties

Cauchy filters are monotonic

For any Cauchy filter U and ε δ : ℚ⁺ with ε < δ, Uε ⊆ Uδ.

module _
  {l1 l2 l : Level} (M : Metric-Space l1 l2)
  (U : cauchy-filter-Metric-Space l M)
  where abstract

  is-monotonic-cauchy-filter-Metric-Space :
    ( x : type-Metric-Space M) →
    ( ε δ : ℚ⁺) →
    le-ℚ⁺ ε δ →
    is-in-cauchy-filter-Metric-Space M U ε x →
    is-in-cauchy-filter-Metric-Space M U δ x
  is-monotonic-cauchy-filter-Metric-Space =
    is-monotonic-cauchy-filter-Pseudometric-Space
      ( pseudometric-Metric-Space M)
      ( U)

Any point is in the filter of its image by the unit map

module _
  {l1 l2 : Level} (M : Metric-Space l1 l2)
  where abstract

  is-in-filter-map-unit-cauchy-filter-Metric-Space :
    ( ε : ℚ⁺) →
    ( x : type-Metric-Space M) →
    is-in-cauchy-filter-Metric-Space
      ( M)
      ( map-unit-cauchy-filter-Metric-Space M x)
      ( ε)
      ( x)
  is-in-filter-map-unit-cauchy-filter-Metric-Space ε x =
    refl-neighborhood-Metric-Space M ε x

References

This definition essentially corresponds to “Cauchy filters of formal balls” as described in [Vic05], with closed (i.e. saturated) formal balls.

[Vic05]
Steven Vickers. Localic completion of generalized metric spaces i. Theory and Applications of Categories, 14(15):328–356, 2005. URL: http://www.tac.mta.ca/tac/volumes/14/15/14-15.pdf.

Recent changes