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 CategoryTheory.GlueData : 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.

• J : Type u_1
• U : self.J → TopCat
• V : self.J × self.J → TopCat
• f : (i j : self.J) → self.V (i, j) ⟶ self.U i
• f_mono : ∀ (i j : self.J), CategoryTheory.Mono (self.f i j)
• f_hasPullback : ∀ (i j k : self.J), CategoryTheory.Limits.HasPullback (self.f i j) (self.f i k)
• f_id : ∀ (i : self.J), CategoryTheory.IsIso (self.f i i)
• t : (i j : self.J) → self.V (i, j) ⟶ self.V (j, i)
• t_id : ∀ (i : self.J), self.t i i = CategoryTheory.CategoryStruct.id (self.V (i, i))
• t' : (i j k : self.J) → CategoryTheory.Limits.pullback (self.f i j) (self.f i k) ⟶ CategoryTheory.Limits.pullback (self.f j k) (self.f j i)
• t_fac : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.t' i j k) CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (self.t i j)
• cocycle : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.t' i j k) (CategoryTheory.CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.f i j) (self.f i k))
• f_open : ∀ (i j : self.J), OpenEmbedding ⇑(self.f i j)

theorem TopCat.GlueData.f_open (self : TopCat.GlueData) (i : self.J) (j : self.J) : OpenEmbedding ⇑(self.f i j)

theorem TopCat.GlueData.π_surjective (D : TopCat.GlueData) : Function.Surjective ⇑D.π

theorem TopCat.GlueData.isOpen_iff (D : TopCat.GlueData) (U : Set ↑D.glued) : IsOpen U ↔ ∀ (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)) : Prop

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)

theorem TopCat.GlueData.rel_equiv (D : TopCat.GlueData) : Equivalence D.Rel

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⟩

theorem TopCat.GlueData.ι_injective (D : TopCat.GlueData) (i : D.J) : Function.Injective ⇑(D.ι i)

instance TopCat.GlueData.ι_mono (D : TopCat.GlueData) (i : D.J) : CategoryTheory.Mono (D.ι i)

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)

theorem TopCat.GlueData.ι_openEmbedding (D : TopCat.GlueData) (i : D.J) : OpenEmbedding ⇑(D.ι i)

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.J → TopCat
• V : (i : self.J) → self.J → TopologicalSpace.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⟩)

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 (h : TopCat.GlueData.MkCore) (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 (h : TopCat.GlueData.MkCore) (i : h.J) (j : h.J) : CategoryTheory.IsIso (h.t i j)

Equations

• ⋯ = ⋯

def TopCat.GlueData.MkCore.t' (h : TopCat.GlueData.MkCore) (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.

def TopCat.GlueData.mk' (h : TopCat.GlueData.MkCore) : TopCat.GlueData

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.

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_J {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : (TopCat.GlueData.ofOpenSubsets U).J = J

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_t {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : (TopCat.GlueData.MkCore.mk (fun (i : J) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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.ofOpenSubsets U).t i j = { toFun := fun (x : ↑((TopologicalSpace.Opens.toTopCat ((TopologicalSpace.Opens.toTopCat (TopCat.of α)).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} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : (TopCat.GlueData.MkCore.mk (fun (i : J) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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.ofOpenSubsets U).f i j = ((TopologicalSpace.Opens.map (U i).inclusion).obj (U j)).inclusion

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_U {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : ∀ (a : (TopCat.GlueData.MkCore.mk (fun (i : J) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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.ofOpenSubsets U).U a = (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U a)

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_V {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : (TopCat.GlueData.MkCore.mk (fun (i : J) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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) => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).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.ofOpenSubsets U).V i = (TopologicalSpace.Opens.toTopCat ((TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i.1))).obj ((TopologicalSpace.Opens.map (U i.1).inclusion).obj (U i.2))

def TopCat.GlueData.ofOpenSubsets {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : TopCat.GlueData

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.

def TopCat.GlueData.fromOpenSubsetsGlue {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : (TopCat.GlueData.ofOpenSubsets U).glued ⟶ TopCat.of α

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.

theorem TopCat.GlueData.ι_fromOpenSubsetsGlue_apply {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : J) (x : (CategoryTheory.forget TopCat).obj ((TopCat.GlueData.ofOpenSubsets U).diagram.right i)) : (CategoryTheory.Limits.Multicoequalizer.desc (TopCat.GlueData.ofOpenSubsets U).diagram (TopCat.of α) (fun (x : (TopCat.GlueData.ofOpenSubsets U).diagram.R) => (U x).inclusion) ⋯) ((CategoryTheory.Limits.Multicoequalizer.π (TopCat.GlueData.ofOpenSubsets U).diagram i) x) = (U i).inclusion x

@[simp]

theorem TopCat.GlueData.ι_fromOpenSubsetsGlue {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : J) : CategoryTheory.CategoryStruct.comp ((TopCat.GlueData.ofOpenSubsets U).ι i) (TopCat.GlueData.fromOpenSubsetsGlue U) = (U i).inclusion

theorem TopCat.GlueData.fromOpenSubsetsGlue_injective {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : Function.Injective ⇑(TopCat.GlueData.fromOpenSubsetsGlue U)

theorem TopCat.GlueData.fromOpenSubsetsGlue_isOpenMap {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : IsOpenMap ⇑(TopCat.GlueData.fromOpenSubsetsGlue U)

theorem TopCat.GlueData.fromOpenSubsetsGlue_openEmbedding {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : OpenEmbedding ⇑(TopCat.GlueData.fromOpenSubsetsGlue U)

theorem TopCat.GlueData.range_fromOpenSubsetsGlue {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : Set.range ⇑(TopCat.GlueData.fromOpenSubsetsGlue U) = ⋃ (i : J), ↑(U i)

def TopCat.GlueData.openCoverGlueHomeo {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (h : ⋃ (i : J), ↑(U i) = Set.univ) : ↑(TopCat.GlueData.ofOpenSubsets U).glued ≃ₜ α

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

Equations

• TopCat.GlueData.openCoverGlueHomeo U h = Homeomorph.homeomorphOfContinuousOpen (Equiv.ofBijective ⇑(TopCat.GlueData.fromOpenSubsetsGlue U) ⋯) ⋯ ⋯