Documentation

Mathlib.Topology.Gluing

Gluing Topological spaces #

Given a family of gluing data (see Mathlib/CategoryTheory/GlueData.lean), 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 #

• TopCat.GlueData: A structure containing the family of gluing data.
• CategoryTheory.GlueData.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.
• CategoryTheory.GlueData.ι: The immersion ι i : U i ⟶ glued for each i : ι.
• TopCat.GlueData.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 TopCat.GlueData.ι_eq_iff_rel.
• TopCat.GlueData.mk: A constructor of GlueData whose conditions are stated in terms of elements rather than subobjects and pullbacks.
• TopCat.GlueData.ofOpenSubsets: 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 (TopCat.GlueData.openCoverGlueHomeo).

Main results #

• TopCat.GlueData.isOpen_iff: A set in glued is open iff its preimage along each ι i is open.
• TopCat.GlueData.ι_jointly_surjective: The ι is are jointly surjective.
• TopCat.GlueData.rel_equiv: Rel is an equivalence relation.
• TopCat.GlueData.ι_eq_iff_rel: ι i x = ι j y ↔ ⟨i, x⟩ ~ ⟨j, y⟩.
• TopCat.GlueData.image_inter: The intersection of the images of U i and U j in glued is V i j.
• TopCat.GlueData.preimage_range: The preimage of the image of U i in U j is V i j.
• TopCat.GlueData.preimage_image_eq_image: The preimage of the image of some U ⊆ U i is given by XXX.
• TopCat.GlueData.ι_openEmbedding: Each of the ι is are open embeddings.
structure TopCat.GlueDataextends :
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 → TopCat rather than J → J → TopCat 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 TopCat.GlueData.mk' where the conditions are stated in a less categorical way.

