mathlib documentation

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 #

Main results #

@[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 (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

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

Equations

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} [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) :
@[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) :
noncomputable def Top.glue_data.of_open_subsets {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) :

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

Equations
@[simp]
theorem Top.glue_data.of_open_subsets_to_glue_data_V {α : Type u} [topological_space α] {J : Type u} (U : J → topological_space.opens α) (i : {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 × {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) :
@[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) :

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
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) :

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

Equations