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.toGlueData.V (i, j) ⟶ self.toGlueData.U i
• f_mono : ∀ (i j : self.J), CategoryTheory.Mono (self.toGlueData.f i j)
• f_hasPullback : ∀ (i j k : self.J), CategoryTheory.Limits.HasPullback (self.toGlueData.f i j) (self.toGlueData.f i k)
• f_id : ∀ (i : self.J), CategoryTheory.IsIso (self.toGlueData.f i i)
• t : (i j : self.J) → self.toGlueData.V (i, j) ⟶ self.toGlueData.V (j, i)
• t_id : ∀ (i : self.J), self.toGlueData.t i i = CategoryTheory.CategoryStruct.id (self.toGlueData.V (i, i))
• t' : (i j k : self.J) → CategoryTheory.Limits.pullback (self.toGlueData.f i j) (self.toGlueData.f i k) ⟶ CategoryTheory.Limits.pullback (self.toGlueData.f j k) (self.toGlueData.f j i)
• t_fac : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.toGlueData.t' i j k) CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (self.toGlueData.t i j)
• cocycle : ∀ (i j k : self.J), CategoryTheory.CategoryStruct.comp (self.toGlueData.t' i j k) (CategoryTheory.CategoryStruct.comp (self.toGlueData.t' j k i) (self.toGlueData.t' k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (self.toGlueData.f i j) (self.toGlueData.f i k))
• f_open : ∀ (i j : self.J), OpenEmbedding ⇑(self.toGlueData.f i j)

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 : D.J) (y : ↑(D.toGlueData.U i)), (CategoryTheory.GlueData.ι D.toGlueData i) y = x

def TopCat.GlueData.Rel (D : TopCat.GlueData) (a : (i : D.J) × ↑(D.toGlueData.U i)) (b : (i : D.J) × ↑(D.toGlueData.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 : 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 : ↑(D.toGlueData.U i)) (y : ↑(D.toGlueData.U 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)

Equations

• (_ : CategoryTheory.Mono (CategoryTheory.GlueData.ι D.toGlueData i)) = (_ : 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 (D.toGlueData.f 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 ⇑(D.toGlueData.f j i)

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

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

theorem TopCat.GlueData.open_image_open (D : TopCat.GlueData) (i : D.J) (U : TopologicalSpace.Opens ↑(D.toGlueData.U 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)

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)).toPrefunctor.obj (self.V i j) ⟶ (TopologicalSpace.Opens.toTopCat (self.U j)).toPrefunctor.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) { val := ↑((self.t i j) x), property := (_ : ↑((self.t i j) x) ∈ self.V j k) }) = ↑((self.t i k) { val := ↑x, property := 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.instIsIsoTopCatInstTopCatLargeCategoryObjOpensαTopologicalSpaceUTopologicalSpace_coeToQuiverToCategoryStructSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToQuiverToCategoryStructToPrefunctorToTopCatVT (h : TopCat.GlueData.MkCore) (i : h.J) (j : h.J) : CategoryTheory.IsIso (h.t i j)

Equations

• (_ : CategoryTheory.IsIso (h.t i j)) = (_ : CategoryTheory.IsIso (h.t 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 (h.V i j)) (TopologicalSpace.Opens.inclusion (h.V i k)) ⟶ CategoryTheory.Limits.pullback (TopologicalSpace.Opens.inclusion (h.V j k)) (TopologicalSpace.Opens.inclusion (h.V j i))

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

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).toPrefunctor.obj ((CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).right i)) : (CategoryTheory.Limits.Multicoequalizer.desc (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData) (TopCat.of α) (fun (x : (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).R) => TopologicalSpace.Opens.inclusion (U x)) (_ : ∀ (a : (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).L), CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).fst a) ((fun (x : (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).R) => TopologicalSpace.Opens.inclusion (U x)) ((CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).fstFrom a)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).snd a) ((fun (x : (CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).R) => TopologicalSpace.Opens.inclusion (U x)) ((CategoryTheory.GlueData.diagram (TopCat.GlueData.ofOpenSubsets U).toGlueData).sndFrom 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.

Equations

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