Singular chains subordinate to an open cover

A singular simplex is small for a family of subsets when its image is contained in one member of the family. Small simplices form a subcomplex of the singular simplicial set: every face and degeneracy of a small simplex is still small. Applying Mathlib's simplicial chain-complex functor therefore gives the complex of chains subordinate to the family, together with its canonical inclusion into singular chains.

For an open cover, sufficiently fine barycentric subdivision of each singular simplex factors through this inclusion. This is the chain-level smallness statement used to construct the small-chain equivalence and prove excision.

Main definitions and results

• TopCat.smallSingularSubcomplex: the subcomplex of singular simplices whose image lies in one member of a family of subsets.
• TopCat.smallSingularSubcomplexMap: a covered map restricts to the small subcomplexes.
• TopCat.preimage_smallSingularSubcomplex: the preimage of a small subcomplex along a map is the small subcomplex of the preimage family.
• TopCat.toSmallSingularSubcomplex: the singular simplicial set of a subset of a member of the family maps into the small subcomplex.
• TauCeti.AffineChain.smallSingularChain: push affine chains forward along a small simplex with values in the small-chain complex.
• TauCeti.AffineChain.exists_singularChain_small_factor: a pushed-forward affine chain supported on small simplices factors through the small-chain complex.
• TauCeti.exists_iterate_singularSubdivision_factor_small: a sufficiently fine subdivision of any singular simplex factors through the small-chain inclusion.

References

• A. Hatcher, Algebraic Topology, Section 2.1, proof of Proposition 2.21, step (4).

def TopCat.smallSingularSubcomplex (X : TopCat) {ι : Type u_1} (U : ι → Set ↑X) : (toSSet.obj X).Subcomplex

The subcomplex of the singular simplicial set consisting of the simplices whose image is contained in one member of the family U. No covering or openness hypothesis is needed for the definition.

Equations

• X.smallSingularSubcomplex U = { obj := fun (n : SimplexCategoryᵒᵖ) => {σ : (TopCat.toSSet.obj X).obj n | ∃ (i : ι), Set.range ⇑((X.toSSetObjEquiv n) σ) ⊆ U i}, map := ⋯ }

@[simp]

theorem TopCat.mem_smallSingularSubcomplex_iff (X : TopCat) {ι : Type u_1} (U : ι → Set ↑X) {n : SimplexCategoryᵒᵖ} (σ : (toSSet.obj X).obj n) : σ ∈ (X.smallSingularSubcomplex U).obj n ↔ ∃ (i : ι), Set.range ⇑((X.toSSetObjEquiv n) σ) ⊆ U i

noncomputable def TopCat.smallSingularSubcomplexMap {X : TopCat} {ι : Type u_1} {κ : Type u_2} {Y : TopCat} (U : ι → Set ↑X) (V : κ → Set ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i))) : (X.smallSingularSubcomplex U).toSSet ⟶ (Y.smallSingularSubcomplex V).toSSet

A map carrying each member of one family into a member of another restricts to a map of the corresponding small singular subcomplexes.

Equations

• TopCat.smallSingularSubcomplexMap U V f r hf = SSet.Subcomplex.lift (CategoryTheory.CategoryStruct.comp (X.smallSingularSubcomplex U).ι (TopCat.toSSet.map f)) ⋯

@[simp]

theorem TopCat.smallSingularSubcomplexMap_ι {X : TopCat} {ι : Type u_1} {κ : Type u_2} {Y : TopCat} (U : ι → Set ↑X) (V : κ → Set ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i))) : CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexMap U V f r hf) (Y.smallSingularSubcomplex V).ι = CategoryTheory.CategoryStruct.comp (X.smallSingularSubcomplex U).ι (toSSet.map f)

@[simp]

theorem TopCat.smallSingularSubcomplexMap_ι_assoc {X : TopCat} {ι : Type u_1} {κ : Type u_2} {Y : TopCat} (U : ι → Set ↑X) (V : κ → Set ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i))) {Z : SSet} (h : toSSet.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexMap U V f r hf) (CategoryTheory.CategoryStruct.comp (Y.smallSingularSubcomplex V).ι h) = CategoryTheory.CategoryStruct.comp (X.smallSingularSubcomplex U).ι (CategoryTheory.CategoryStruct.comp (toSSet.map f) h)

@[simp]

theorem TopCat.smallSingularSubcomplexMap_id {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) : smallSingularSubcomplexMap U U (CategoryTheory.CategoryStruct.id X) id ⋯ = CategoryTheory.CategoryStruct.id (X.smallSingularSubcomplex U).toSSet

@[simp]

theorem TopCat.preimage_smallSingularSubcomplex {X : TopCat} {ι : Type u_1} {Y : TopCat} (U : ι → Set ↑X) (f : Y ⟶ X) : (X.smallSingularSubcomplex U).preimage (toSSet.map f) = Y.smallSingularSubcomplex fun (i : ι) => ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' U i

The preimage of the small singular subcomplex of a family along a continuous map is the small singular subcomplex of the preimage family.

noncomputable def TopCat.toSmallSingularSubcomplex {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) {S : Set ↑X} {i : ι} (h : S ⊆ U i) : toSSet.obj ↧↑S ⟶ (X.smallSingularSubcomplex U).toSSet

The singular simplicial set of a subset S contained in a member U i of the family maps into the small singular subcomplex of the family: every singular simplex of S is small.

Equations

• TopCat.toSmallSingularSubcomplex U h = SSet.Subcomplex.lift (TopCat.toSSet.map (TopCat.ofHom (ContinuousMap.subtypeVal S))) ⋯

@[simp]

