Documentation

Mathlib.Topology.MetricSpace.Gluing

Metric space gluing #

Gluing two metric spaces along a common subset. Formally, we are given

     Φ
  Z ---> X
  |
  |Ψ
  v
  Y

where hΦ : Isometry Φ and hΨ : Isometry Ψ. We want to complete the square by a space GlueSpacescan hΦ hΨ and two isometries toGlueL hΦ hΨ and toGlueR hΦ hΨ that make the square commute. We start by defining a predistance on the disjoint union X ⊕ Y, for which points Φ p and Ψ p are at distance 0. The (quotient) metric space associated to this predistance is the desired space.

This is an instance of a more general construction, where Φ and Ψ do not have to be isometries, but the distances in the image almost coincide, up to say. Then one can almost glue the two spaces so that the images of a point under Φ and Ψ are ε-close. If ε > 0, this yields a metric space structure on X ⊕ Y, without the need to take a quotient. In particular, this gives a natural metric space structure on X ⊕ Y, where the basepoints are at distance 1, say, and the distances between other points are obtained by going through the two basepoints. (We also register the same metric space structure on a general disjoint union Σ i, E i).

We also define the inductive limit of metric spaces. Given

     f 0        f 1        f 2        f 3
X 0 -----> X 1 -----> X 2 -----> X 3 -----> ...

where the X n are metric spaces and f n isometric embeddings, we define the inductive limit of the X n, also known as the increasing union of the X n in this context, if we identify X n and X (n+1) through f n. This is a metric space in which all X n embed isometrically and in a way compatible with f n.

def Metric.glueDist {X : Type u} {Y : Type v} {Z : Type w} [MetricSpace X] [MetricSpace Y] (Φ : ZX) (Ψ : ZY) (ε : ) :
X YX Y

Define a predistance on X ⊕ Y, for which Φ p and Ψ p are at distance ε

