mathlib3 documentation

topology.metric_space.gluing

Metric space gluing #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 glue_space hΦ hΨ and two isometries to_glue_l hΦ hΨ and to_glue_r 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 2ε 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.

noncomputable def metric.glue_dist {X : Type u} {Y : Type v} {Z : Type w} [metric_space X] [metric_space Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) :

X ⊕ Y → X ⊕ Y → ℝ

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

Equations

metric.glue_dist Φ Ψ ε (sum.inr x) (sum.inr y) = has_dist.dist x y
metric.glue_dist Φ Ψ ε (sum.inr x) (sum.inl y) = (⨅ (p : Z), has_dist.dist y (Φ p) + has_dist.dist x (Ψ p)) + ε
metric.glue_dist Φ Ψ ε (sum.inl x) (sum.inr y) = (⨅ (p : Z), has_dist.dist x (Φ p) + has_dist.dist y (Ψ p)) + ε
metric.glue_dist Φ Ψ ε (sum.inl x) (sum.inl y) = has_dist.dist x y

theorem metric.glue_dist_glued_points {X : Type u} {Y : Type v} {Z : Type w} [metric_space X] [metric_space Y] [nonempty Z] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (p : Z) :

metric.glue_dist Φ Ψ ε (sum.inl (Φ p)) (sum.inr (Ψ p)) = ε

noncomputable def metric.glue_metric_approx {X : Type u} {Y : Type v} {Z : Type w} [metric_space X] [metric_space Y] [nonempty Z] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ) (ε0 : 0 < ε) (H : ∀ (p q : Z), |has_dist.dist (Φ p) (Φ q) - has_dist.dist (Ψ p) (Ψ q)| ≤ 2 * ε) :

metric_space (X ⊕ Y)

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

metric.glue_metric_approx Φ Ψ ε ε0 H = {to_pseudo_metric_space := {to_has_dist := {dist := metric.glue_dist Φ Ψ ε}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : X ⊕ Y), ↑⟨metric.glue_dist Φ Ψ ε x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (metric.glue_dist Φ Ψ ε) _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist (metric.glue_dist Φ Ψ ε) _ _ _, cobounded_sets := _}, eq_of_dist_eq_zero := _}

noncomputable def metric.sum.dist {X : Type u} {Y : Type v} [metric_space X] [metric_space Y] :

X ⊕ Y → X ⊕ 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