theorem TopCat.toSmallSingularSubcomplex_ι {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) {S : Set ↑X} {i : ι} (h : S ⊆ U i) : CategoryTheory.CategoryStruct.comp (toSmallSingularSubcomplex U h) (X.smallSingularSubcomplex U).ι = toSSet.map (ofHom (ContinuousMap.subtypeVal S))

@[simp]

theorem TopCat.toSmallSingularSubcomplex_ι_assoc {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) {S : Set ↑X} {i : ι} (h : S ⊆ U i) {Z : SSet} (h✝ : toSSet.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (toSmallSingularSubcomplex U h) (CategoryTheory.CategoryStruct.comp (X.smallSingularSubcomplex U).ι h✝) = CategoryTheory.CategoryStruct.comp (toSSet.map (ofHom (ContinuousMap.subtypeVal S))) h✝

@[simp]

theorem TopCat.toSmallSingularSubcomplex_app_coe {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) {S : Set ↑X} {i : ι} (h : S ⊆ U i) {n : SimplexCategoryᵒᵖ} (σ : (toSSet.obj ↧↑S).obj n) : ↑((CategoryTheory.ConcreteCategory.hom ((toSmallSingularSubcomplex U h).app n)) σ) = (CategoryTheory.ConcreteCategory.hom ((toSSet.map (ofHom (ContinuousMap.subtypeVal S))).app n)) σ

theorem TopCat.smallSingularSubcomplexMap_comp {X : TopCat} {ι : Type u_1} {κ : Type u_2} {Y : TopCat} (U : ι → Set ↑X) (V : κ → Set ↑Y) {μ : Type u_3} {Z : TopCat} (W : μ → Set ↑Z) (f : X ⟶ Y) (g : Y ⟶ Z) (r : ι → κ) (s : κ → μ) (hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i))) (hg : ∀ (j : κ), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) (V j) (W (s j))) : smallSingularSubcomplexMap U W (CategoryTheory.CategoryStruct.comp f g) (s ∘ r) ⋯ = CategoryTheory.CategoryStruct.comp (smallSingularSubcomplexMap U V f r hf) (smallSingularSubcomplexMap V W g s hg)

Restriction of covered maps to small singular subcomplexes respects composition.

theorem TauCeti.AffineChain.exists_singularChain_small_factor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) {m k : ℕ} (σ : C(Convexity.StdSimplex ℝ (Fin (m + 1)), ↑X)) (c : (Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) (hc : ∀ v ∈ c.support, ∃ (i : ι), Set.range ⇑(σ.comp (Convexity.StdSimplex.continuousAffineMapMk v)) ⊆ U i) : ∃ (f : R ⟶ ((X.smallSingularSubcomplex U).toSSet.chainComplex R).X k), CategoryTheory.CategoryStruct.comp f ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f k) = (singularChain R σ k) c

Pushing forward an affine chain supported on simplices subordinate to U factors through the chain complex of the small singular subcomplex.

noncomputable def TauCeti.AffineChain.smallSingularChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) {m : ℕ} (σ : (X.smallSingularSubcomplex U).toSSet.obj (Opposite.op { len := m })) (k : ℕ) : ((Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) →ₗ[ℤ] R ⟶ ((X.smallSingularSubcomplex U).toSSet.chainComplex R).X k

Push an affine chain forward along a small singular simplex, with values in the small-chain complex. Every resulting simplex has image inside the original simplex.

Equations

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

@[simp]

theorem TauCeti.AffineChain.smallSingularChain_single {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) {m k : ℕ} (σ : (X.smallSingularSubcomplex U).toSSet.obj (Opposite.op { len := m })) (v : Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) (a : ℤ) : (smallSingularChain R U σ k) (Finsupp.single v a) = a • (X.smallSingularSubcomplex U).toSSet.ιChainComplex ⟨(X.toSSetObjEquiv (Opposite.op { len := k })).symm (((X.toSSetObjEquiv (Opposite.op { len := m })) ↑σ).comp (Convexity.StdSimplex.continuousAffineMapMk v)), ⋯⟩

@[simp]

theorem TauCeti.AffineChain.smallSingularChain_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) {m k : ℕ} (σ : (X.smallSingularSubcomplex U).toSSet.obj (Opposite.op { len := m })) (c : (Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) : CategoryTheory.CategoryStruct.comp ((smallSingularChain R U σ k) c) ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f k) = (singularChain R ((X.toSSetObjEquiv (Opposite.op { len := m })) ↑σ) k) c

The small-chain push-forward agrees with the ordinary push-forward after inclusion.

@[simp]

theorem TauCeti.AffineChain.smallSingularChain_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) {m k : ℕ} (σ : (X.smallSingularSubcomplex U).toSSet.obj (Opposite.op { len := m })) (c : (Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) {Z : C} (h : ((TopCat.toSSet.obj X).chainComplex R).X k ⟶ Z) : CategoryTheory.CategoryStruct.comp ((smallSingularChain R U σ k) c) (CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f k) h) = CategoryTheory.CategoryStruct.comp ((singularChain R ((X.toSSetObjEquiv (Opposite.op { len := m })) ↑σ) k) c) h

The small-chain push-forward agrees with the ordinary push-forward after inclusion.

theorem TauCeti.exists_iterate_singularSubdivision_factor_small {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {X : TopCat} {ι : Type u_1} (U : ι → Set ↑X) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) {k : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := k })) : ∃ (n₀ : ℕ), ∀ n ≥ n₀, ∃ (f : R ⟶ ((X.smallSingularSubcomplex U).toSSet.chainComplex R).X k), CategoryTheory.CategoryStruct.comp f ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f k) = CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) ((CategoryTheory.End.of (singularSubdivisionChainMap R X) ^ n).f k)

For an open cover, a sufficiently fine iterated barycentric subdivision of every singular simplex factors through the inclusion of the complex of chains subordinate to the cover.