Open embeddings from pushouts and coproducts in TopCat

This file records the open embeddings produced by the two colimits used to attach cells.

• Pushouts: in a pushout square

       g
    A ───> B
  f │      │ f'
    v      v
    A' ──> B'
       g'
  

  of TopCat, the map g' carries the complement of the range of f onto the complement of the range of f' (TauCeti.TopCat.image_compl_range_of_isPushout), sends open subsets of that complement to open subsets (TauCeti.TopCat.isOpen_image_of_isPushout), and so restricts to an open embedding on it when the range of f is closed (TauCeti.TopCat.isOpenEmbedding_domRestrict_compl_range_of_isPushout).
• Coproducts: the injections of a colimit cofan in TopCat are open embeddings (TauCeti.TopCat.isOpenEmbedding_inj_of_isColimit).

When f is a coproduct of boundary inclusions ∂𝔻 n ⟶ 𝔻 n, the complement of its range is the union of the open disks, so these statements show that attaching cells embeds each open disk homeomorphically onto an open subset of the new space, away from the old one; see TauCeti.Topology.CWComplex.Abstract.OpenCell.

References

• A. Hatcher, Algebraic Topology, Appendix, on the topology of cell complexes.

theorem TauCeti.TopCat.image_compl_range_of_isPushout {A A' B B' : TopCat} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : CategoryTheory.IsPushout g f f' g') : ⇑(CategoryTheory.ConcreteCategory.hom g') '' (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))ᶜ = (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f'))ᶜ

In a pushout square in TopCat, the map opposite to f' carries the complement of the range of f onto the complement of the range of f'.

theorem TauCeti.TopCat.isOpen_image_of_isPushout {A A' B B' : TopCat} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : CategoryTheory.IsPushout g f f' g') {W : Set ↑A'} (hW : IsOpen W) (hWf : W ⊆ (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))ᶜ) : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom g') '' W)

In a pushout square in TopCat, the map opposite to f' sends open subsets of the complement of the range of f to open subsets.

theorem TauCeti.TopCat.isOpenEmbedding_domRestrict_compl_range_of_isPushout {A A' B B' : TopCat} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : CategoryTheory.IsPushout g f f' g') (hf : IsClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))) : Topology.IsOpenEmbedding ((Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))ᶜ.domRestrict ⇑(CategoryTheory.ConcreteCategory.hom g'))

In a pushout square in TopCat where the range of f is closed, the map opposite to f' restricts to an open embedding on the complement of the range of f.

theorem TauCeti.TopCat.isOpenEmbedding_inj_of_isColimit {ι : Type w} {X : ι → TopCat} {c : CategoryTheory.Limits.Cofan X} (hc : CategoryTheory.Limits.IsColimit c) (i : ι) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (c.inj i))

In TopCat, the injections of a colimit cofan are open embeddings.