Chains subordinate to a cover are a deformation retract of all singular chains

For an open cover U of a space X, the singular chains subordinate to U — those supported on simplices whose image lies in a single member of U — include into all singular chains by a chain homotopy equivalence. This is the small-chain theorem, the analytic heart of excision: it lets every singular chain be replaced, without changing its homology class, by one assembled from simplices small enough to be seen inside a single member of the cover.

The construction is Hatcher's. Barycentric subdivision S is chain homotopic to the identity through the prism operator P, so the m-fold subdivision Sᵐ is chain homotopic to the identity through ∑_{k < m} Sᵏ ≫ P. A singular simplex σ becomes subordinate to U after enough subdivisions; taking for each σ a number singularSubdivisionDepth of subdivisions that works simultaneously for σ and all of its iterated faces produces a chain-homotopy operator D whose associated map ρ = 1 - ∂D - D∂ is a chain map landing in the chains subordinate to U. Since D vanishes on subordinate simplices, ρ restricts to the identity there, so the inclusion is a deformation retract in the chain-level sense: it has a strict retraction which is a homotopy inverse.

The number of subdivisions depends on the simplex, so ρ and the resulting retraction are not natural in the space. The inclusion itself is natural, hence so is the induced isomorphism smallSingularHomologyIso on homology.

Main definitions and results

• TauCeti.smallSingularChains: the subgroup of singular chains factoring through the chains subordinate to U.
• TauCeti.singularSubdivisionDepth: a number of barycentric subdivisions making a singular simplex and all of its iterated faces subordinate to U, monotone under passing to a face.
• TauCeti.singularSmallApprox: the chain endomorphism ρ, with TauCeti.singularSmallApproxHomotopy the chain homotopy to the identity and TauCeti.mem_smallSingularChains_ιChainComplex_comp_singularSmallApprox the statement that it lands in the chains subordinate to U.
• TauCeti.smallSingularRetraction: the resulting retraction of singular chains onto the chains subordinate to U.
• TauCeti.smallSingularChainHomotopyEquiv: the small-chain inclusion is a chain homotopy equivalence, and TauCeti.smallSingularHomologyIso the induced isomorphism on homology.

References

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

theorem TauCeti.instMonoFNatChainComplexMapιSmallSingularSubcomplex_1 {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) (n : ℕ) : CategoryTheory.Mono ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n)

noncomputable def TauCeti.smallSingularChains {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) (n : ℕ) : AddSubgroup (R ⟶ ((TopCat.toSSet.obj X).chainComplex R).X n)

The subgroup of the singular n-chains of X with coefficients in R consisting of the chains that factor through the chains subordinate to the family U.

Equations

• TauCeti.smallSingularChains R U n = (CategoryTheory.Preadditive.rightComp R ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n)).range

theorem TauCeti.mem_smallSingularChains_iff {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} {n : ℕ} (f : R ⟶ ((TopCat.toSSet.obj X).chainComplex R).X n) : f ∈ smallSingularChains R U n ↔ ∃ (g : R ⟶ ((X.smallSingularSubcomplex U).toSSet.chainComplex R).X n), CategoryTheory.CategoryStruct.comp g ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n) = f

theorem TauCeti.ιChainComplex_mem_smallSingularChains {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} {n : ℕ} (σ : (X.smallSingularSubcomplex U).toSSet.obj (Opposite.op { len := n })) : (TopCat.toSSet.obj X).ιChainComplex ↑σ ∈ smallSingularChains R U n

The summand of a simplex subordinate to U is a chain subordinate to U.

theorem TauCeti.smallSingularChains.comp_singularPrismX {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} {n : ℕ} {f : R ⟶ ((TopCat.toSSet.obj X).chainComplex R).X n} (hf : f ∈ smallSingularChains R U n) : CategoryTheory.CategoryStruct.comp f (singularPrismX R X n) ∈ smallSingularChains R U (n + 1)

The prism operator of barycentric subdivision preserves chains subordinate to U.

