# 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 results #

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 × JTopCat rather than JJTopCat 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.f_open (self : TopCat.GlueData) (i : self.J) (j : self.J) :
OpenEmbedding (self.f i j)
theorem TopCat.GlueData.isOpen_iff (D : TopCat.GlueData) (U : Set D.glued) :
∀ (i : D.J), IsOpen ((D i) ⁻¹' U)
theorem TopCat.GlueData.ι_jointly_surjective (D : TopCat.GlueData) (x : D.glued) :
∃ (i : D.J) (y : (D.U i)), (D i) y = x
def TopCat.GlueData.Rel (D : TopCat.GlueData) (a : (i : D.J) × (D.U i)) (b : (i : D.J) × (D.U i)) :

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

Equations
• D.Rel a b = (a = b ∃ (x : (D.V (a.fst, b.fst))), (D.f a.fst b.fst) x = a.snd (D.f b.fst a.fst) ((D.t a.fst b.fst) x) = b.snd)
Instances For
theorem TopCat.GlueData.eqvGen_of_π_eq (D : TopCat.GlueData) {x : ( D.U)} {y : ( D.U)} (h : D x = D y) :
EqvGen (CategoryTheory.Limits.Types.CoequalizerRel D.diagram.fstSigmaMap D.diagram.sndSigmaMap) x y
theorem TopCat.GlueData.ι_eq_iff_rel (D : TopCat.GlueData) (i : D.J) (j : D.J) (x : (D.U i)) (y : (D.U j)) :
(D i) x = (D j) y D.Rel i, x j, y
Equations
• =
theorem TopCat.GlueData.image_inter (D : TopCat.GlueData) (i : D.J) (j : D.J) :
Set.range (D i) Set.range (D j) = Set.range (CategoryTheory.CategoryStruct.comp (D.f i j) (D i))
theorem TopCat.GlueData.preimage_range (D : TopCat.GlueData) (i : D.J) (j : D.J) :
(D j) ⁻¹' Set.range (D i) = Set.range (D.f j i)
theorem TopCat.GlueData.preimage_image_eq_image (D : TopCat.GlueData) (i : D.J) (j : D.J) (U : Set (D.U i)) :
(D j) ⁻¹' ((D i) '' U) = (D.f j i) '' ((CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j)) ⁻¹' U)
theorem TopCat.GlueData.preimage_image_eq_image' (D : TopCat.GlueData) (i : D.J) (j : D.J) (U : Set (D.U i)) :
(D j) ⁻¹' ((D i) '' U) = (CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i)) '' ((D.f i j) ⁻¹' U)
theorem TopCat.GlueData.open_image_open (D : TopCat.GlueData) (i : D.J) (U : TopologicalSpace.Opens (D.U i)) :
IsOpen ((D i) '' U)
structure TopCat.GlueData.MkCore :
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.

