The Hausdorff criterion for a glued space #
Let D be topological gluing data (Mathlib's TopCat.GlueData: spaces U i, open subsets
V (i, j) ⊆ U i through the open embeddings f i j, transition homeomorphisms t i j). If every
U i is Hausdorff and, for i ≠ j, the graph {(f i j x, f j i (t i j x))} of the transition map
(transitionGraph) is closed in U i × U j, then the glued space is Hausdorff
(t2Space_glued_of_isClosed_transitionGraph). Mathlib's TopCat.GlueData carries no separation
statement; this is the separation lemma the gluing of local complexifications rests on, where the
whole difficulty is to arrange closed graphs by shrinking the pieces (following the shrinking
pattern of the proof of [Car57, §3, Proposition 2], which shrinks the covers for the sheaf
cocycle).
Conventions. Points of D.glued are ι i y, and ι i y = ι j y' iff D.Rel ⟨i, y⟩ ⟨j, y'⟩, that
is, iff (y, y') = (f i j x, f j i (t i j x)) for some x : V (i, j) (Mathlib's ι_eq_iff_rel,
mem_transitionGraph_iff_rel). Two points ι i y ≠ ι j y' are separated by the images of disjoint
neighbourhoods when i = j (Hausdorffness of U i, injectivity of ι i) and by the images of a
product neighbourhood of (y, y') disjoint from the closed graph when i ≠ j. For a single space
the criterion is the Hausdorffness of U; for a disjoint gluing (V (i, j) = ∅ for i ≠ j) the
graphs are empty and the glued space is the disjoint union. The converse (a Hausdorff glued space
has closed graphs) holds as well; nothing in the library requires it, so it is not proved here.
The graph of the transition map from the i-th to the j-th piece, as a subset of
U i × U j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Hausdorff criterion: Hausdorff pieces and closed transition graphs give a Hausdorff glued space.