theorem TauCeti.smallSingularChains.comp_singularSubdivisionX {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} {n : ℕ} {f : R ⟶ ((TopCat.toSSet.obj X).chainComplex R).X n} (hf : f ∈ smallSingularChains R U n) : CategoryTheory.CategoryStruct.comp f (singularSubdivisionX R X n) ∈ smallSingularChains R U n

Barycentric subdivision preserves chains subordinate to U.

theorem TauCeti.smallSingularChains.comp_singularSubdivisionChainMap_pow_of_le {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} {n m m' : ℕ} (hm : m ≤ m') {f : R ⟶ ((TopCat.toSSet.obj X).chainComplex R).X n} (hf : CategoryTheory.CategoryStruct.comp f ((CategoryTheory.End.of (singularSubdivisionChainMap R X) ^ m).f n) ∈ smallSingularChains R U n) : CategoryTheory.CategoryStruct.comp f ((CategoryTheory.End.of (singularSubdivisionChainMap R X) ^ m').f n) ∈ smallSingularChains R U n

Once a chain has become subordinate to U after m subdivisions, it stays subordinate after any larger number of subdivisions.

noncomputable def TauCeti.singularSubdivisionOrder {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) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : ℕ

The least number of barycentric subdivisions after which a singular simplex becomes a chain subordinate to the family U.

Equations

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

theorem TauCeti.singularSubdivisionOrder_le {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) {n m : ℕ} {σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })} (hσ : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) ((CategoryTheory.End.of (singularSubdivisionChainMap R X) ^ m).f n) ∈ smallSingularChains R U n) : singularSubdivisionOrder R U σ ≤ m

The subdivision order is at most any number of subdivisions that makes the simplex subordinate to U.

theorem TauCeti.mem_smallSingularChains_ιChainComplex_comp_pow {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) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) {m : ℕ} (hm : singularSubdivisionOrder R U σ ≤ m) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) ((CategoryTheory.End.of (singularSubdivisionChainMap R X) ^ m).f n) ∈ smallSingularChains R U n

After singularSubdivisionOrder subdivisions, or any larger number, a singular simplex is a chain subordinate to the open cover U.

@[simp]

theorem TauCeti.singularSubdivisionOrder_eq_zero {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) {n : ℕ} {σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })} (hσ : σ ∈ (X.smallSingularSubcomplex U).obj (Opposite.op { len := n })) : singularSubdivisionOrder R U σ = 0

A simplex already subordinate to U needs no subdivision.

def TauCeti.singularSubdivisionDepth {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) (n : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : ℕ

The subdivision depth of a singular simplex: a number of barycentric subdivisions after which the simplex and all of its iterated faces are subordinate to the family U. Unlike the order, it is monotone under passing to a face, which is what makes the operator TauCeti.singularSmallApproxHom below land in the chains subordinate to U.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.singularSubdivisionDepth R U 0 σ_2 = TauCeti.singularSubdivisionOrder R U σ_2

theorem TauCeti.singularSubdivisionOrder_le_singularSubdivisionDepth {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) (n : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : singularSubdivisionOrder R U σ ≤ singularSubdivisionDepth R U n σ

theorem TauCeti.singularSubdivisionDepth_δ_le {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) (n : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n + 1 })) (j : Fin (n + 2)) : singularSubdivisionDepth R U n ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) j)) σ) ≤ singularSubdivisionDepth R U (n + 1) σ

@[simp]

theorem TauCeti.singularSubdivisionDepth_eq_zero {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) (n : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : σ ∈ (X.smallSingularSubcomplex U).obj (Opposite.op { len := n }) → singularSubdivisionDepth R U n σ = 0

The small-chain approximation

noncomputable def TauCeti.singularSmallApproxHom {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) (i j : ℕ) : ((TopCat.toSSet.obj X).chainComplex R).X i ⟶ ((TopCat.toSSet.obj X).chainComplex R).X j

The chain-homotopy operator of the small-chain approximation. On the summand of a singular simplex σ it is the iterated prism operator of the chain homotopy from the identity to the singularSubdivisionDepth-fold barycentric subdivision.

Equations

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

@[simp]

theorem TauCeti.ιChainComplex_singularSmallApproxHom {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) {i j : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := i })) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) (singularSmallApproxHom R U i j) = CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) (((singularSubdivisionHomotopy R X).idPow (singularSubdivisionDepth R U i σ)).hom i j)

