# mathlibdocumentation

topology.metric_space.gluing

# Metric space gluing

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

     Φ
γ ---> α
|
|Ψ
v
β


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 α ⊕ β, 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 α ⊕ β, without the need to take a quotient. In particular, when α and β are inhabited, this gives a natural metric space structure on α ⊕ β, where the basepoints are at distance 1, say, and the distances between other points are obtained by going through the two basepoints.

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.glue_dist {α : Type u} {β : Type v} {γ : Type w} [metric_space α] [metric_space β] :
(γ → α)(γ → β)α βα β

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

Equations
theorem metric.glue_dist_glued_points {α : Type u} {β : Type v} {γ : Type w} [metric_space α] [metric_space β] [nonempty γ] (Φ : γ → α) (Ψ : γ → β) (ε : ) (p : γ) :
ε (sum.inl (Φ p)) (sum.inr (Ψ p)) = ε

def metric.glue_metric_approx {α : Type u} {β : Type v} {γ : Type w} [metric_space α] [metric_space β] [nonempty γ] (Φ : γ → α) (Ψ : γ → β) (ε : ) :
0 < ε(∀ (p q : γ), abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) 2 * ε)metric_space β)

Given two maps Φ and Ψ intro metric spaces α and β 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 α and β along the images of Φ and Ψ, so that Φ p and Ψ p are at distance ε.

Equations
def metric.sum.dist {α : Type u} {β : Type v} [metric_space α] [metric_space β] [inhabited α] [inhabited β] :
α βα β

Equations
theorem metric.sum.dist_eq_glue_dist {α : Type u} {β : Type v} [metric_space α] [metric_space β] [inhabited α] [inhabited β] {p q : α β} :
= metric.glue_dist (λ (_x : unit), default α) (λ (_x : unit), default β) 1 p q

theorem metric.sum.one_dist_le {α : Type u} {β : Type v} [metric_space α] [metric_space β] [inhabited α] [inhabited β] {x : α} {y : β} :
1 (sum.inr y)

theorem metric.sum.one_dist_le' {α : Type u} {β : Type v} [metric_space α] [metric_space β] [inhabited α] [inhabited β] {x : α} {y : β} :
1 (sum.inl x)

def metric.metric_space_sum {α : Type u} {β : Type v} [metric_space α] [metric_space β] [inhabited α] [inhabited β] :

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
theorem metric.sum.dist_eq {α : Type u} {β : Type v} [metric_space α] [metric_space β] [inhabited α] [inhabited β] {x y : α β} :
dist x y =

theorem metric.isometry_on_inl {α : Type u} {β : Type v} [metric_space α] [metric_space β] [inhabited α] [inhabited β] :

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

theorem metric.isometry_on_inr {α : Type u} {β : Type v} [metric_space α] [metric_space β] [inhabited α] [inhabited β] :

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

def metric.glue_premetric {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} :
premetric_space β)

Equations
def metric.glue_space {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} :
Type (max u v)

Equations
@[instance]
def metric.metric_space_glue_space {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} (hΦ : isometry Φ) (hΨ : isometry Ψ) :

Equations
def metric.to_glue_l {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} (hΦ : isometry Φ) (hΨ : isometry Ψ) :
α →

Equations
def metric.to_glue_r {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} (hΦ : isometry Φ) (hΨ : isometry Ψ) :
β →

Equations
@[instance]
def metric.inhabited_left {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited α] :

Equations
@[instance]
def metric.inhabited_right {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited β] :

Equations
theorem metric.to_glue_commute {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} (hΦ : isometry Φ) (hΨ : isometry Ψ) :
Φ = Ψ

theorem metric.to_glue_l_isometry {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} (hΦ : isometry Φ) (hΨ : isometry Ψ) :

theorem metric.to_glue_r_isometry {α : Type u} {β : Type v} {γ : Type w} [nonempty γ] [metric_space γ] [metric_space α] [metric_space β] {Φ : γ → α} {Ψ : γ → β} (hΦ : isometry Φ) (hΨ : isometry Ψ) :

def metric.inductive_limit_dist {X : Type u} [Π (n : ), metric_space (X n)] :
(Π (n : ), X nX (n + 1))(Σ (n : ), X n)(Σ (n : ), X n)

Predistance on the disjoint union Σn, X n.

Equations
theorem metric.inductive_limit_dist_eq_dist {X : Type u} [Π (n : ), metric_space (X n)] {f : Π (n : ), X nX (n + 1)} (I : ∀ (n : ), isometry (f n)) (x y : Σ (n : ), X n) (m : ) (hx : x.fst m) (hy : y.fst m) :
= dist f x.snd) 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 nX (n + 1)} :
(∀ (n : ), isometry (f n))premetric_space (Σ (n : ), X n)

Premetric space structure on Σn, X n.

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

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

Equations
@[instance]
def metric.metric_space_inductive_limit {X : Type u} [Π (n : ), metric_space (X n)] {f : Π (n : ), X nX (n + 1)} (I : ∀ (n : ), isometry (f n)) :

Metric space structure on the inductive limit.

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

Mapping each X n to the inductive limit.

Equations
@[instance]
def metric.inhabited {X : Type u} [Π (n : ), metric_space (X n)] {f : Π (n : ), X nX (n + 1)} (I : ∀ (n : ), isometry (f n)) [inhabited (X 0)] :

Equations
theorem metric.to_inductive_limit_isometry {X : Type u} [Π (n : ), metric_space (X n)] {f : Π (n : ), X nX (n + 1)} (I : ∀ (n : ), isometry (f n)) (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 nX (n + 1)} (I : ∀ (n : ), isometry (f n)) (n : ) :
f n =

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