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)

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

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.

theorem TopCat.GlueData.π_surjective (D : TopCat.GlueData) : Function.Surjective ↑(CategoryTheory.GlueData.π D.toGlueData)

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

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

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

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 (CategoryTheory.Limits.Types.CoequalizerRel ↑(CategoryTheory.Limits.MultispanIndex.fstSigmaMap (CategoryTheory.GlueData.diagram D.toGlueData)) ↑(CategoryTheory.Limits.MultispanIndex.sndSigmaMap (CategoryTheory.GlueData.diagram D.toGlueData))) 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.ι_injective (D : TopCat.GlueData) (i : D.J) : Function.Injective ↑(CategoryTheory.GlueData.ι D.toGlueData i)

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

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

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)

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

theorem TopCat.GlueData.ι_openEmbedding (D : TopCat.GlueData) (i : D.J) : OpenEmbedding ↑(CategoryTheory.GlueData.ι D.toGlueData i)

structure TopCat.GlueData.MkCore : Type (u + 1)

• J : Type u
• U : s.J → TopCat
• V : (i : s.J) → s.J → TopologicalSpace.Opens ↑(TopCat.GlueData.MkCore.U s i)
• t : (i j : s.J) → (TopologicalSpace.Opens.toTopCat (TopCat.GlueData.MkCore.U s i)).obj (TopCat.GlueData.MkCore.V s i j) ⟶ (TopologicalSpace.Opens.toTopCat (TopCat.GlueData.MkCore.U s j)).obj (TopCat.GlueData.MkCore.V s j i)
• V_id : ∀ (i : s.J), TopCat.GlueData.MkCore.V s i i = ⊤
• t_id : ∀ (i : s.J), ↑(TopCat.GlueData.MkCore.t s i i) = id
• t_inter : ∀ ⦃i j : s.J⦄ (k : s.J) (x : { x // x ∈ TopCat.GlueData.MkCore.V s i j }), ↑x ∈ TopCat.GlueData.MkCore.V s i k → ↑(↑(TopCat.GlueData.MkCore.t s i j) x) ∈ TopCat.GlueData.MkCore.V s j k
• cocycle : ∀ (i j k : s.J) (x : { x // x ∈ TopCat.GlueData.MkCore.V s i j }) (h : ↑x ∈ TopCat.GlueData.MkCore.V s i k), ↑(↑(TopCat.GlueData.MkCore.t s j k) { val := ↑(↑(TopCat.GlueData.MkCore.t s i j) x), property := (_ : ↑(↑(TopCat.GlueData.MkCore.t s i j) x) ∈ TopCat.GlueData.MkCore.V s j k) }) = ↑(↑(TopCat.GlueData.MkCore.t s i k) { 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.

theorem TopCat.GlueData.MkCore.t_inv (h : TopCat.GlueData.MkCore) (i : h.J) (j : h.J) (x : { x // x ∈ TopCat.GlueData.MkCore.V h j i }) : ↑(TopCat.GlueData.MkCore.t h i j) (↑(TopCat.GlueData.MkCore.t h j i) x) = x

instance TopCat.GlueData.instIsIsoTopCatInstTopCatLargeCategoryObjOpensαTopologicalSpaceUTopologicalSpace_coeToQuiverToCategoryStructSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToQuiverToCategoryStructToPrefunctorToTopCatVT (h : TopCat.GlueData.MkCore) (i : h.J) (j : h.J) : CategoryTheory.IsIso (TopCat.GlueData.MkCore.t h i j)

def TopCat.GlueData.MkCore.t' (h : TopCat.GlueData.MkCore) (i : h.J) (j : h.J) (k : h.J) : CategoryTheory.Limits.pullback (TopologicalSpace.Opens.inclusion (TopCat.GlueData.MkCore.V h i j)) (TopologicalSpace.Opens.inclusion (TopCat.GlueData.MkCore.V h i k)) ⟶ CategoryTheory.Limits.pullback (TopologicalSpace.Opens.inclusion (TopCat.GlueData.MkCore.V h j k)) (TopologicalSpace.Opens.inclusion (TopCat.GlueData.MkCore.V h j i))

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

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.

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_U {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : ∀ (a : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) (_ : ∀ (i : J), (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i i = ⊤) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }), ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k → ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }) (h : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }))).J), CategoryTheory.GlueData.U (TopCat.GlueData.ofOpenSubsets U).toGlueData a = (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U a)

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_t {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) (_ : ∀ (i : J), (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i i = ⊤) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }), ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k → ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }) (h : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }))).J) (j : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) (_ : ∀ (i : J), (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i i = ⊤) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }), ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k → ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }) (h : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }))).J) : CategoryTheory.GlueData.t (TopCat.GlueData.ofOpenSubsets U).toGlueData i j = ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_f {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) (_ : ∀ (i : J), (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i i = ⊤) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }), ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k → ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }) (h : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }))).J) (j : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) (_ : ∀ (i : J), (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i i = ⊤) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }), ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k → ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }) (h : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }))).J) : CategoryTheory.GlueData.f (TopCat.GlueData.ofOpenSubsets U).toGlueData i j = TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j))

@[simp]

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

@[simp]

theorem TopCat.GlueData.ofOpenSubsets_toGlueData_V {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) (_ : ∀ (i : J), (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i i = ⊤) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }), ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k → ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }) (h : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }))).J × (TopCat.GlueData.MkCore.mk (fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i)) (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) (fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) (_ : ∀ (i : J), (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i i = ⊤) (_ : ∀ (i : J), ↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i i) = id) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }), ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k → ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) (_ : ∀ (i j k : J) (x : { x // x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j }) (h : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k), ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }) = ↑(↑((fun i j => ContinuousMap.mk fun x => { val := { val := ↑↑x, property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).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 => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i j) }, property := (_ : ↑↑x ∈ U i) }) i j) x), property := (_ : ↑x ∈ (fun i j => (TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i))).obj (U j)) i k) }))).J) : CategoryTheory.GlueData.V (TopCat.GlueData.ofOpenSubsets U).toGlueData i = (TopologicalSpace.Opens.toTopCat ((TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i.fst))).obj ((TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusion (U i.fst))).obj (U i.snd))

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.

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

theorem TopCat.GlueData.ι_fromOpenSubsetsGlue_apply {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) (i : J) (x : (CategoryTheory.forget TopCat).obj (CategoryTheory.Limits.MultispanIndex.right (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData) i)) : ↑(CategoryTheory.Limits.Multicoequalizer.desc (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData) (TopCat.of α) (fun x => TopologicalSpace.Opens.inclusion (U x)) (_ : ∀ (a : (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).L), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.fst (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData) a) ((fun x => TopologicalSpace.Opens.inclusion (U x)) (CategoryTheory.Limits.MultispanIndex.fstFrom (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData) a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.MultispanIndex.snd (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData) a) ((fun x => TopologicalSpace.Opens.inclusion (U x)) (CategoryTheory.Limits.MultispanIndex.sndFrom (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData) a)))) (↑(CategoryTheory.Limits.Multicoequalizer.π (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData) i) x) = ↑(TopologicalSpace.Opens.inclusion (U i)) x

@[simp]

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

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) : ↑(CategoryTheory.GlueData.glued (TopCat.GlueData.ofOpenSubsets U).toGlueData) ≃ₜ α

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