Gluing Topological spaces #

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

Given a family of gluing data (see category_theory/glue_data), we can then glue them together.

The construction should be "sealed" and considered as a black box, while only using the API provided.

Main definitions #

Top.glue_data: A structure containing the family of gluing data.
category_theory.glue_data.glued: The glued topological space. This is defined as the multicoequalizer of ∐ V i j ⇉ ∐ U i, so that the general colimit API can be used.
category_theory.glue_data.ι: The immersion ι i : U i ⟶ glued for each i : ι.
Top.glue_data.rel: A relation on Σ i, D.U i defined by ⟨i, x⟩ ~ ⟨j, y⟩ iff ⟨i, x⟩ = ⟨j, y⟩ or t i j x = y. See Top.glue_data.ι_eq_iff_rel.
Top.glue_data.mk: A constructor of glue_data whose conditions are stated in terms of elements rather than subobjects and pullbacks.
Top.glue_data.of_open_subsets: Given a family of open sets, we may glue them into a new topological space. This new space embeds into the original space, and is homeomorphic to it if the given family is an open cover (Top.glue_data.open_cover_glue_homeo).

Main results #

Top.glue_data.is_open_iff: A set in glued is open iff its preimage along each ι i is open.
Top.glue_data.ι_jointly_surjective: The ι is are jointly surjective.
Top.glue_data.rel_equiv: rel is an equivalence relation.
Top.glue_data.ι_eq_iff_rel: ι i x = ι j y ↔ ⟨i, x⟩ ~ ⟨j, y⟩.
Top.glue_data.image_inter: The intersection of the images of U i and U j in glued is V i j.
Top.glue_data.preimage_range: The preimage of the image of U i in U j is V i j.
Top.glue_data.preimage_image_eq_preimage_f: The preimage of the image of some U ⊆ U i is given by the preimage along f j i.
Top.glue_data.ι_open_embedding: Each of the ι is are open embeddings.

source

@[nolint]

structure Top.glue_data :

Type (u_1+1)

to_glue_data : category_theory.glue_data Top
f_open : ∀ (i j : self.to_glue_data.J), open_embedding ⇑(self.to_glue_data.f i j)

A family of gluing data consists of