Instances For
theorem TopCat.GlueData.isOpen_iff (D : TopCat.GlueData) (U : Set ↑(CategoryTheory.GlueData.glued D.toGlueData)) :
∀ (i : D.J), IsOpen (↑(CategoryTheory.GlueData.ι D.toGlueData i) ⁻¹' U)
theorem TopCat.GlueData.ι_jointly_surjective (D : TopCat.GlueData) (x : ↑(CategoryTheory.GlueData.glued D.toGlueData)) :
i y, ↑(CategoryTheory.GlueData.ι D.toGlueData i) y = x
def TopCat.GlueData.Rel (D : TopCat.GlueData) (a : (i : D.J) × ↑(CategoryTheory.GlueData.U D.toGlueData i)) (b : (i : D.J) × ↑(CategoryTheory.GlueData.U D.toGlueData i)) :

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

Instances For
theorem TopCat.GlueData.eqvGen_of_π_eq (D : TopCat.GlueData) {x : ↑( D.U)} {y : ↑( D.U)} (h : ↑(CategoryTheory.GlueData.π D.toGlueData) x = ↑(CategoryTheory.GlueData.π D.toGlueData) y) :
EqvGen () x y
theorem TopCat.GlueData.ι_eq_iff_rel (D : TopCat.GlueData) (i : D.J) (j : D.J) (x : ↑(CategoryTheory.GlueData.U D.toGlueData i)) (y : ↑(CategoryTheory.GlueData.U D.toGlueData j)) :
↑(CategoryTheory.GlueData.ι D.toGlueData i) x = ↑(CategoryTheory.GlueData.ι D.toGlueData j) y TopCat.GlueData.Rel D { fst := i, snd := x } { fst := j, snd := y }
theorem TopCat.GlueData.preimage_range (D : TopCat.GlueData) (i : D.J) (j : D.J) :
↑(CategoryTheory.GlueData.ι D.toGlueData j) ⁻¹' Set.range ↑(CategoryTheory.GlueData.ι D.toGlueData i) = Set.range ↑(CategoryTheory.GlueData.f D.toGlueData j i)
theorem TopCat.GlueData.preimage_image_eq_image (D : TopCat.GlueData) (i : D.J) (j : D.J) (U : Set ↑(CategoryTheory.GlueData.U D.toGlueData i)) :
↑(CategoryTheory.GlueData.ι D.toGlueData j) ⁻¹' (↑(CategoryTheory.GlueData.ι D.toGlueData i) '' U) = ↑(CategoryTheory.GlueData.f D.toGlueData j i) '' (↑(CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData j i) (CategoryTheory.GlueData.f D.toGlueData i j)) ⁻¹' U)
theorem TopCat.GlueData.preimage_image_eq_image' (D : TopCat.GlueData) (i : D.J) (j : D.J) (U : Set ↑(CategoryTheory.GlueData.U D.toGlueData i)) :
↑(CategoryTheory.GlueData.ι D.toGlueData j) ⁻¹' (↑(CategoryTheory.GlueData.ι D.toGlueData i) '' U) = ↑(CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t D.toGlueData i j) (CategoryTheory.GlueData.f D.toGlueData j i)) '' (↑(CategoryTheory.GlueData.f D.toGlueData i j) ⁻¹' U)
structure TopCat.GlueData.MkCore :
Type (u + 1)
• J : Type u
• U : s.JTopCat
• V : (i : s.J) → s.J
• t : (i j : s.J) → ().obj () ().obj ()
• V_id : ∀ (i : s.J),
• t_id : ∀ (i : s.J), ↑() = id
• t_inter : ∀ ⦃i j : s.J⦄ (k : s.J) (x : { x // x }), x ↑(↑() x)
• cocycle : ∀ (i j k : s.J) (x : { x // x }) (h : x ), ↑(↑() { val := ↑(↑() x), property := (_ : ↑(↑() x) ) }) = ↑(↑() { val := x, property := h })

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
theorem TopCat.GlueData.MkCore.t_inv (i : h.J) (j : h.J) (x : { x // x }) :
↑() (↑() x) = x
def TopCat.GlueData.MkCore.t' (i : h.J) (j : h.J) (k : h.J) :

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

Instances For

This is a constructor of TopCat.GlueData whose arguments are in terms of elements and intersections rather than subobjects and pullbacks. Please refer to TopCat.GlueData.MkCore for details.

Instances For
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_U {α : Type u} [] {J : Type u} (U : ) :
∀ (a : (TopCat.GlueData.MkCore.mk (fun i => ().obj (U i)) (fun i j => ().obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) (_ : ∀ (i : J), (fun i j => ().obj (U j)) i i = ) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }), x (fun i j => ().obj (U j)) i kx (fun i j => ().obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }) (h : x (fun i j => ().obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }))).J), CategoryTheory.GlueData.U ().toGlueData a = ().obj (U a)
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_t {α : Type u} [] {J : Type u} (U : ) (i : (TopCat.GlueData.MkCore.mk (fun i => ().obj (U i)) (fun i j => ().obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) (_ : ∀ (i : J), (fun i j => ().obj (U j)) i i = ) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }), x (fun i j => ().obj (U j)) i kx (fun i j => ().obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }) (h : x (fun i j => ().obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }))).J) (j : (TopCat.GlueData.MkCore.mk (fun i => ().obj (U i)) (fun i j => ().obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) (_ : ∀ (i : J), (fun i j => ().obj (U j)) i i = ) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }), x (fun i j => ().obj (U j)) i kx (fun i j => ().obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }) (h : x (fun i j => ().obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }))).J) :
CategoryTheory.GlueData.t ().toGlueData i j = ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_f {α : Type u} [] {J : Type u} (U : ) (i : (TopCat.GlueData.MkCore.mk (fun i => ().obj (U i)) (fun i j => ().obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) (_ : ∀ (i : J), (fun i j => ().obj (U j)) i i = ) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }), x (fun i j => ().obj (U j)) i kx (fun i j => ().obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }) (h : x (fun i j => ().obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }))).J) (j : (TopCat.GlueData.MkCore.mk (fun i => ().obj (U i)) (fun i j => ().obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) (_ : ∀ (i : J), (fun i j => ().obj (U j)) i i = ) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }), x (fun i j => ().obj (U j)) i kx (fun i j => ().obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }) (h : x (fun i j => ().obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }))).J) :
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_J {α : Type u} [] {J : Type u} (U : ) :
().toGlueData.J = J
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_V {α : Type u} [] {J : Type u} (U : ) (i : (TopCat.GlueData.MkCore.mk (fun i => ().obj (U i)) (fun i j => ().obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) (_ : ∀ (i : J), (fun i j => ().obj (U j)) i i = ) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }), x (fun i j => ().obj (U j)) i kx (fun i j => ().obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }) (h : x (fun i j => ().obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }))).J × (TopCat.GlueData.MkCore.mk (fun i => ().obj (U i)) (fun i j => ().obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) (_ : ∀ (i : J), (fun i j => ().obj (U j)) i i = ) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }), x (fun i j => ().obj (U j)) i kx (fun i j => ().obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x (fun i j => ().obj (U j)) i j }) (h : x (fun i j => ().obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) j k) { val := ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := x, property := (_ : x (fun i j => ().obj (U j)) i j) }, property := (_ : x U i) }) i j) x), property := (_ : x (fun i j => ().obj (U j)) i k) }))).J) :
CategoryTheory.GlueData.V ().toGlueData i = (TopologicalSpace.Opens.toTopCat (().obj (U i.fst))).obj (().obj (U i.snd))
def TopCat.GlueData.ofOpenSubsets {α : Type u} [] {J : Type u} (U : ) :

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

Instances For
def TopCat.GlueData.fromOpenSubsetsGlue {α : Type u} [] {J : Type u} (U : ) :

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

Instances For
theorem TopCat.GlueData.ι_fromOpenSubsetsGlue_apply {α : Type u} [] {J : Type u} (U : ) (i : J) (x : ().obj ()) :
↑(CategoryTheory.Limits.Multicoequalizer.desc (CategoryTheory.GlueData.diagram ().toGlueData) () (fun x => ) (_ : ∀ (a : (CategoryTheory.GlueData.diagram ().toGlueData).L), CategoryTheory.CategoryStruct.comp () ((fun x => ) ()) = CategoryTheory.CategoryStruct.comp () ((fun x => ) ()))) (↑() x) = ↑() x
@[simp]
theorem TopCat.GlueData.ι_fromOpenSubsetsGlue {α : Type u} [] {J : Type u} (U : ) (i : J) :
theorem TopCat.GlueData.range_fromOpenSubsetsGlue {α : Type u} [] {J : Type u} (U : ) :
= ⋃ (i : J), ↑(U i)
def TopCat.GlueData.openCoverGlueHomeo {α : Type u} [] {J : Type u} (U : ) (h : ⋃ (i : J), ↑(U i) = Set.univ) :

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

Instances For