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.ι_isOpenEmbedding: Each of the ι is are open embeddings.

structure TopCat.GlueDataextends CategoryTheory.GlueData TopCat : 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) : Mono (self.f i j)
• f_hasPullback (i j k : self.J) : Limits.HasPullback (self.f i j) (self.f i k)
• f_id (i : self.J) : 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 = CategoryStruct.id (self.V (i, i))
• t' (i j k : self.J) : Limits.pullback (self.f i j) (self.f i k) ⟶ Limits.pullback (self.f j k) (self.f j i)
• t_fac (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (Limits.pullback.snd (self.f j k) (self.f j i)) = CategoryStruct.comp (Limits.pullback.fst (self.f i j) (self.f i k)) (self.t i j)
• cocycle (i j k : self.J) : CategoryStruct.comp (self.t' i j k) (CategoryStruct.comp (self.t' j k i) (self.t' k i j)) = CategoryStruct.id (Limits.pullback (self.f i j) (self.f i k))
• f_open (i j : self.J) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (self.f i j))

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

theorem TopCat.GlueData.isOpen_iff (D : GlueData) (U : Set ↑D.glued) : IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) ⁻¹' U)

theorem TopCat.GlueData.ι_jointly_surjective (D : GlueData) (x : ↑D.glued) : ∃ (i : D.J) (y : ↑(D.U i)), (CategoryTheory.ConcreteCategory.hom (D.ι i)) y = x

def TopCat.GlueData.Rel (D : GlueData) (a 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

• One or more equations did not get rendered due to their size.

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

theorem TopCat.GlueData.eqvGen_of_π_eq (D : GlueData) {x y : ↑(∐ D.U)} (h : (CategoryTheory.ConcreteCategory.hom D.π) x = (CategoryTheory.ConcreteCategory.hom D.π) y) : Relation.EqvGen (Function.Coequalizer.Rel ⇑(CategoryTheory.ConcreteCategory.hom D.diagram.fstSigmaMap) ⇑(CategoryTheory.ConcreteCategory.hom D.diagram.sndSigmaMap)) x y

theorem TopCat.GlueData.ι_eq_iff_rel (D : GlueData) (i j : D.J) (x : ↑(D.U i)) (y : ↑(D.U j)) : (CategoryTheory.ConcreteCategory.hom (D.ι i)) x = (CategoryTheory.ConcreteCategory.hom (D.ι j)) y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩

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

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

theorem TopCat.GlueData.image_inter (D : GlueData) (i j : D.J) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j)) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (D.f i j) (D.ι i)))

theorem TopCat.GlueData.preimage_range (D : GlueData) (i j : D.J) : ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j)) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.f j i))

theorem TopCat.GlueData.preimage_image_eq_image (D : GlueData) (i j : D.J) (U : Set ↑(D.U i)) : ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) '' U) = ⇑(CategoryTheory.ConcreteCategory.hom (D.f j i)) '' (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))) ⁻¹' U)

theorem TopCat.GlueData.preimage_image_eq_image' (D : GlueData) (i j : D.J) (U : Set ↑(D.U i)) : ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) '' U) = ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i))) '' (⇑(CategoryTheory.ConcreteCategory.hom (D.f i j)) ⁻¹' U)

theorem TopCat.GlueData.open_image_open (D : GlueData) (i : D.J) (U : TopologicalSpace.Opens ↑(D.U i)) : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) '' ↑U)

theorem TopCat.GlueData.ι_isOpenEmbedding (D : GlueData) (i : D.J) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i))

@[deprecated TopCat.GlueData.ι_isOpenEmbedding (since := "2024-10-18")]

theorem TopCat.GlueData.ι_openEmbedding (D : GlueData) (i : D.J) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i))

