Compact supports in relative CW complexes

A compact subset of a relative CW complex meets only finitely many open cells outside the base. Consequently it lies in a skeleton of finite dimension, even when the complex is infinite-dimensional. The base itself need not be compact or finite-dimensional. So the preimages of the skeleta under a continuous map into the complex absorb every compact set (TauCeti.exists_subset_preimageSkeleton_of_isCompact).

These are the compact-support statements used to pass from skeletal homology to homology of the whole pair. They do not require local finiteness of the CW structure. The key weak-topology criterion is that a subset meeting each open cell in a finite set is closed (respectively discrete) as soon as its intersection with the base is.

References

• A. Hatcher, Algebraic Topology, Appendix, Proposition A.1.

theorem TauCeti.isClosed_of_finite_inter_openCell {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D S : Set X} [Topology.RelCWComplex C D] (hSC : S ⊆ C) (hSD : IsClosed (S ∩ D)) (hS : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), (S ∩ Topology.RelCWComplex.openCell n i).Finite) : IsClosed S

A subset of a relative CW complex is closed if it meets each open cell in a finite set and meets the base in a closed set.

theorem TauCeti.isDiscrete_of_finite_inter_openCell {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D S : Set X} [Topology.RelCWComplex C D] (hSC : S ⊆ C) (hSD : IsDiscrete (S ∩ D)) (hS : ∀ (n : ℕ) (i : Topology.RelCWComplex.cell C n), (S ∩ Topology.RelCWComplex.openCell n i).Finite) : IsDiscrete S

A subset of a relative CW complex is discrete if it meets each open cell in a finite set and meets the base in a discrete set.

theorem TauCeti.finite_setOf_nonempty_inter_openCell_of_isCompact {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {K : Set X} (hK : IsCompact K) : {a : (n : ℕ) × Topology.RelCWComplex.cell C n | (K ∩ Topology.RelCWComplex.openCell a.fst a.snd).Nonempty}.Finite

A compact subset of the ambient space meets only finitely many relative open cells. There is no local-finiteness or dimension assumption, and the base is excluded from the cell indexing.

theorem TauCeti.exists_subset_skeletonLT_of_isCompact {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {K : Set X} (hK : IsCompact K) (hKC : K ⊆ C) : ∃ (n : ℕ), K ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑n)

Every compact subset of a relative CW complex is contained in a skeleton of finite relative dimension. The skeleton contains the entire base, so no restriction on the base is needed.

theorem TauCeti.exists_subset_preimageSkeleton_of_isCompact {X : Type u_1} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] {E : Type u_2} [TopologicalSpace E] {f : E → X} (hf : Continuous f) (hfC : Set.range f ⊆ C) {K : Set E} (hK : IsCompact K) : ∃ (q : ℤ), K ⊆ preimageSkeleton C f q

The skeletal filtration absorbs compact sets. If f is continuous with values in the complex C, every compact subset of E lies in the preimage of some skeleton, since its image is compact and so lies in a finite skeleton.