Extending disjoint open sets along maps of TopCat

A map f : X ⟶ Y of topological spaces extends disjoint open sets (TauCeti.TopCat.extendsDisjointOpens) if every pair of disjoint open subsets of X is the preimage of a pair of disjoint open subsets of Y (TauCeti.TopCat.extendsDisjointOpens_iff). A pair of disjoint open subsets of X is the same as a continuous map from X to the space TauCeti.TopCat.disjointOpensClassifier of pairs of propositions which are not both true, a subspace of the square of the Sierpiński space Prop. So these are the maps with the left lifting property with respect to the map from that space to a point, and the general theory of lifting properties shows that they are stable under cobase change, coproducts and transfinite composition. In particular a relative cell complex in TopCat whose cells extend disjoint open sets extends disjoint open sets. A map with a continuous retraction on a neighbourhood of its range extends disjoint open sets (TauCeti.TopCat.extendsDisjointOpens_of_continuousOn).

The application is to Hausdorffness of cell complexes: two points separated by open sets stay separated after a map which extends disjoint open sets.

• TauCeti.TopCat.t2Space_of_isColimit: the colimit of a directed diagram of Hausdorff spaces is Hausdorff if the maps to the colimit extend disjoint open sets.
• TauCeti.TopCat.t2Space_of_isPushout: attaching a regular Hausdorff space B to a Hausdorff space along a map m : A ⟶ B with closed range which extends disjoint open sets gives a Hausdorff space.

Both rest on the description of the open sets of a colimit in TopCat through their preimages: in a pushout square, two compatible pairs of disjoint open sets of the two sides glue to a pair of disjoint open sets of the corner (TauCeti.TopCat.exists_disjoint_isOpen_of_isPushout).

References

• A. Hatcher, Algebraic Topology, Appendix: the open neighbourhoods N_ε(A) of subsets of a cell complex, which are built cell by cell in the same way, and the proof of Proposition A.3 that cell complexes are normal.

@[reducible, inline]

abbrev TauCeti.TopCat.disjointOpensClassifier : TopCat

The space classifying pairs of disjoint open sets: the pairs (p, q) of propositions which are not both true, as a subspace of the square of the Sierpiński space Prop, lifted to universe u. A pair (U, V) of disjoint open subsets of a space X corresponds to the continuous map x ↦ (x ∈ U, x ∈ V).

def TauCeti.TopCat.extendsDisjointOpens : CategoryTheory.MorphismProperty TopCat

The maps of TopCat which extend disjoint open sets: the maps with the left lifting property with respect to the map from TauCeti.TopCat.disjointOpensClassifier to a point. By TauCeti.TopCat.extendsDisjointOpens_iff, a map f : X ⟶ Y extends disjoint open sets if and only if every pair of disjoint open subsets of X is the preimage under f of a pair of disjoint open subsets of Y.

instance TauCeti.TopCat.instIsMultiplicativeTopCatExtendsDisjointOpens : extendsDisjointOpens.IsMultiplicative

instance TauCeti.TopCat.instIsStableUnderRetractsTopCatExtendsDisjointOpens : extendsDisjointOpens.IsStableUnderRetracts

instance TauCeti.TopCat.instIsStableUnderCobaseChangeTopCatExtendsDisjointOpens : extendsDisjointOpens.IsStableUnderCobaseChange

instance TauCeti.TopCat.instIsStableUnderCoproductsTopCatExtendsDisjointOpens : CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{w, u, u + 1} extendsDisjointOpens

instance TauCeti.TopCat.instIsStableUnderTransfiniteCompositionTopCatExtendsDisjointOpens : extendsDisjointOpens.IsStableUnderTransfiniteComposition

theorem TauCeti.TopCat.extendsDisjointOpens_iff {X Y : TopCat} (f : X ⟶ Y) : extendsDisjointOpens f ↔ ∀ (U V : Set ↑X), IsOpen U → IsOpen V → Disjoint U V → ∃ (U' : Set ↑Y) (V' : Set ↑Y), IsOpen U' ∧ IsOpen V' ∧ Disjoint U' V' ∧ ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' U' = U ∧ ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' V' = V

