Singular homology of a directed union

A singular simplex has compact image, so it lies in one member of any directed family of subspaces whose members absorb every compact subset. Consequently the singular simplicial set of a space is the filtered colimit of the singular simplicial sets of such a family, and, since the singular chain complex preserves colimits and homology commutes with exact filtered colimits, singular homology of the space is the colimit of the singular homology of the members. This is the "compact supports" property of singular homology.

The typical family is an increasing family of open subsets covering a space: a compact set is covered by finitely many of them, hence by one. For coefficients in modules, the colimit statement says that a class in the homology of a member which vanishes in the whole space already vanishes in some larger member. This is the compactness step in the computation of the homology of the complement of an embedded cube or sphere (TauCeti/AlgebraicTopology/Singular/CubeComplement).

Main definitions and results

• TauCeti.isColimitMapCoconeToSSet: for a cocone over a filtered diagram of spaces whose legs are embeddings, such that every compact subset of the apex lies in the range of a leg, the singular simplicial sets form a colimit cocone.
• TauCeti.isColimitMapCoconeSingularHomology: the same cocone is a colimit cocone after applying singular homology, for coefficients in an abelian category whose filtered colimits are exact.
• TauCeti.exists_singularHomologyMap_inclusion_eq_zero: with coefficients in a module, a class of one member of an increasing cover of a subspace by relatively open sets that vanishes in the subspace already vanishes in some larger member.

References

• A. Hatcher, Algebraic Topology, Section 2.1, Proposition 2.6 and the compactness argument in the proof of Proposition 2B.1.

noncomputable def TauCeti.isColimitMapCoconeToSSet {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone F) [CategoryTheory.IsFiltered J] (hc : ∀ (j : J), Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) (hK : ∀ (K : Set ↑c.pt), IsCompact K → ∃ (j : J), K ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) : CategoryTheory.Limits.IsColimit (TopCat.toSSet.mapCocone c)

Singular simplices have compact support. Let c be a cocone over a filtered diagram of spaces whose legs are embeddings, such that every compact subset of the apex lies in the range of some leg. Then the singular simplicial sets of the diagram form a colimit cocone with apex the singular simplicial set of c.pt.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.isColimitMapCoconeSingularHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (n : ℕ) {J : Type u_1} [CategoryTheory.Category.{u_1, u_1} J] [CategoryTheory.IsFiltered J] [CategoryTheory.Limits.HasColimitsOfShape J (Type w)] [CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone F) (hc : ∀ (j : J), Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) (hK : ∀ (K : Set ↑c.pt), IsCompact K → ∃ (j : J), K ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) : CategoryTheory.Limits.IsColimit (((AlgebraicTopology.singularHomologyFunctor C n).obj R).mapCocone c)

Singular homology has compact supports. For a cocone over a filtered diagram of spaces whose legs are embeddings, such that every compact subset of the apex lies in the range of some leg, singular homology of the apex is the colimit of singular homology of the diagram, provided filtered colimits of the coefficient category are exact.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.exists_singularHomologyMap_inclusion_eq_zero {A : Type w} [Ring A] (M : ModuleCat A) (n : ℕ) {Y : TopCat} {J : Type} [Preorder J] [IsDirected J fun (x1 x2 : J) => x1 ≤ x2] [Nonempty J] {U : J → Set ↑Y} (hU : Monotone U) {V : Set ↑Y} (hUV : ∀ (j : J), U j ⊆ V) (hopen : ∀ (j : J), IsOpen (Subtype.val ⁻¹' U j)) (hcover : V ⊆ ⋃ (j : J), U j) {i : J} (x : ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat A) n).obj M).obj ↧↑(U i))) (hx : (CategoryTheory.ConcreteCategory.hom (((AlgebraicTopology.singularHomologyFunctor (ModuleCat A) n).obj M).map (TopCat.ofHom (ContinuousMap.inclusion ⋯)))) x = 0) : ∃ (j : J) (hij : i ≤ j), (CategoryTheory.ConcreteCategory.hom (((AlgebraicTopology.singularHomologyFunctor (ModuleCat A) n).obj M).map (TopCat.ofHom (ContinuousMap.inclusion ⋯)))) x = 0

Vanishing of a homology class is detected in a member of an increasing open cover. With coefficients in a module, a singular homology class of one member U i of an increasing cover of V by subsets open in V that vanishes in V already vanishes in some larger member U j.