An index type J
An object U i for each i : J.
An object V i j for each i j : J. (Note that this is J × J → Top rather than J → J → Top to connect to the limits library easier.)
An open embedding f i j : V i j ⟶ U i for each i j : ι.
A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
f i i is an isomorphism.
t i i is the identity.
V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i. (This merely means that V i j ∩ V i k ⊆ t i j ⁻¹' (V j i ∩ V j k).)
t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.

We can then glue the topological spaces U i together by identifying V i j with V j i, such that the U i's are open subspaces of the glued space.

Most of the times it would be easier to use the constructor Top.glue_data.mk' where the conditions are stated in a less categorical way.

Instances for Top.glue_data

Top.glue_data.has_sizeof_inst

source

theorem Top.glue_data.π_surjective (D : Top.glue_data) :

function.surjective ⇑(D.to_glue_data.π)

source

theorem Top.glue_data.is_open_iff (D : Top.glue_data) (U : set ↥(D.to_glue_data.glued)) :

is_open U ↔ ∀ (i : D.to_glue_data.J), is_open (⇑(D.to_glue_data.ι i) ⁻¹' U)

source

theorem Top.glue_data.ι_jointly_surjective (D : Top.glue_data) (x : ↥(D.to_glue_data.glued)) :

∃ (i : D.to_glue_data.J) (y : ↥(D.to_glue_data.U i)), ⇑(D.to_glue_data.ι i) y = x

source

def Top.glue_data.rel (D : Top.glue_data) (a b : Σ (i : D.to_glue_data.J), ↥(D.to_glue_data.U i)) :

Prop

An equivalence relation on Σ i, D.U i that holds iff 𝖣 .ι i x = 𝖣 .ι j y. See Top.glue_data.ι_eq_iff_rel.

Equations

D.rel a b = (a = b ∨ ∃ (x : ↥(D.to_glue_data.V (a.fst, b.fst))), ⇑(D.to_glue_data.f a.fst b.fst) x = a.snd ∧ ⇑(D.to_glue_data.f b.fst a.fst) (⇑(D.to_glue_data.t a.fst b.fst) x) = b.snd)

source

theorem Top.glue_data.rel_equiv (D : Top.glue_data) :

equivalence D.rel

source

theorem Top.glue_data.eqv_gen_of_π_eq (D : Top.glue_data) {x y : ↥∐ D.to_glue_data.U} (h : ⇑(D.to_glue_data.π) x = ⇑(D.to_glue_data.π) y) :

eqv_gen (category_theory.limits.types.coequalizer_rel ⇑(D.to_glue_data.diagram.fst_sigma_map) ⇑(D.to_glue_data.diagram.snd_sigma_map)) x y

source

theorem Top.glue_data.ι_eq_iff_rel (D : Top.glue_data) (i j : D.to_glue_data.J) (x : ↥(D.to_glue_data.U i)) (y : ↥(D.to_glue_data.U j)) :

⇑(D.to_glue_data.ι i) x = ⇑(D.to_glue_data.ι j) y ↔ D.rel ⟨i, x⟩ ⟨j, y⟩

source

theorem Top.glue_data.ι_injective (D : Top.glue_data) (i : D.to_glue_data.J) :

function.injective ⇑(D.to_glue_data.ι i)

source

@[protected, instance]

def Top.glue_data.ι_mono (D : Top.glue_data) (i : D.to_glue_data.J) :

category_theory.mono (D.to_glue_data.ι i)

source

theorem Top.glue_data.image_inter (D : Top.glue_data) (i j : D.to_glue_data.J) :

set.range ⇑(D.to_glue_data.ι i) ∩ set.range ⇑(D.to_glue_data.ι j) = set.range ⇑(D.to_glue_data.f i j ≫ D.to_glue_data.ι i)

source

theorem Top.glue_data.preimage_range (D : Top.glue_data) (i j : D.to_glue_data.J) :

⇑(D.to_glue_data.ι j) ⁻¹' set.range ⇑(D.to_glue_data.ι i) = set.range ⇑(D.to_glue_data.f j i)

source

theorem Top.glue_data.preimage_image_eq_image (D : Top.glue_data) (i j : D.to_glue_data.J) (U : set ↥(D.to_glue_data.U i)) :

⇑(D.to_glue_data.ι j) ⁻¹' (⇑(D.to_glue_data.ι i) '' U) = ⇑(D.to_glue_data.f j i) '' (⇑(D.to_glue_data.t j i ≫ D.to_glue_data.f i j) ⁻¹' U)

source

theorem Top.glue_data.preimage_image_eq_image' (D : Top.glue_data) (i j : D.to_glue_data.J) (U : set ↥(D.to_glue_data.U i)) :

⇑(D.to_glue_data.ι j) ⁻¹' (⇑(D.to_glue_data.ι i) '' U) = ⇑(D.to_glue_data.t i j ≫ D.to_glue_data.f j i) '' (⇑(D.to_glue_data.f i j) ⁻¹' U)

source

theorem Top.glue_data.open_image_open (D : Top.glue_data) (i : D.to_glue_data.J) (U : topological_space.opens ↥(D.to_glue_data.U i)) :

is_open (⇑(D.to_glue_data.ι i) '' ↑U)

source

theorem Top.glue_data.ι_open_embedding (D : Top.glue_data) (i : D.to_glue_data.J) :

open_embedding ⇑(D.to_glue_data.ι i)

source

@[nolint]

structure Top.glue_data.mk_core :

Type (u+1)

J : Type ?
U : self.J → Top
V : Π (i : self.J), self.J → topological_space.opens ↥(self.U i)
t : Π (i j : self.J), (topological_space.opens.to_Top (self.U i)).obj (self.V i j) ⟶ (topological_space.opens.to_Top (self.U j)).obj (self.V j i)
V_id : ∀ (i : self.J), self.V i i = ⊤
t_id : ∀ (i : self.J), ⇑(self.t i i) = id
t_inter : ∀ ⦃i j : self.J⦄ (k : self.J) (x : ↥(self.V i j)), ↑x ∈ self.V i k → ↑(⇑(self.t i j) x) ∈ self.V j k
cocycle : ∀ (i j k : self.J) (x : ↥(self.V i j)) (h : ↑x ∈ self.V i k), ↑(⇑(self.t j k) ⟨↑(⇑(self.t i j) x), _⟩) = ↑(⇑(self.t i k) ⟨↑x, h⟩)

A family of gluing data consists of

An index type J
A bundled topological space U i for each i : J.
An open set V i j ⊆ U i for each i j : J.
A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
V i i = U i.
t i i is the identity.
For each x ∈ V i j ∩ V i k, t i j x ∈ V j k.
t j k (t i j x) = t i k x.