@[simp]

theorem TauCeti.ιChainComplex_singularSmallApproxHom_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) {i j : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := i })) {Z : C} (h : ((TopCat.toSSet.obj X).chainComplex R).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp (singularSmallApproxHom R U i j) h) = CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp (((singularSubdivisionHomotopy R X).idPow (singularSubdivisionDepth R U i σ)).hom i j) h)

theorem TauCeti.singularSmallApproxHom_eq_zero {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) (i j : ℕ) (hij : ¬(ComplexShape.down ℕ).Rel j i) : singularSmallApproxHom R U i j = 0

noncomputable def TauCeti.singularSmallApprox {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) : (TopCat.toSSet.obj X).chainComplex R ⟶ (TopCat.toSSet.obj X).chainComplex R

The small-chain approximation of the singular chain complex: a chain endomorphism homotopic to the identity all of whose values are chains subordinate to U. It is Hatcher's operator ρ = 1 - ∂D - D∂, where D is TauCeti.singularSmallApproxHom.

Equations

• TauCeti.singularSmallApprox R U = CategoryTheory.CategoryStruct.id ((TopCat.toSSet.obj X).chainComplex R) - Homotopy.nullHomotopicMap (TauCeti.singularSmallApproxHom R U)

theorem TauCeti.singularSmallApprox_f {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) (n : ℕ) : (singularSmallApprox R U).f n = CategoryTheory.CategoryStruct.id (((TopCat.toSSet.obj X).chainComplex R).X n) - ((dNext n) (singularSmallApproxHom R U) + (prevD n) (singularSmallApproxHom R U))

noncomputable def TauCeti.singularSmallApproxHomotopy {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) : Homotopy (CategoryTheory.CategoryStruct.id ((TopCat.toSSet.obj X).chainComplex R)) (singularSmallApprox R U)

The small-chain approximation is chain homotopic to the identity.

Equations

• TauCeti.singularSmallApproxHomotopy R U = { hom := TauCeti.singularSmallApproxHom R U, zero := ⋯, comm := ⋯ }

theorem TauCeti.ι_comp_singularSmallApproxHom {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) (i j : ℕ) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f i) (singularSmallApproxHom R U i j) = 0

The approximation operator kills the chains that are already subordinate to U.

@[simp]

theorem TauCeti.ι_comp_singularSmallApprox {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) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) (singularSmallApprox R U) = SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R

The approximation restricts to the identity on the chains subordinate to U.

@[simp]

theorem TauCeti.ι_comp_singularSmallApprox_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) {Z : ChainComplex C ℕ} (h : (TopCat.toSSet.obj X).chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) (CategoryTheory.CategoryStruct.comp (singularSmallApprox R U) h) = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) h

The approximation restricts to the identity on the chains subordinate to U.

theorem TauCeti.mem_smallSingularChains_ιChainComplex_comp_idPow_hom_sub {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) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) {m m' : ℕ} (hm' : singularSubdivisionOrder R U σ ≤ m') (hmm : m' ≤ m) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) (((singularSubdivisionHomotopy R X).idPow m).hom n (n + 1) - ((singularSubdivisionHomotopy R X).idPow m').hom n (n + 1)) ∈ smallSingularChains R U (n + 1)

Enlarging the number of subdivisions in the iterated prism operator changes it by a chain subordinate to U, provided the simplex is already subordinate after the smaller number.

theorem TauCeti.mem_smallSingularChains_ιChainComplex_comp_singularSmallApprox {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) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) ((singularSmallApprox R U).f n) ∈ smallSingularChains R U n

The small-chain approximation lands in the chains subordinate to the cover.

The retraction onto the chains subordinate to the cover

noncomputable def TauCeti.smallSingularRetraction {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) : (TopCat.toSSet.obj X).chainComplex R ⟶ (X.smallSingularSubcomplex U).toSSet.chainComplex R

The retraction of singular chains onto the chains subordinate to an open cover.

Equations

• TauCeti.smallSingularRetraction R U hU hcov = { f := TauCeti.smallSingularRetractionX✝ R U hU hcov, comm' := ⋯ }

@[simp]

theorem TauCeti.smallSingularRetraction_comp_ι {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) : CategoryTheory.CategoryStruct.comp (smallSingularRetraction R U hU hcov) (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) = singularSmallApprox R U

@[simp]

theorem TauCeti.smallSingularRetraction_comp_ι_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) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) {Z : ChainComplex C ℕ} (h : (TopCat.toSSet.obj X).chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (smallSingularRetraction R U hU hcov) (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) h) = CategoryTheory.CategoryStruct.comp (singularSmallApprox R U) h

