Separation, countability, local compactness, and connectedness of glued spaces

A space obtained by gluing open charts is second countable when the chart family is countable and every chart is second countable. It is locally compact when every chart is locally compact. It is Hausdorff exactly when the gluing relation between each pair of charts is closed in their product. The latter criterion isolates the mathematical separation argument needed in applications: for example, toric charts must prove that their monomial overlap relation is closed.

By the cocycle condition, the gluing relation between two charts is the image of their overlap under its two maps to the charts, and it is also the relation generated by all identifications. For Hausdorff charts, its closedness only has to be checked at the boundaries of the overlaps: over the overlap V (i, j) the relation is the graph of a continuous map into a Hausdorff space, hence closed there. The glued space is therefore Hausdorff exactly when the charts are and any point of the i-th chart outside V (i, j) and any point of the j-th chart outside the overlap have neighbourhoods containing no pair of identified points (TopCat.GlueData.t2Space_iff_forall_nhds). These are finitely many checks for finitely many charts, and they hold automatically when the overlaps are closed in their charts.

Connectedness is controlled by the overlap graph, whose vertices are the charts and in which i and j are adjacent when the overlap V (i, j) is nonempty. A space glued from preconnected charts is preconnected exactly when any two nonempty charts are joined by a path in this graph, and a space glued from a nonempty family of connected charts is connected exactly when the overlap graph is connected. Paths may pass through charts which are not adjacent to their endpoints: the criterion uses the generated relation, not a single overlap.

def TopCat.GlueData.chartRel (D : GlueData) (i j : D.J) : Set (↑(D.U i) × ↑(D.U j))

The relation between the i-th and j-th charts: two points are related when the gluing identifies their images.

theorem TopCat.GlueData.mem_chartRel_iff_exists (D : GlueData) {i j : D.J} {p : ↑(D.U i) × ↑(D.U j)} : p ∈ D.chartRel i j ↔ ∃ (z : ↑(D.V (i, j))), (CategoryTheory.ConcreteCategory.hom (D.f i j)) z = p.1 ∧ (CategoryTheory.ConcreteCategory.hom (D.f j i)) ((CategoryTheory.ConcreteCategory.hom (D.t i j)) z) = p.2

A point of the i-th chart and a point of the j-th chart are related exactly when they are the images of a single point of the overlap V (i, j) under f i j and under f j i composed with the transition t i j.

@[simp]

theorem TopCat.GlueData.mem_chartRel_iff (D : GlueData) {i j : D.J} {p : ↑(D.U i) × ↑(D.U j)} : p ∈ D.chartRel i j ↔ (CategoryTheory.ConcreteCategory.hom (D.ι i)) p.1 = (CategoryTheory.ConcreteCategory.hom (D.ι j)) p.2

Membership in the relation between two charts is equivalent to equality of their images in the glued space.

theorem TopCat.GlueData.isOpenQuotientMap_sigma_ι (D : GlueData) : IsOpenQuotientMap fun (x : (i : D.J) × ↑(D.U i)) => (CategoryTheory.ConcreteCategory.hom (D.ι x.fst)) x.snd

The map from the disjoint union of the charts to the glued space is an open quotient map.

theorem TopCat.GlueData.t2Space_iff_isClosed_chartRel (D : GlueData) : T2Space ↑D.glued ↔ ∀ (i j : D.J), IsClosed (D.chartRel i j)

The space obtained by gluing open charts is Hausdorff exactly when the gluing relation between every pair of charts is closed in the product of those charts.

theorem TopCat.GlueData.iUnion_range_ι (D : GlueData) : ⋃ (i : D.J), Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) = Set.univ

The images of the charts cover the glued space.