We can then glue the topological spaces U i together by identifying V i j with V j i.

Instances for Top.glue_data.mk_core

Top.glue_data.mk_core.has_sizeof_inst

source

theorem Top.glue_data.mk_core.t_inv (h : Top.glue_data.mk_core) (i j : h.J) (x : ↥(h.V j i)) :

⇑(h.t i j) (⇑(h.t j i) x) = x

source

@[protected, instance]

def Top.glue_data.mk_core.t.category_theory.is_iso (h : Top.glue_data.mk_core) (i j : h.J) :

category_theory.is_iso (h.t i j)

source

noncomputable def Top.glue_data.mk_core.t' (h : Top.glue_data.mk_core) (i j k : h.J) :

category_theory.limits.pullback (h.V i j).inclusion (h.V i k).inclusion ⟶ category_theory.limits.pullback (h.V j k).inclusion (h.V j i).inclusion

(Implementation) the restricted transition map to be fed into glue_data.

Equations

h.t' i j k = (Top.pullback_iso_prod_subtype (h.V i j).inclusion (h.V i k).inclusion).hom ≫ {to_fun := λ (x : ↥(Top.of {p // ⇑((h.V i j).inclusion) p.fst = ⇑((h.V i k).inclusion) p.snd})), ⟨(⟨(⇑(h.t i j) x.val.fst).val, _⟩, ⇑(h.t i j) x.val.fst), _⟩, continuous_to_fun := _} ≫ (Top.pullback_iso_prod_subtype (h.V j k).inclusion (h.V j i).inclusion).inv

source

noncomputable def Top.glue_data.mk' (h : Top.glue_data.mk_core) :

Top.glue_data

This is a constructor of Top.glue_data whose arguments are in terms of elements and intersections rather than subobjects and pullbacks. Please refer to Top.glue_data.mk_core for details.

Equations

Top.glue_data.mk' h = {to_glue_data := {J := h.J, U := h.U, V := λ (i : h.J × h.J), (topological_space.opens.to_Top (h.U i.fst)).obj (h.V i.fst i.snd), f := λ (i j : h.J), (h.V i j).inclusion, f_mono := _, f_has_pullback := _, f_id := _, t := h.t, t_id := _, t' := h.t', t_fac := _, cocycle := _}, f_open := _}

source

@[simp]

theorem Top.glue_data.of_open_subsets_to_glue_data_U {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) (ᾰ : {J := J, U := λ (i : J), (topological_space.opens.to_Top (Top.of α)).obj (U i), V := λ (i j : J), (topological_space.opens.map (U i).inclusion).obj (U j), t := λ (i j : J), {to_fun := λ (x : ↥((topological_space.opens.to_Top ((topological_space.opens.to_Top (Top.of α)).obj (U i))).obj ((topological_space.opens.map (U i).inclusion).obj (U j)))), ⟨⟨x.val.val, _⟩, _⟩, continuous_to_fun := _}, V_id := _, t_id := _, t_inter := _, cocycle := _}.J) :

(Top.glue_data.of_open_subsets U).to_glue_data.U ᾰ = (topological_space.opens.to_Top (Top.of α)).obj (U ᾰ)

source

@[simp]

theorem Top.glue_data.of_open_subsets_to_glue_data_t {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) (i j : {J := J, U := λ (i : J), (topological_space.opens.to_Top (Top.of α)).obj (U i), V := λ (i j : J), (topological_space.opens.map (U i).inclusion).obj (U j), t := λ (i j : J), {to_fun := λ (x : ↥((topological_space.opens.to_Top ((topological_space.opens.to_Top (Top.of α)).obj (U i))).obj ((topological_space.opens.map (U i).inclusion).obj (U j)))), ⟨⟨x.val.val, _⟩, _⟩, continuous_to_fun := _}, V_id := _, t_id := _, t_inter := _, cocycle := _}.J) :

(Top.glue_data.of_open_subsets U).to_glue_data.t i j = {to_fun := λ (x : ↥((topological_space.opens.to_Top ((topological_space.opens.to_Top (Top.of α)).obj (U i))).obj ((topological_space.opens.map (U i).inclusion).obj (U j)))), ⟨⟨↑↑x, _⟩, _⟩, continuous_to_fun := _}

source

noncomputable def Top.glue_data.of_open_subsets {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) :

Top.glue_data

We may construct a glue data from a family of open sets.

Equations

