The relative small-chain theorem

Let P be a topological pair and U a family of subsets of its ambient space. The singular simplices of the ambient space whose image lies in a member of U form a subcomplex TopPair.smallSingularSubcomplex P U of the ambient simplicial set of the singular pair of P, to which the singular pair restricts. Its preimage in the singular simplicial set of the subspace is the small subcomplex of the subspace for the pulled-back family (TopPair.smallSingularSubcomplex_preimage_hom), and a map of pairs carries the simplices small for the pulled-back family into the simplices small for the family (TopPair.smallSingularSubcomplex_le_preimage).

The main result is the relative form of the small-chain theorem: when U is an open cover, the inclusion of the restricted pair induces isomorphisms on relative singular homology in every degree (TopPair.isIso_homologyMap_restrictι_smallSingularSubcomplex). It identifies the relative homology of a topological pair with that of its singular pair restricted to the simplices subordinate to any open cover of the ambient space, and is the input from the small-chain theorem to excision for relative singular homology.

References

• A. Hatcher, Algebraic Topology, Section 2.1, Proposition 2.21.

def TopPair.smallSingularSubcomplex (P : TopPair) {ι : Type u_1} (U : ι → Set ↑fst) : (toSSetPair.obj P).right.Subcomplex

The singular simplices of the ambient space of a topological pair whose image lies in a member of the family U, as a subcomplex of the ambient simplicial set of the singular pair of P. It is TopCat.smallSingularSubcomplex of the ambient space, typed so that the singular pair can be restricted to it.

Equations

• P.smallSingularSubcomplex U = TopPair.fst.smallSingularSubcomplex U

@[simp]

theorem TopPair.mem_smallSingularSubcomplex_iff (P : TopPair) {ι : Type u_1} (U : ι → Set ↑fst) {n : SimplexCategoryᵒᵖ} (σ : (toSSetPair.obj P).right.obj n) : σ ∈ (P.smallSingularSubcomplex U).obj n ↔ ∃ (i : ι), Set.range ⇑((fst.toSSetObjEquiv n) σ) ⊆ U i

theorem TopPair.smallSingularSubcomplex_preimage_hom (P : TopPair) {ι : Type u_1} (U : ι → Set ↑fst) : (P.smallSingularSubcomplex U).preimage (toSSetPair.obj P).hom = snd.smallSingularSubcomplex fun (i : ι) => ⇑(CategoryTheory.ConcreteCategory.hom map) ⁻¹' U i

The preimage of the small subcomplex of a pair in the singular simplicial set of its subspace is the small subcomplex of the subspace for the restricted family.

theorem TopPair.isIso_homologyMap_restrictι_smallSingularSubcomplex {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (P : TopPair) {ι : Type u_1} (U : ι → Set ↑fst) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) (n : ℕ) : CategoryTheory.IsIso (SSetPair.homologyMap ((toSSetPair.obj P).restrictι (P.smallSingularSubcomplex U)) R n)

The relative small-chain theorem. Restricting the singular pair of a topological pair to the simplices subordinate to an open cover of the ambient space does not change relative homology.

theorem TopPair.smallSingularSubcomplex_le_preimage {P : TopPair} {ι : Type u_1} {P' : TopPair} (f : P ⟶ P') (U : ι → Set ↑fst) : (P.smallSingularSubcomplex fun (i : ι) => ⇑(CategoryTheory.ConcreteCategory.hom (Hom.fst f)) ⁻¹' U i) ≤ (P'.smallSingularSubcomplex U).preimage (toSSetPair.map f).right

A map of pairs carries the simplices small for the pulled-back family into the simplices small for the family. This is TopCat.preimage_smallSingularSubcomplex at the pair-level types required to restrict the map of singular pairs (SSetPair.restrictMap).