topology.gluing

# Gluing Topological spaces #

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.
@[nolint]
structure Top.glue_data  :
Type (u_1+1)

A family of gluing data consists of

1. An index type J
2. An object U i for each i : J.
3. 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.)
4. An open embedding f i j : V i j ⟶ U i for each i j : ι.
5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
6. f i i is an isomorphism.
7. t i i is the identity.
8. 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).)
9. 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
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
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⟩
@[protected, instance]
@[nolint]
structure Top.glue_data.mk_core  :
Type (u+1)

A family of gluing data consists of

1. An index type J
2. A bundled topological space U i for each i : J.
3. An open set V i j ⊆ U i for each i j : J.
4. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
5. V i i = U i.
6. t i i is the identity.
7. For each x ∈ V i j ∩ V i k, t i j x ∈ V j k.
8. 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
theorem Top.glue_data.mk_core.t_inv (i j : h.J) (x : (h.V j i)) :
(h.t i j) ((h.t j i) x) = x
@[protected, instance]
noncomputable def Top.glue_data.mk_core.t' (i j k : h.J) :
(h.V i k).inclusion (h.V j i).inclusion

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

Equations
noncomputable def Top.glue_data.mk'  :

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
@[simp]
theorem Top.glue_data.of_open_subsets_to_glue_data_U {α : Type u} {J : Type u} (U : J → ) (ᾰ : {J := J, U := λ (i : J), (U i), V := λ (i j : J), .obj (U j), t := λ (i j : J), {to_fun := λ (x : ((topological_space.opens.to_Top (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) :
= (U ᾰ)
@[simp]
theorem Top.glue_data.of_open_subsets_to_glue_data_t {α : Type u} {J : Type u} (U : J → ) (i j : {J := J, U := λ (i : J), (U i), V := λ (i j : J), .obj (U j), t := λ (i j : J), {to_fun := λ (x : ((topological_space.opens.to_Top (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) :
noncomputable def Top.glue_data.of_open_subsets {α : Type u} {J : Type u} (U : J → ) :

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

Equations
@[simp]
theorem Top.glue_data.of_open_subsets_to_glue_data_J {α : Type u} {J : Type u} (U : J → ) :
@[simp]
theorem Top.glue_data.of_open_subsets_to_glue_data_V {α : Type u} {J : Type u} (U : J → ) (i : {J := J, U := λ (i : J), (U i), V := λ (i j : J), .obj (U j), t := λ (i j : J), {to_fun := λ (x : ((topological_space.opens.to_Top (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 × {J := J, U := λ (i : J), (U i), V := λ (i j : J), .obj (U j), t := λ (i j : J), {to_fun := λ (x : ((topological_space.opens.to_Top (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) :
@[simp]
theorem Top.glue_data.of_open_subsets_to_glue_data_f {α : Type u} {J : Type u} (U : J → ) (i j : {J := J, U := λ (i : J), (U i), V := λ (i j : J), .obj (U j), t := λ (i j : J), {to_fun := λ (x : ((topological_space.opens.to_Top (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) :
noncomputable def Top.glue_data.from_open_subsets_glue {α : Type u} {J : Type u} (U : J → ) :

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
@[simp]
theorem Top.glue_data.ι_from_open_subsets_glue_apply {α : Type u} {J : Type u} (U : J → ) (i : J) (x : ) :
= ((U i).inclusion) x
@[simp]
theorem Top.glue_data.ι_from_open_subsets_glue {α : Type u} {J : Type u} (U : J → ) (i : J) :
theorem Top.glue_data.from_open_subsets_glue_injective {α : Type u} {J : Type u} (U : J → ) :
theorem Top.glue_data.from_open_subsets_glue_is_open_map {α : Type u} {J : Type u} (U : J → ) :
theorem Top.glue_data.from_open_subsets_glue_open_embedding {α : Type u} {J : Type u} (U : J → ) :
theorem Top.glue_data.range_from_open_subsets_glue {α : Type u} {J : Type u} (U : J → ) :
= ⋃ (i : J), (U i)
noncomputable def Top.glue_data.open_cover_glue_homeo {α : Type u} {J : Type u} (U : J → ) (h : (⋃ (i : J), (U i)) = set.univ) :

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

Equations