Documentation

Mathlib.Topology.Gluing

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 #

Main results #

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 × JTopCat rather than JJTopCat to connect to the limits library easier.)
  4. An open embedding f i j : V i j ⟶ U i for each i j : ι.
  5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
  6. f i i is an isomorphism.
  7. t i i is the identity.
  8. V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i. (This merely means that V i j ∩ V i k ⊆ t i j ⁻¹' (V j i ∩ V j k).)
  9. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.

We can then glue the topological spaces U i together by identifying V i j with V j i, such that the U i's are open subspaces of the glued space.

Most of the times it would be easier to use the constructor TopCat.GlueData.mk' where the conditions are stated in a less categorical way.

Instances For
    theorem TopCat.GlueData.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)) :

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

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

      Instances For
        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 }) :

        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.

        Instances For
          @[simp]
          theorem TopCat.GlueData.ofOpenSubsets_toGlueData_U {α : Type u} [TopologicalSpace α] {J : Type u} (U : JTopologicalSpace.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 kx (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 : JTopologicalSpace.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 kx (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 kx (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 : JTopologicalSpace.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 kx (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 kx (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) :
          @[simp]
          theorem TopCat.GlueData.ofOpenSubsets_toGlueData_V {α : Type u} [TopologicalSpace α] {J : Type u} (U : JTopologicalSpace.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 kx (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 kx (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) :

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

          Instances For

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

            Instances For
              def TopCat.GlueData.openCoverGlueHomeo {α : Type u} [TopologicalSpace α] {J : Type u} (U : JTopologicalSpace.Opens α) (h : ⋃ (i : J), ↑(U i) = Set.univ) :

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

              Instances For