Top.glue_data.of_open_subsets U = Top.glue_data.mk' {J := J, U := λ (i : J), (topological_space.opens.to_Top (Top.of α)).obj (U i), V := λ (i j : J), (topological_space.opens.map (U i).inclusion).obj (U j), t := λ (i j : J), {to_fun := λ (x : ↥((topological_space.opens.to_Top ((topological_space.opens.to_Top (Top.of α)).obj (U i))).obj ((topological_space.opens.map (U i).inclusion).obj (U j)))), ⟨⟨x.val.val, _⟩, _⟩, continuous_to_fun := _}, V_id := _, t_id := _, t_inter := _, cocycle := _}

source

@[simp]

theorem Top.glue_data.of_open_subsets_to_glue_data_J {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) :

(Top.glue_data.of_open_subsets U).to_glue_data.J = J

source

@[simp]

(Top.glue_data.of_open_subsets U).to_glue_data.V i = (topological_space.opens.to_Top ((topological_space.opens.to_Top (Top.of α)).obj (U i.fst))).obj ((topological_space.opens.map (U i.fst).inclusion).obj (U i.snd))

source

@[simp]

theorem Top.glue_data.of_open_subsets_to_glue_data_f {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) (i j : {J := J, U := λ (i : J), (topological_space.opens.to_Top (Top.of α)).obj (U i), V := λ (i j : J), (topological_space.opens.map (U i).inclusion).obj (U j), t := λ (i j : J), {to_fun := λ (x : ↥((topological_space.opens.to_Top ((topological_space.opens.to_Top (Top.of α)).obj (U i))).obj ((topological_space.opens.map (U i).inclusion).obj (U j)))), ⟨⟨x.val.val, _⟩, _⟩, continuous_to_fun := _}, V_id := _, t_id := _, t_inter := _, cocycle := _}.J) :

(Top.glue_data.of_open_subsets U).to_glue_data.f i j = ((topological_space.opens.map (U i).inclusion).obj (U j)).inclusion

source

noncomputable def Top.glue_data.from_open_subsets_glue {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) :

(Top.glue_data.of_open_subsets U).to_glue_data.glued ⟶ Top.of α

The canonical map from the glue of a family of open subsets α into α. This map is an open embedding (from_open_subsets_glue_open_embedding), and its range is ⋃ i, (U i : set α) (range_from_open_subsets_glue).

Equations

Top.glue_data.from_open_subsets_glue U = category_theory.limits.multicoequalizer.desc (Top.glue_data.of_open_subsets U).to_glue_data.diagram (Top.of α) (λ (x : (Top.glue_data.of_open_subsets U).to_glue_data.diagram.R), (U x).inclusion) _

source

@[simp]

theorem Top.glue_data.ι_from_open_subsets_glue_apply {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) (i : J) (x : ↥((Top.glue_data.of_open_subsets U).to_glue_data.U i)) :

⇑(Top.glue_data.from_open_subsets_glue U) (⇑((Top.glue_data.of_open_subsets U).to_glue_data.ι i) x) = ⇑((U i).inclusion) x

source

@[simp]

theorem Top.glue_data.ι_from_open_subsets_glue {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) (i : J) :

(Top.glue_data.of_open_subsets U).to_glue_data.ι i ≫ Top.glue_data.from_open_subsets_glue U = (U i).inclusion

source

theorem Top.glue_data.from_open_subsets_glue_injective {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) :

function.injective ⇑(Top.glue_data.from_open_subsets_glue U)

source

theorem Top.glue_data.from_open_subsets_glue_is_open_map {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) :

is_open_map ⇑(Top.glue_data.from_open_subsets_glue U)

source

theorem Top.glue_data.from_open_subsets_glue_open_embedding {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) :

open_embedding ⇑(Top.glue_data.from_open_subsets_glue U)

source

theorem Top.glue_data.range_from_open_subsets_glue {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) :

set.range ⇑(Top.glue_data.from_open_subsets_glue U) = ⋃ (i : J), ↑(U i)

source

noncomputable def Top.glue_data.open_cover_glue_homeo {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) (h : (⋃ (i : J), ↑(U i)) = set.univ) :

↥((Top.glue_data.of_open_subsets U).to_glue_data.glued) ≃ₜ α

The gluing of an open cover is homeomomorphic to the original space.

Equations

Top.glue_data.open_cover_glue_homeo U h = homeomorph.homeomorph_of_continuous_open (equiv.of_bijective ⇑(Top.glue_data.from_open_subsets_glue U) _) _ _