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 eachi : ι
.Top.glue_data.rel
: A relation onΣ i, D.U i
defined by⟨i, x⟩ ~ ⟨j, y⟩
iff⟨i, x⟩ = ⟨j, y⟩
ort i j x = y
. SeeTop.glue_data.ι_eq_iff_rel
.Top.glue_data.mk
: A constructor ofglue_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 inglued
is open iff its preimage along eachι i
is open.Top.glue_data.ι_jointly_surjective
: Theι i
s 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 ofU i
andU j
inglued
isV i j
.Top.glue_data.preimage_range
: The preimage of the image ofU i
inU j
isV i j
.Top.glue_data.preimage_image_eq_preimage_f
: The preimage of the image of someU ⊆ U i
is given by the preimage alongf j i
.Top.glue_data.ι_open_embedding
: Each of theι i
s are open embeddings.
- 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 eachi : J
. - An object
V i j
for eachi j : J
. (Note that this isJ × J → Top
rather thanJ → J → Top
to connect to the limits library easier.) - An open embedding
f i j : V i j ⟶ U i
for eachi j : ι
. - A transition map
t i j : V i j ⟶ V j i
for eachi 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 throughV j k ×[U j] V j i ⟶ V j i
via somet' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i
. (This merely means thatV 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
An equivalence relation on Σ i, D.U i
that holds iff 𝖣 .ι i x = 𝖣 .ι j y
.
See Top.glue_data.ι_eq_iff_rel
.
- 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 eachi : J
. - An open set
V i j ⊆ U i
for eachi j : J
. - A transition map
t i j : V i j ⟶ V j i
for eachi 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
(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
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 := _}
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 := _}
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
The gluing of an open cover is homeomomorphic to the original space.