A map f : X ⟶ Y of TopCat extends disjoint open sets if and only if every pair of disjoint open subsets of X is the preimage under f of a pair of disjoint open subsets of Y.

theorem TauCeti.TopCat.extendsDisjointOpens_of_continuousOn {X Y : TopCat} {Z : Type u_1} [TopologicalSpace Z] (m : X ⟶ Y) {μ : ↑X → Z} (hμ : Topology.IsInducing μ) {N : Set ↑Y} (hN : IsOpen N) {ρ : ↑Y → Z} (hρ : ContinuousOn ρ N) (hmN : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom m) x ∈ N) (hρN : Set.MapsTo ρ N (Set.range μ)) (hρm : ∀ (x : ↑X), ρ ((CategoryTheory.ConcreteCategory.hom m) x) = μ x) : extendsDisjointOpens m

A map m : X ⟶ Y of TopCat extends disjoint open sets if it has a continuous retraction near its range, read through an inducing map μ : X → Z: a map ρ : Y → Z continuous on an open neighbourhood N of the range of m, sending N into the range of μ, with ρ ∘ m = μ. An open subset μ ⁻¹' W of X is then the trace of the open set N ∩ ρ ⁻¹' W, and these sets are disjoint over disjoint sets. For the boundary sphere of a disk, ρ is the radial projection.

theorem TauCeti.TopCat.t2Space_of_isColimit {J : Type w} [Preorder J] [IsDirectedOrder J] {F : CategoryTheory.Functor J TopCat} [∀ (j : J), T2Space ↑(F.obj j)] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (h : ∀ (j : J), extendsDisjointOpens (c.ι.app j)) : T2Space ↑c.pt

The colimit of a directed diagram of Hausdorff spaces is Hausdorff if the maps from the spaces of the diagram to the colimit extend disjoint open sets.

theorem TauCeti.TopCat.exists_disjoint_isOpen_of_isPushout {A B X P : TopCat} {g : A ⟶ X} {m : A ⟶ B} {f : X ⟶ P} {g₂ : B ⟶ P} (sq : CategoryTheory.IsPushout g m f g₂) {U V : Set ↑X} (hU : IsOpen U) (hV : IsOpen V) (h : Disjoint U V) {U' V' : Set ↑B} (hU' : IsOpen U') (hV' : IsOpen V') (h' : Disjoint U' V') (hUU' : ⇑(CategoryTheory.ConcreteCategory.hom g) ⁻¹' U = ⇑(CategoryTheory.ConcreteCategory.hom m) ⁻¹' U') (hVV' : ⇑(CategoryTheory.ConcreteCategory.hom g) ⁻¹' V = ⇑(CategoryTheory.ConcreteCategory.hom m) ⁻¹' V') : ∃ (W : Set ↑P) (W' : Set ↑P), IsOpen W ∧ IsOpen W' ∧ Disjoint W W' ∧ ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' W = U ∧ ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' W' = V ∧ ⇑(CategoryTheory.ConcreteCategory.hom g₂) ⁻¹' W = U' ∧ ⇑(CategoryTheory.ConcreteCategory.hom g₂) ⁻¹' W' = V'

In a pushout square in TopCat, compatible pairs of disjoint open sets of the two sides glue to a pair of disjoint open sets of the corner.

theorem TauCeti.TopCat.t2Space_of_isPushout {A B X P : TopCat} {g : A ⟶ X} {m : A ⟶ B} {f : X ⟶ P} {g₂ : B ⟶ P} (sq : CategoryTheory.IsPushout g m f g₂) [T2Space ↑X] [T2Space ↑B] [RegularSpace ↑B] (hm : extendsDisjointOpens m) (hm' : IsClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom m))) : T2Space ↑P

Attaching a regular Hausdorff space B to a Hausdorff space X along a map m : A ⟶ B with closed range which extends disjoint open sets gives a Hausdorff space: in a pushout square in TopCat with sides m : A ⟶ B and f : X ⟶ P, the corner P is Hausdorff.