The inclusion is a chain homotopy equivalence

@[simp]

theorem TauCeti.ι_comp_smallSingularRetraction {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) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) (smallSingularRetraction R U hU hcov) = CategoryTheory.CategoryStruct.id ((X.smallSingularSubcomplex U).toSSet.chainComplex R)

@[simp]

theorem TauCeti.ι_comp_smallSingularRetraction_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) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) {Z : ChainComplex C ℕ} (h : (X.smallSingularSubcomplex U).toSSet.chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) (CategoryTheory.CategoryStruct.comp (smallSingularRetraction R U hU hcov) h) = h

noncomputable def TauCeti.smallSingularChainHomotopyEquiv {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) : HomotopyEquiv ((X.smallSingularSubcomplex U).toSSet.chainComplex R) ((TopCat.toSSet.obj X).chainComplex R)

Chains subordinate to an open cover are a deformation retract of all singular chains. The inclusion of the chains subordinate to an open cover U into the singular chain complex is a chain homotopy equivalence, whose homotopy inverse TauCeti.smallSingularRetraction is even a strict retraction.

Equations

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

noncomputable def TauCeti.smallSingularHomologyIso {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) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : HomologicalComplex.homology ((X.smallSingularSubcomplex U).toSSet.chainComplex R) n ≅ HomologicalComplex.homology ((TopCat.toSSet.obj X).chainComplex R) n

The isomorphism on homology induced by the inclusion of the chains subordinate to an open cover. Since the inclusion is natural in the covered space, so is this isomorphism, whereas the homotopy inverse underlying it is not.

Equations

• TauCeti.smallSingularHomologyIso R U hU hcov n = (TauCeti.smallSingularChainHomotopyEquiv R U hU hcov).toHomologyIso n

@[simp]

theorem TauCeti.smallSingularHomologyIso_hom {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) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : (smallSingularHomologyIso R U hU hcov n).hom = HomologicalComplex.homologyMap (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) n

theorem TauCeti.smallSingularHomologyIso_naturality {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) [CategoryTheory.CategoryWithHomology C] {κ : Type u_2} {Y : TopCat} (V : κ → Set ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i))) (hV : ∀ (j : κ), IsOpen (V j)) (hcovV : ⋃ (j : κ), V j = Set.univ) (n : ℕ) : CategoryTheory.CategoryStruct.comp (smallSingularHomologyIso R U hU hcov n).hom (HomologicalComplex.homologyMap (SSet.chainComplexMap (TopCat.toSSet.map f) R) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (SSet.chainComplexMap (TopCat.smallSingularSubcomplexMap U V f r hf) R) n) (smallSingularHomologyIso R V hV hcovV n).hom

The small-chain homology isomorphism is natural under maps carrying members of one cover into members of another.

theorem TauCeti.isIso_homologyMap_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) (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : CategoryTheory.IsIso (HomologicalComplex.homologyMap (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) n)

The inclusion of the chains subordinate to an open cover induces an isomorphism on homology in every degree.

theorem TauCeti.quasiIso_chainComplexMap_smallSingularSubcomplex_ι {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) [CategoryTheory.CategoryWithHomology C] : QuasiIso (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R)

The inclusion of the chains subordinate to an open cover is a quasi-isomorphism.