• J : Type u
• U : self.JTopCat
• V : (i : self.J) → self.JTopologicalSpace.Opens (self.U i)
• t : (i j : self.J) → (TopologicalSpace.Opens.toTopCat (self.U i)).obj (self.V i j) (TopologicalSpace.Opens.toTopCat (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)
Instances For
theorem TopCat.GlueData.MkCore.V_id (self : TopCat.GlueData.MkCore) (i : self.J) :
self.V i i =
theorem TopCat.GlueData.MkCore.t_id (self : TopCat.GlueData.MkCore) (i : self.J) :
(self.t i i) = id
theorem TopCat.GlueData.MkCore.t_inter (self : TopCat.GlueData.MkCore) ⦃i : self.J ⦃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
theorem TopCat.GlueData.MkCore.cocycle (self : TopCat.GlueData.MkCore) (i : self.J) (j : self.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)
theorem TopCat.GlueData.MkCore.t_inv (i : h.J) (j : h.J) (x : (h.V j i)) :
(h.t i j) ((h.t j i) x) = x
instance TopCat.GlueData.instIsIsoT (i : h.J) (j : h.J) :
Equations
• =
def TopCat.GlueData.MkCore.t' (i : h.J) (j : h.J) (k : h.J) :
CategoryTheory.Limits.pullback (h.V i j).inclusion (h.V i k).inclusion CategoryTheory.Limits.pullback (h.V j k).inclusion (h.V j i).inclusion

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

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_J {α : Type u} [] {J : Type u} (U : ) :
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_t {α : Type u} [] {J : Type u} (U : ) (i : (TopCat.GlueData.MkCore.mk (fun (i : J) => .obj (U i)) (fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun (i j : J) => { toFun := fun (x : ((TopologicalSpace.Opens.toTopCat ((fun (i : J) => .obj (U i)) i)).obj ((fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) i j))) => x, , , continuous_toFun := }) ).J) (j : (TopCat.GlueData.MkCore.mk (fun (i : J) => .obj (U i)) (fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun (i j : J) => { toFun := fun (x : ((TopologicalSpace.Opens.toTopCat ((fun (i : J) => .obj (U i)) i)).obj ((fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) i j))) => x, , , continuous_toFun := }) ).J) :
i j = { toFun := fun (x : ((TopologicalSpace.Opens.toTopCat (.obj (U i))).obj ((TopologicalSpace.Opens.map (U i).inclusion).obj (U j)))) => x, , , continuous_toFun := }
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_f {α : Type u} [] {J : Type u} (U : ) (i : (TopCat.GlueData.MkCore.mk (fun (i : J) => .obj (U i)) (fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun (i j : J) => { toFun := fun (x : ((TopologicalSpace.Opens.toTopCat ((fun (i : J) => .obj (U i)) i)).obj ((fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) i j))) => x, , , continuous_toFun := }) ).J) (j : (TopCat.GlueData.MkCore.mk (fun (i : J) => .obj (U i)) (fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun (i j : J) => { toFun := fun (x : ((TopologicalSpace.Opens.toTopCat ((fun (i : J) => .obj (U i)) i)).obj ((fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) i j))) => x, , , continuous_toFun := }) ).J) :
i j = ((TopologicalSpace.Opens.map (U i).inclusion).obj (U j)).inclusion
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_U {α : Type u} [] {J : Type u} (U : ) :
∀ (a : (TopCat.GlueData.MkCore.mk (fun (i : J) => .obj (U i)) (fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun (i j : J) => { toFun := fun (x : ((TopologicalSpace.Opens.toTopCat ((fun (i : J) => .obj (U i)) i)).obj ((fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) i j))) => x, , , continuous_toFun := }) ).J), = .obj (U a)
@[simp]
theorem TopCat.GlueData.ofOpenSubsets_toGlueData_V {α : Type u} [] {J : Type u} (U : ) (i : (TopCat.GlueData.MkCore.mk (fun (i : J) => .obj (U i)) (fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun (i j : J) => { toFun := fun (x : ((TopologicalSpace.Opens.toTopCat ((fun (i : J) => .obj (U i)) i)).obj ((fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) i j))) => x, , , continuous_toFun := }) ).J × (TopCat.GlueData.MkCore.mk (fun (i : J) => .obj (U i)) (fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) (fun (i j : J) => { toFun := fun (x : ((TopologicalSpace.Opens.toTopCat ((fun (i : J) => .obj (U i)) i)).obj ((fun (i j : J) => (TopologicalSpace.Opens.map (U i).inclusion).obj (U j)) i j))) => x, , , continuous_toFun := }) ).J) :
= (TopologicalSpace.Opens.toTopCat (.obj (U i.1))).obj ((TopologicalSpace.Opens.map (U i.1).inclusion).obj (U i.2))
def TopCat.GlueData.ofOpenSubsets {α : Type u} [] {J : Type u} (U : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.GlueData.fromOpenSubsetsGlue {α : Type u} [] {J : Type u} (U : ) :
.glued

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TopCat.GlueData.ι_fromOpenSubsetsGlue_apply {α : Type u} [] {J : Type u} (U : ) (i : J) (x : .obj (.diagram.right i)) :
(CategoryTheory.Limits.Multicoequalizer.desc .diagram () (fun (x : .diagram.R) => (U x).inclusion) ) ( x) = (U i).inclusion x
@[simp]
theorem TopCat.GlueData.ι_fromOpenSubsetsGlue {α : Type u} [] {J : Type u} (U : ) (i : J) :
= (U i).inclusion
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) :
.glued ≃ₜ α

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

Equations
Instances For