Alias of TopCat.GlueData.ι_isOpenEmbedding.

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 a✝ : 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) : ⇑(CategoryTheory.ConcreteCategory.hom (self.t i i)) = id
• t_inter ⦃i j : self.J⦄ (k : self.J) (x : ↥(self.V i j)) : ↑x ∈ self.V i k → ↑((CategoryTheory.ConcreteCategory.hom (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) : ↑((CategoryTheory.ConcreteCategory.hom (self.t j k)) ⟨↑((CategoryTheory.ConcreteCategory.hom (self.t i j)) x), ⋯⟩) = ↑((CategoryTheory.ConcreteCategory.hom (self.t i k)) ⟨↑x, h⟩)

theorem TopCat.GlueData.MkCore.t_inv (h : MkCore) (i j : h.J) (x : ↥(h.V j i)) : (CategoryTheory.ConcreteCategory.hom (h.t i j)) ((CategoryTheory.ConcreteCategory.hom (h.t j i)) x) = x

instance TopCat.GlueData.instIsIsoT (h : MkCore) (i j : h.J) : CategoryTheory.IsIso (h.t i j)

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

def TopCat.GlueData.ofOpenSubsets {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : 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.

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_U {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (a✝ : (MkCore.mk (fun (i : J) => (TopologicalSpace.Opens.toTopCat (of α)).obj (U i)) (fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) (fun (i j : J) => ofHom { toFun := fun (x : ↥((fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) i j)) => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J) : (ofOpenSubsets U).U a✝ = (TopologicalSpace.Opens.toTopCat (of α)).obj (U a✝)

@[simp]

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

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_V {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : (MkCore.mk (fun (i : J) => (TopologicalSpace.Opens.toTopCat (of α)).obj (U i)) (fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) (fun (i j : J) => ofHom { toFun := fun (x : ↥((fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) i j)) => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J × (MkCore.mk (fun (i : J) => (TopologicalSpace.Opens.toTopCat (of α)).obj (U i)) (fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) (fun (i j : J) => ofHom { toFun := fun (x : ↥((fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) i j)) => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J) : (ofOpenSubsets U).V i = (TopologicalSpace.Opens.toTopCat ((TopologicalSpace.Opens.toTopCat (of α)).obj (U i.1))).obj ((TopologicalSpace.Opens.map (U i.1).inclusion').obj (U i.2))

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_f {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i j : (MkCore.mk (fun (i : J) => (TopologicalSpace.Opens.toTopCat (of α)).obj (U i)) (fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) (fun (i j : J) => ofHom { toFun := fun (x : ↥((fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) i j)) => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J) : (ofOpenSubsets U).f i j = ((TopologicalSpace.Opens.map (U i).inclusion').obj (U j)).inclusion'

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_t {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i j : (MkCore.mk (fun (i : J) => (TopologicalSpace.Opens.toTopCat (of α)).obj (U i)) (fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) (fun (i j : J) => ofHom { toFun := fun (x : ↥((fun (x j : J) => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j)) i j)) => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }) ⋯ ⋯ ⋯ ⋯).J) : (ofOpenSubsets U).t i j = ofHom { toFun := fun (x : ↥((TopologicalSpace.Opens.map (U i).inclusion').obj (U j))) => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

theorem TopCat.GlueData.ι_fromOpenSubsetsGlue_apply {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : J) (x : CategoryTheory.ToType ((ofOpenSubsets U).U i)) : (CategoryTheory.ConcreteCategory.hom (fromOpenSubsetsGlue U)) ((CategoryTheory.ConcreteCategory.hom ((ofOpenSubsets U).ι i)) x) = (U i).inclusion' x

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

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

theorem TopCat.GlueData.fromOpenSubsetsGlue_isOpenEmbedding {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (fromOpenSubsetsGlue U))

@[deprecated TopCat.GlueData.fromOpenSubsetsGlue_isOpenEmbedding (since := "2024-10-18")]

theorem TopCat.GlueData.fromOpenSubsetsGlue_openEmbedding {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (fromOpenSubsetsGlue U))

Alias of TopCat.GlueData.fromOpenSubsetsGlue_isOpenEmbedding.

theorem TopCat.GlueData.range_fromOpenSubsetsGlue {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (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) : ↑(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 ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.GlueData.fromOpenSubsetsGlue U)) ⋯) ⋯ ⋯