Equations
Instances For
    theorem Metric.glueDist_glued_points {X : Type u} {Y : Type v} {Z : Type w} [MetricSpace X] [MetricSpace Y] [Nonempty Z] (Φ : ZX) (Ψ : ZY) (ε : ) (p : Z) :
    Metric.glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
    theorem Metric.glueDist_swap {X : Type u} {Y : Type v} {Z : Type w} [MetricSpace X] [MetricSpace Y] (Φ : ZX) (Ψ : ZY) (ε : ) (x : X Y) (y : X Y) :
    Metric.glueDist Ψ Φ ε x.swap y.swap = Metric.glueDist Φ Ψ ε x y
    theorem Metric.le_glueDist_inl_inr {X : Type u} {Y : Type v} {Z : Type w} [MetricSpace X] [MetricSpace Y] (Φ : ZX) (Ψ : ZY) (ε : ) (x : X) (y : Y) :
    ε Metric.glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y)
    theorem Metric.le_glueDist_inr_inl {X : Type u} {Y : Type v} {Z : Type w} [MetricSpace X] [MetricSpace Y] (Φ : ZX) (Ψ : ZY) (ε : ) (x : Y) (y : X) :
    ε Metric.glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)
    theorem Metric.Sum.mem_uniformity_iff_glueDist {X : Type u} {Y : Type v} {Z : Type w} [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} {ε : } (hε : 0 < ε) (s : Set ((X Y) × (X Y))) :
    s uniformity (X Y) δ > 0, ∀ (a b : X Y), Metric.glueDist Φ Ψ ε a b < δ(a, b) s
    def Metric.glueMetricApprox {X : Type u} {Y : Type v} {Z : Type w} [MetricSpace X] [MetricSpace Y] [Nonempty Z] (Φ : ZX) (Ψ : ZY) (ε : ) (ε0 : 0 < ε) (H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| 2 * ε) :

    Given two maps Φ and Ψ intro metric spaces X and Y such that the distances between Φ p and Φ q, and between Ψ p and Ψ q, coincide up to 2 ε where ε > 0, one can almost glue the two spaces X and Y along the images of Φ and Ψ, so that Φ p and Ψ p are at distance ε.

    Equations
    Instances For

      Metric on X ⊕ Y #

      A particular case of the previous construction is when one uses basepoints in X and Y and one glues only along the basepoints, putting them at distance 1. We give a direct definition of the distance, without iInf, as it is easier to use in applications, and show that it is equal to the gluing distance defined above to take advantage of the lemmas we have already proved.

      def Metric.Sum.dist {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] :
      X YX Y

      Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible with each factor. If the two spaces are bounded, one can say for instance that each point in the first is at distance diam X + diam Y + 1 of each point in the second. Instead, we choose a construction that works for unbounded spaces, but requires basepoints, chosen arbitrarily. We embed isometrically each factor, set the basepoints at distance 1, arbitrarily, and say that the distance from a to b is the sum of the distances of a and b to their respective basepoints, plus the distance 1 between the basepoints. Since there is an arbitrary choice in this construction, it is not an instance by default.

      Equations
      Instances For
        theorem Metric.Sum.dist_eq_glueDist {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] {p : X Y} {q : X Y} (x : X) (y : Y) :
        Metric.Sum.dist p q = Metric.glueDist (fun (x_1 : Unit) => .some) (fun (x : Unit) => .some) 1 p q
        theorem Metric.Sum.one_le_dist_inl_inr {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] {x : X} {y : Y} :
        theorem Metric.Sum.one_le_dist_inr_inl {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] {x : X} {y : Y} :

        The distance on the disjoint union indeed defines a metric space. All the distance properties follow from our choice of the distance. The harder work is to show that the uniform structure defined by the distance coincides with the disjoint union uniform structure.

        Equations
        Instances For
          theorem Metric.Sum.dist_eq {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] {x : X Y} {y : X Y} :
          theorem Metric.isometry_inl {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] :
          Isometry Sum.inl

          The left injection of a space in a disjoint union is an isometry

          theorem Metric.isometry_inr {X : Type u} {Y : Type v} [MetricSpace X] [MetricSpace Y] :
          Isometry Sum.inr

          The right injection of a space in a disjoint union is an isometry

          def Metric.Sigma.dist {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] :
          (i : ι) × E i(i : ι) × E i

          Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible with each factor. We choose a construction that works for unbounded spaces, but requires basepoints, chosen arbitrarily. We embed isometrically each factor, set the basepoints at distance 1, arbitrarily, and say that the distance from a to b is the sum of the distances of a and b to their respective basepoints, plus the distance 1 between the basepoints. Since there is an arbitrary choice in this construction, it is not an instance by default.

          Equations
          Instances For
            def Metric.Sigma.instDist {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] :
            Dist ((i : ι) × E i)

            A Dist instance on the disjoint union Σ i, E i. We embed isometrically each factor, set the basepoints at distance 1, arbitrarily, and say that the distance from a to b is the sum of the distances of a and b to their respective basepoints, plus the distance 1 between the basepoints. Since there is an arbitrary choice in this construction, it is not an instance by default.

            Equations
            • Metric.Sigma.instDist = { dist := Metric.Sigma.dist }
            Instances For
              @[simp]
              theorem Metric.Sigma.dist_same {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] (i : ι) (x : E i) (y : E i) :
              dist i, x i, y = dist x y
              @[simp]
              theorem Metric.Sigma.dist_ne {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] {i : ι} {j : ι} (h : i j) (x : E i) (y : E j) :
              dist i, x j, y = dist x .some + 1 + dist .some y
              theorem Metric.Sigma.one_le_dist_of_ne {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] {i : ι} {j : ι} (h : i j) (x : E i) (y : E j) :
              1 dist i, x j, y
              theorem Metric.Sigma.fst_eq_of_dist_lt_one {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] (x : (i : ι) × E i) (y : (i : ι) × E i) (h : dist x y < 1) :
              x.fst = y.fst
              theorem Metric.Sigma.dist_triangle {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] (x : (i : ι) × E i) (y : (i : ι) × E i) (z : (i : ι) × E i) :
              dist x z dist x y + dist y z
              theorem Metric.Sigma.isOpen_iff {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] (s : Set ((i : ι) × E i)) :
              IsOpen s xs, ε > 0, ∀ (y : (i : ι) × E i), dist x y < εy s
              def Metric.Sigma.metricSpace {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] :
              MetricSpace ((i : ι) × E i)

              A metric space structure on the disjoint union Σ i, E i. We embed isometrically each factor, set the basepoints at distance 1, arbitrarily, and say that the distance from a to b is the sum of the distances of a and b to their respective basepoints, plus the distance 1 between the basepoints. Since there is an arbitrary choice in this construction, it is not an instance by default.

              Equations
              Instances For
                theorem Metric.Sigma.isometry_mk {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] (i : ι) :

                The injection of a space in a disjoint union is an isometry

                theorem Metric.Sigma.completeSpace {ι : Type u_1} {E : ιType u_2} [(i : ι) → MetricSpace (E i)] [∀ (i : ι), CompleteSpace (E i)] :
                CompleteSpace ((i : ι) × E i)

                A disjoint union of complete metric spaces is complete.

                def Metric.gluePremetric {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) :

                Given two isometric embeddings Φ : Z → X and Ψ : Z → Y, we define a pseudo metric space structure on X ⊕ Y by declaring that Φ x and Ψ x are at distance 0.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Metric.GlueSpace {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) :
                  Type (max u v)

                  Given two isometric embeddings Φ : Z → X and Ψ : Z → Y, we define a space GlueSpace hΦ hΨ by identifying in X ⊕ Y the points Φ x and Ψ x.

                  Equations
                  Instances For
                    instance Metric.instMetricSpaceGlueSpace {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) :
                    Equations
                    def Metric.toGlueL {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) (x : X) :

                    The canonical map from X to the space obtained by gluing isometric subsets in X and Y.

                    Equations
                    Instances For
                      def Metric.toGlueR {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) (y : Y) :

                      The canonical map from Y to the space obtained by gluing isometric subsets in X and Y.

                      Equations
                      Instances For
                        instance Metric.inhabitedLeft {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) [Inhabited X] :
                        Equations
                        instance Metric.inhabitedRight {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) [Inhabited Y] :
                        Equations
                        theorem Metric.toGlue_commute {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) :
                        Metric.toGlueL Φ = Metric.toGlueR Ψ
                        theorem Metric.toGlueL_isometry {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) :
                        theorem Metric.toGlueR_isometry {X : Type u} {Y : Type v} {Z : Type w} [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : ZX} {Ψ : ZY} (hΦ : Isometry Φ) (hΨ : Isometry Ψ) :

                        Inductive limit of metric spaces #

                        In this section, we define the inductive limit of

                             f 0        f 1        f 2        f 3
                        X 0 -----> X 1 -----> X 2 -----> X 3 -----> ...
                        

                        where the X n are metric spaces and f n isometric embeddings. We do it by defining a premetric space structure on Σ n, X n, where the predistance dist x y is obtained by pushing x and y in a common X k using composition by the f n, and taking the distance there. This does not depend on the choice of k as the f n are isometries. The metric space associated to this premetric space is the desired inductive limit.

                        def Metric.inductiveLimitDist {X : Type u} [(n : ) → MetricSpace (X n)] (f : (n : ) → X nX (n + 1)) (x : (n : ) × X n) (y : (n : ) × X n) :

                        Predistance on the disjoint union Σ n, X n.

                        Equations
                        Instances For
                          theorem Metric.inductiveLimitDist_eq_dist {X : Type u} [(n : ) → MetricSpace (X n)] {f : (n : ) → X nX (n + 1)} (I : ∀ (n : ), Isometry (f n)) (x : (n : ) × X n) (y : (n : ) × X n) (m : ) (hx : x.fst m) (hy : y.fst m) :
                          Metric.inductiveLimitDist f x y = dist (Nat.leRecOn hx (fun {k : } => f k) x.snd) (Nat.leRecOn hy (fun {k : } => f k) y.snd)

                          The predistance on the disjoint union Σ n, X n can be computed in any X k for large enough k.

                          def Metric.inductivePremetric {X : Type u} [(n : ) → MetricSpace (X n)] {f : (n : ) → X nX (n + 1)} (I : ∀ (n : ), Isometry (f n)) :
                          PseudoMetricSpace ((n : ) × X n)

                          Premetric space structure on Σ n, X n.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Metric.InductiveLimit {X : Type u} [(n : ) → MetricSpace (X n)] {f : (n : ) → X nX (n + 1)} (I : ∀ (n : ), Isometry (f n)) :

                            The type giving the inductive limit in a metric space context.

                            Equations
                            Instances For
                              instance Metric.instMetricSpaceInductiveLimit {X : Type u} [(n : ) → MetricSpace (X n)] {f : (n : ) → X nX (n + 1)} {I : ∀ (n : ), Isometry (f n)} :
                              Equations
                              def Metric.toInductiveLimit {X : Type u} [(n : ) → MetricSpace (X n)] {f : (n : ) → X nX (n + 1)} (I : ∀ (n : ), Isometry (f n)) (n : ) (x : X n) :

                              Mapping each X n to the inductive limit.

                              Equations
                              Instances For
                                instance Metric.instInhabitedInductiveLimitOfOfNatNat {X : Type u} [(n : ) → MetricSpace (X n)] {f : (n : ) → X nX (n + 1)} (I : ∀ (n : ), Isometry (f n)) [Inhabited (X 0)] :
                                Equations
                                theorem Metric.toInductiveLimit_isometry {X : Type u} [(n : ) → MetricSpace (X n)] {f : (n : ) → X nX (n + 1)} (I : ∀ (n : ), Isometry (f n)) (n : ) :

                                The map toInductiveLimit n mapping X n to the inductive limit is an isometry.

                                theorem Metric.toInductiveLimit_commute {X : Type u} [(n : ) → MetricSpace (X n)] {f : (n : ) → X nX (n + 1)} (I : ∀ (n : ), Isometry (f n)) (n : ) :

                                The maps toInductiveLimit n are compatible with the maps f n.