metric.sum.dist (sum.inr b) (sum.inr b') = has_dist.dist b b'
metric.sum.dist (sum.inr b) (sum.inl a) = has_dist.dist b _.some + 1 + has_dist.dist _.some a
metric.sum.dist (sum.inl a) (sum.inr b) = has_dist.dist a _.some + 1 + has_dist.dist _.some b
metric.sum.dist (sum.inl a) (sum.inl a') = has_dist.dist a a'

theorem metric.sum.dist_eq_glue_dist {X : Type u} {Y : Type v} [metric_space X] [metric_space Y] {p q : X ⊕ Y} (x : X) (y : Y) :

metric.sum.dist p q = metric.glue_dist (λ (_x : unit), _.some) (λ (_x : unit), _.some) 1 p q

theorem metric.sum.one_dist_le {X : Type u} {Y : Type v} [metric_space X] [metric_space Y] {x : X} {y : Y} :

1 ≤ metric.sum.dist (sum.inl x) (sum.inr y)

theorem metric.sum.one_dist_le' {X : Type u} {Y : Type v} [metric_space X] [metric_space Y] {x : X} {y : Y} :

1 ≤ metric.sum.dist (sum.inr y) (sum.inl x)

noncomputable def metric.metric_space_sum {X : Type u} {Y : Type v} [metric_space X] [metric_space Y] :

metric_space (X ⊕ 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

metric.metric_space_sum = {to_pseudo_metric_space := {to_has_dist := {dist := metric.sum.dist _inst_2}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : X ⊕ Y), ↑⟨metric.sum.dist x y, _⟩, edist_dist := _, to_uniform_space := sum.uniform_space pseudo_metric_space.to_uniform_space, uniformity_dist := _, to_bornology := bornology.of_dist metric.sum.dist metric.metric_space_sum._proof_6 sum.dist_comm metric.metric_space_sum._proof_7, cobounded_sets := _}, eq_of_dist_eq_zero := _}

theorem metric.sum.dist_eq {X : Type u} {Y : Type v} [metric_space X] [metric_space Y] {x y : X ⊕ Y} :

has_dist.dist x y = metric.sum.dist x y

theorem metric.isometry_inl {X : Type u} {Y : Type v} [metric_space X] [metric_space 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} [metric_space X] [metric_space Y] :

isometry sum.inr

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

@[protected]

noncomputable def metric.sigma.dist {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (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

metric.sigma.dist ⟨i, x⟩ ⟨j, y⟩ = dite (i = j) (λ (h : i = j), has_dist.dist x (cast _ y)) (λ (h : ¬i = j), has_dist.dist x _.some + 1 + has_dist.dist _.some y)

noncomputable def metric.sigma.has_dist {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] :

has_dist (Σ (i : ι), E i)

A has_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.has_dist = {dist := metric.sigma.dist (λ (i : ι), _inst_1 i)}

@[simp]

theorem metric.sigma.dist_same {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] (i : ι) (x y : E i) :

has_dist.dist ⟨i, x⟩ ⟨i, y⟩ = has_dist.dist x y

@[simp]

theorem metric.sigma.dist_ne {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] {i j : ι} (h : i ≠ j) (x : E i) (y : E j) :

has_dist.dist ⟨i, x⟩ ⟨j, y⟩ = has_dist.dist x _.some + 1 + has_dist.dist _.some y

theorem metric.sigma.one_le_dist_of_ne {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] {i j : ι} (h : i ≠ j) (x : E i) (y : E j) :

1 ≤ has_dist.dist ⟨i, x⟩ ⟨j, y⟩

theorem metric.sigma.fst_eq_of_dist_lt_one {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] (x y : Σ (i : ι), E i) (h : has_dist.dist x y < 1) :

@[protected]

theorem metric.sigma.dist_triangle {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] (x y z : Σ (i : ι), E i) :

has_dist.dist x z ≤ has_dist.dist x y + has_dist.dist y z

@[protected]

theorem metric.sigma.is_open_iff {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] (s : set (Σ (i : ι), E i)) :

is_open s ↔ ∀ (x : Σ (i : ι), E i), x ∈ s → (∃ (ε : ℝ) (H : ε > 0), ∀ (y : Σ (i : ι), E i), has_dist.dist x y < ε → y ∈ s)

@[protected]

noncomputable def metric.sigma.metric_space {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] :

metric_space (Σ (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

metric.sigma.metric_space = metric_space.of_dist_topology metric.sigma.dist metric.sigma.metric_space._proof_1 metric.sigma.metric_space._proof_2 metric.sigma.metric_space._proof_3 metric.sigma.metric_space._proof_4 metric.sigma.metric_space._proof_5

theorem metric.sigma.isometry_mk {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] (i : ι) :

isometry (sigma.mk i)

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

@[protected]

theorem metric.sigma.complete_space {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), metric_space (E i)] [∀ (i : ι), complete_space (E i)] :

complete_space (Σ (i : ι), E i)

A disjoint union of complete metric spaces is complete.

noncomputable def metric.glue_premetric {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) :

pseudo_metric_space (X ⊕ Y)

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

metric.glue_premetric hΦ hΨ = {to_has_dist := {dist := metric.glue_dist Φ Ψ 0}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : X ⊕ Y), ↑⟨metric.glue_dist Φ Ψ 0 x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (metric.glue_dist Φ Ψ 0) metric.glue_premetric._proof_6 metric.glue_premetric._proof_7 _, uniformity_dist := _, to_bornology := bornology.of_dist (metric.glue_dist Φ Ψ 0) metric.glue_premetric._proof_10 metric.glue_premetric._proof_11 _, cobounded_sets := _}

@[protected, instance]

noncomputable def metric.glue_space.metric_space {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) :

metric_space (metric.glue_space hΦ hΨ)

def metric.glue_space {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) :

Type (max u v)

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

Equations

metric.glue_space hΦ hΨ = uniform_space.separation_quotient (X ⊕ Y)

Instances for metric.glue_space

noncomputable def metric.to_glue_l {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) (x : X) :

metric.glue_space hΦ hΨ

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

Equations

metric.to_glue_l hΦ hΨ x = quotient.mk' (sum.inl x)

noncomputable def metric.to_glue_r {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) (y : Y) :

metric.glue_space hΦ hΨ

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

Equations

metric.to_glue_r hΦ hΨ y = quotient.mk' (sum.inr y)

@[protected, instance]

noncomputable def metric.inhabited_left {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited X] :

inhabited (metric.glue_space hΦ hΨ)

Equations

metric.inhabited_left hΦ hΨ = {default := metric.to_glue_l hΦ hΨ inhabited.default}

@[protected, instance]

noncomputable def metric.inhabited_right {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited Y] :

inhabited (metric.glue_space hΦ hΨ)

Equations

metric.inhabited_right hΦ hΨ = {default := metric.to_glue_r hΦ hΨ inhabited.default}

theorem metric.to_glue_commute {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) :

metric.to_glue_l hΦ hΨ ∘ Φ = metric.to_glue_r hΦ hΨ ∘ Ψ

theorem metric.to_glue_l_isometry {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) :

isometry (metric.to_glue_l hΦ hΨ)

theorem metric.to_glue_r_isometry {X : Type u} {Y : Type v} {Z : Type w} [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : isometry Φ) (hΨ : isometry Ψ) :

isometry (metric.to_glue_r hΦ hΨ)

def metric.inductive_limit_dist {X : ℕ → Type u} [Π (n : ℕ), metric_space (X n)] (f : Π (n : ℕ), X n → X (n + 1)) (x y : Σ (n : ℕ), X n) :

Predistance on the disjoint union Σ n, X n.

Equations

metric.inductive_limit_dist f x y = has_dist.dist (nat.le_rec_on _ f x.snd) (nat.le_rec_on _ f y.snd)

theorem metric.inductive_limit_dist_eq_dist {X : ℕ → Type u} [Π (n : ℕ), metric_space (X n)] {f : Π (n : ℕ), X n → X (n + 1)} (I : ∀ (n : ℕ), isometry (f n)) (x y : Σ (n : ℕ), X n) (m : ℕ) (hx : x.fst ≤ m) (hy : y.fst ≤ m) :

metric.inductive_limit_dist f x y = has_dist.dist (nat.le_rec_on hx f x.snd) (nat.le_rec_on hy f y.snd)

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

def metric.inductive_premetric {X : ℕ → Type u} [Π (n : ℕ), metric_space (X n)] {f : Π (n : ℕ), X n → X (n + 1)} (I : ∀ (n : ℕ), isometry (f n)) :

pseudo_metric_space (Σ (n : ℕ), X n)

Premetric space structure on Σ n, X n.

Equations

metric.inductive_premetric I = {to_has_dist := {dist := metric.inductive_limit_dist f}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : Σ (n : ℕ), X n), ↑⟨metric.inductive_limit_dist f x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (metric.inductive_limit_dist f) metric.inductive_premetric._proof_6 _ _, uniformity_dist := _, to_bornology := bornology.of_dist (metric.inductive_limit_dist f) metric.inductive_premetric._proof_10 _ _, cobounded_sets := _}

@[protected, instance]

def metric.inductive_limit.metric_space {X : ℕ → Type u} [Π (n : ℕ), metric_space (X n)] {f : Π (n : ℕ), X n → X (n + 1)} (I : ∀ (n : ℕ), isometry (f n)) :

metric_space (metric.inductive_limit I)

def metric.inductive_limit {X : ℕ → Type u} [Π (n : ℕ), metric_space (X n)] {f : Π (n : ℕ), X n → X (n + 1)} (I : ∀ (n : ℕ), isometry (f n)) :

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

Equations

metric.inductive_limit I = uniform_space.separation_quotient (Σ (n : ℕ), X n)

Instances for metric.inductive_limit

def metric.to_inductive_limit {X : ℕ → Type u} [Π (n : ℕ), metric_space (X n)] {f : Π (n : ℕ), X n → X (n + 1)} (I : ∀ (n : ℕ), isometry (f n)) (n : ℕ) (x : X n) :

metric.inductive_limit I

Mapping each X n to the inductive limit.

Equations

metric.to_inductive_limit I n x = quotient.mk' ⟨n, x⟩

@[protected, instance]

def metric.inductive_limit.inhabited {X : ℕ → Type u} [Π (n : ℕ), metric_space (X n)] {f : Π (n : ℕ), X n → X (n + 1)} (I : ∀ (n : ℕ), isometry (f n)) [inhabited (X 0)] :

inhabited (metric.inductive_limit I)

Equations

metric.inductive_limit.inhabited I = {default := metric.to_inductive_limit I 0 inhabited.default}

theorem metric.to_inductive_limit_isometry {X : ℕ → Type u} [Π (n : ℕ), metric_space (X n)] {f : Π (n : ℕ), X n → X (n + 1)} (I : ∀ (n : ℕ), isometry (f n)) (n : ℕ) :

isometry (metric.to_inductive_limit I n)

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

theorem metric.to_inductive_limit_commute {X : ℕ → Type u} [Π (n : ℕ), metric_space (X n)] {f : Π (n : ℕ), X n → X (n + 1)} (I : ∀ (n : ℕ), isometry (f n)) (n : ℕ) :

metric.to_inductive_limit I n.succ ∘ f n = metric.to_inductive_limit I n

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