Closed embeddings in TopCat

This file introduces the morphism property TauCeti.TopCat.isClosedEmbedding of TopCat, the closed embeddings, and proves that it is stable under the operations used to build relative cell complexes:

• cobase change: in a pushout square, the map opposite to a closed embedding is a closed embedding (TauCeti.TopCat.isClosedEmbedding_of_isPushout);
• coproducts: a coproduct of closed embeddings is a closed embedding (TauCeti.TopCat.isClosedEmbedding_sigmaMap);
• transfinite composition: if every successor map of a well-order-continuous diagram is a closed embedding, then so is every transition map (TauCeti.TopCat.isClosedEmbedding_map_of_isWellOrderContinuous), and a transfinite composition of closed embeddings is a closed embedding (the IsStableUnderTransfiniteComposition instance). Mathlib's MorphismProperty.TransfiniteCompositionOfShape.mem_incl_app then shows that the map from each stage of such a composition to the composite is a closed embedding.

The last point comes from a statement about directed colimits: if all transition maps of a directed diagram are closed embeddings, so are the maps to its colimit (TauCeti.TopCat.isClosedEmbedding_ι_of_isColimit), refining the corresponding statement for injective maps (TauCeti.TopCat.injective_ι_of_isColimit).

With Mathlib's description of a relative cell complex as a transfinite composition of pushouts of coproducts of its basic cells, these stability properties show that a relative cell complex in TopCat whose basic cells are closed embeddings is a closed embedding; see TauCeti.Topology.CWComplex.Abstract.ClosedEmbedding.

References

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

def TauCeti.TopCat.isClosedEmbedding : CategoryTheory.MorphismProperty TopCat

The closed embeddings, as a class of morphisms of TopCat.

@[simp]

theorem TauCeti.TopCat.isClosedEmbedding_iff {X Y : TopCat} (f : X ⟶ Y) : isClosedEmbedding f ↔ Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)

instance TauCeti.TopCat.instIsMultiplicativeTopCatIsClosedEmbedding : isClosedEmbedding.IsMultiplicative

instance TauCeti.TopCat.instRespectsIsoTopCatIsClosedEmbedding : isClosedEmbedding.RespectsIso

theorem TauCeti.TopCat.isClosed_iff_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') (s : Set ↑B') : IsClosed s ↔ IsClosed (⇑(CategoryTheory.ConcreteCategory.hom f') ⁻¹' s) ∧ IsClosed (⇑(CategoryTheory.ConcreteCategory.hom g') ⁻¹' s)

A subset of the corner of a pushout square in TopCat is closed if and only if its preimages under the two maps into the corner are closed.

theorem TauCeti.TopCat.isClosedEmbedding_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 : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f')

In TopCat, the cobase change of a closed embedding is a closed embedding: in a pushout square, the map opposite to a closed embedding is a closed embedding.

instance TauCeti.TopCat.instIsStableUnderCobaseChangeTopCatIsClosedEmbedding : isClosedEmbedding.IsStableUnderCobaseChange

theorem TauCeti.TopCat.isClosedEmbedding_sigmaMap {ι : Type w} {X₁ X₂ : ι → TopCat} [CategoryTheory.Limits.HasCoproduct X₁] [CategoryTheory.Limits.HasCoproduct X₂] (f : (i : ι) → X₁ i ⟶ X₂ i) (hf : ∀ (i : ι), Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (f i))) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.map f))

In TopCat, a coproduct of closed embeddings is a closed embedding.

instance TauCeti.TopCat.instIsStableUnderCoproductsOfShapeTopCatIsClosedEmbedding (J : Type w) : isClosedEmbedding.IsStableUnderCoproductsOfShape J

instance TauCeti.TopCat.instIsStableUnderCoproductsTopCatIsClosedEmbedding : CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{w, u, u + 1} isClosedEmbedding

theorem TauCeti.TopCat.isClosedEmbedding_ι_of_isColimit {J : Type w} [Preorder J] [IsDirectedOrder J] {F : CategoryTheory.Functor J TopCat} (hF : ∀ ⦃i j : J⦄ (hij : i ≤ j), Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij)))) {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (i : J) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app i))

If all transition maps of a directed diagram in TopCat are closed embeddings, then so are the maps from the objects of the diagram to its colimit.

theorem TauCeti.TopCat.isClosedEmbedding_map_of_isWellOrderContinuous {J : Type w} [LinearOrder J] [SuccOrder J] [WellFoundedLT J] (F : CategoryTheory.Functor J TopCat) [F.IsWellOrderContinuous] (hF : ∀ (j : J), ¬IsMax j → Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯)))) {i j : J} (hij : i ≤ j) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij)))

If every successor map of a well-order-continuous diagram in TopCat is a closed embedding, then so is every transition map.

instance TauCeti.TopCat.instIsStableUnderTransfiniteCompositionTopCatIsClosedEmbedding : isClosedEmbedding.IsStableUnderTransfiniteComposition