theorem TopCat.GlueData.prod_ι_jointly_surjective (D : GlueData) (D' : GlueData) (x : ↑D.glued × ↑D'.glued) : ∃ (ij : D.J × D'.J) (y : ↑(D.U ij.1) × ↑(D'.U ij.2)), Prod.map (⇑(CategoryTheory.ConcreteCategory.hom (D.ι ij.1))) (⇑(CategoryTheory.ConcreteCategory.hom (D'.ι ij.2))) y = x

Pairs of canonical inclusions jointly cover the product of two glued spaces.

instance TopCat.GlueData.secondCountableTopology (D : GlueData) [Countable D.J] [∀ (i : D.J), SecondCountableTopology ↑(D.U i)] : SecondCountableTopology ↑D.glued

A glued space with countably many second-countable charts is second countable.

instance TopCat.GlueData.locallyCompactSpace (D : GlueData) [∀ (i : D.J), LocallyCompactSpace ↑(D.U i)] : LocallyCompactSpace ↑D.glued

A glued space with locally compact charts is locally compact.

Hausdorffness from the boundaries of the overlaps

theorem TopCat.GlueData.swap_mem_chartRel_iff (D : GlueData) {i j : D.J} {p : ↑(D.U i) × ↑(D.U j)} : p.swap ∈ D.chartRel j i ↔ p ∈ D.chartRel i j

Exchanging the two points of a pair exchanges the relations between two charts.

theorem TopCat.GlueData.mem_chartRel_of_mem_closure (D : GlueData) {i j : D.J} [T2Space ↑(D.U j)] {p : ↑(D.U i) × ↑(D.U j)} (hp : p ∈ closure (D.chartRel i j)) (h : p.1 ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.f i j))) : p ∈ D.chartRel i j

Let the j-th chart be Hausdorff. A pair in the closure of the relation between the i-th and j-th charts lies in the relation as soon as its first point lies in the overlap: there the relation is the graph of the continuous transition map.

theorem TopCat.GlueData.isClosed_chartRel_iff (D : GlueData) {i j : D.J} [T2Space ↑(D.U i)] [T2Space ↑(D.U j)] : IsClosed (D.chartRel i j) ↔ ∀ x ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.f i j)), ∀ y ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.f j i)), ∃ A ∈ nhds x, ∃ B ∈ nhds y, ∀ (z : ↑(D.V (i, j))), (CategoryTheory.ConcreteCategory.hom (D.f i j)) z ∈ A → (CategoryTheory.ConcreteCategory.hom (D.f j i)) ((CategoryTheory.ConcreteCategory.hom (D.t i j)) z) ∉ B

Boundary criterion. For Hausdorff charts, the relation between the i-th and j-th charts is closed exactly when a point of the i-th chart outside the overlap V (i, j) and a point of the j-th chart outside the overlap always have neighbourhoods containing no pair of points identified by the gluing.

theorem TopCat.GlueData.t2Space_iff_forall_nhds (D : GlueData) : T2Space ↑D.glued ↔ (∀ (i : D.J), T2Space ↑(D.U i)) ∧ ∀ (i j : D.J), ∀ x ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.f i j)), ∀ y ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.f j i)), ∃ A ∈ nhds x, ∃ B ∈ nhds y, ∀ (z : ↑(D.V (i, j))), (CategoryTheory.ConcreteCategory.hom (D.f i j)) z ∈ A → (CategoryTheory.ConcreteCategory.hom (D.f j i)) ((CategoryTheory.ConcreteCategory.hom (D.t i j)) z) ∉ B

Hausdorff criterion for glued spaces. The glued space is Hausdorff exactly when every chart is Hausdorff and, for all charts i and j, a point of the i-th chart outside the overlap V (i, j) and a point of the j-th chart outside the overlap always have neighbourhoods containing no pair of points identified by the gluing.

Only points on the boundaries of the overlaps need to be checked, and the condition is vacuous for i = j, since V (i, i) is the whole i-th chart.

theorem TopCat.GlueData.t2Space_of_isClosed_range (D : GlueData) [∀ (i : D.J), T2Space ↑(D.U i)] (h : ∀ (i j : D.J), IsClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.f i j)))) : T2Space ↑D.glued

A space glued from Hausdorff charts along overlaps which are closed in their charts is Hausdorff.

Connectedness and the overlap graph

@[simp]

theorem TopCat.GlueData.range_ι_inter_range_ι_nonempty_iff (D : GlueData) (i j : D.J) : (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) ∩ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j))).Nonempty ↔ Nonempty ↑(D.V (i, j))

The images of two charts in the glued space meet exactly when their overlap is nonempty.

theorem TopCat.GlueData.transGen_of_preconnectedSpace (D : GlueData) [PreconnectedSpace ↑D.glued] {i j : D.J} (hi : Nonempty ↑(D.U i)) (hj : Nonempty ↑(D.U j)) : Relation.TransGen (fun (i j : D.J) => Nonempty ↑(D.V (i, j))) i j

If the glued space is preconnected, then any two nonempty charts are joined by a nonempty chain of charts with consecutive nonempty overlaps.

theorem TopCat.GlueData.preconnectedSpace_iff_reflTransGen (D : GlueData) [∀ (i : D.J), PreconnectedSpace ↑(D.U i)] : PreconnectedSpace ↑D.glued ↔ ∀ (i j : D.J), Nonempty ↑(D.U i) → Nonempty ↑(D.U j) → Relation.ReflTransGen (fun (i j : D.J) => Nonempty ↑(D.V (i, j))) i j

A space glued from preconnected charts is preconnected exactly when any two nonempty charts are joined by a chain of charts with consecutive nonempty overlaps. Empty charts impose no condition.

theorem TopCat.GlueData.connectedSpace_iff_reflTransGen (D : GlueData) [Nonempty D.J] [∀ (i : D.J), ConnectedSpace ↑(D.U i)] : ConnectedSpace ↑D.glued ↔ ∀ (i j : D.J), Relation.ReflTransGen (fun (i j : D.J) => Nonempty ↑(D.V (i, j))) i j

A space glued from a nonempty family of connected charts is connected exactly when the overlap graph is connected: any two charts are joined by a chain of charts with consecutive nonempty overlaps.