@[reducible, inline]

abbrev CWComplex.cellularChains (X : Type u_1) [TopologicalSpace X] [Topology.CWComplex Set.univ] (n : ℕ) : Type u_1

Definition 16.1. The group of cellular n-chains of a CW complex X, defined as the free abelian group on the set of n-cells of X.

noncomputable def CWComplex.RelativeSingularHomology (Y : Type u_2) [TopologicalSpace Y] (A B : Set Y) (n : ℕ) : Type

The relative singular homology group H_n(A, B) for two subsets A, B ⊆ Y of a topological space Y.

noncomputable def CWComplex.RelativeSingularHomology.addCommGroup (Y : Type u_2) [TopologicalSpace Y] (A B : Set Y) (n : ℕ) : AddCommGroup (RelativeSingularHomology Y A B n)

The abelian group structure on the relative singular homology group H_n(A, B).

@[implicit_reducible]

noncomputable instance CWComplex.instAddCommGroupRelativeSingularHomology (Y : Type u_2) [TopologicalSpace Y] (A B : Set Y) (n : ℕ) : AddCommGroup (RelativeSingularHomology Y A B n)

The abelian group instance on the relative singular homology group H_n(A, B).

noncomputable def CWComplex.prevSkeleton (X : Type u_1) [TopologicalSpace X] [Topology.CWComplex Set.univ] [T2Space X] (n : ℕ) : Set X

The previous skeleton X_{n-1} for n ≥ 1, and the empty set for n = 0. Convenient shorthand used for forming the CW-pair (X_n, X_{n-1}).

noncomputable def CWComplex.cellularChains_eq_relativeSingularHomology (X : Type u_2) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : RelativeSingularHomology X (↑(skeleton X ↑n)) (prevSkeleton X n) n ≃+ cellularChains X n

The cellular chain group C_n(X) is isomorphic to the relative singular homology H_n(X_n, X_{n-1}) of the CW-pair (Definition 16.1 of Miller).

def CWComplex.SkeletonHomology.skeletonInclusion (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k : ℕ) : TopCat.of ↑↑(skeleton X ↑k) ⟶ TopCat.of X

The continuous inclusion of the k-skeleton X_k ↪ X, viewed as a morphism in TopCat.

noncomputable def CWComplex.SkeletonHomology.skeletonHomologyMap (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) : AlgebraicTopologyI.SingularHomologyGroup q ↑↑(skeleton X ↑k) ⟶ AlgebraicTopologyI.SingularHomologyGroup q X

The map on singular homology H_q(X_k) → H_q(X) induced by the inclusion of the k-skeleton.

def CWComplex.SkeletonHomology.skeletonStepInclusion (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k : ℕ) : TopCat.of ↑↑(skeleton X ↑k) ⟶ TopCat.of ↑↑(skeleton X (↑k + 1))

The one-step skeleton inclusion X_k ↪ X_{k+1}, viewed as a morphism in TopCat.

noncomputable def CWComplex.SkeletonHomology.skeletonStepHomologyMap (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) : AlgebraicTopologyI.SingularHomologyGroup q ↑↑(skeleton X ↑k) ⟶ AlgebraicTopologyI.SingularHomologyGroup q ↑↑(skeleton X (↑k + 1))

The map on singular homology H_q(X_k) → H_q(X_{k+1}) induced by the one-step skeleton inclusion.

theorem CWComplex.SkeletonHomology.skeletonInclusion_factor (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k : ℕ) : skeletonInclusion X k = CategoryTheory.CategoryStruct.comp (skeletonStepInclusion X k) (skeletonInclusion X (k + 1))

The inclusion X_k ↪ X factors through the one-step inclusion X_k ↪ X_{k+1}.

theorem CWComplex.SkeletonHomology.skeletonHomologyMap_factor (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) : skeletonHomologyMap X q k = CategoryTheory.CategoryStruct.comp (skeletonStepHomologyMap X q k) (skeletonHomologyMap X q (k + 1))

Functoriality: the homology map H_q(X_k) → H_q(X) factors through H_q(X_{k+1}).

theorem CWComplex.SkeletonHomology.skeleton_zero_inter_openCell_empty {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] {n : ℕ} (hn : n ≥ 1) (j : Topology.RelCWComplex.cell Set.univ n) : ↑(skeleton X 0) ∩ Topology.RelCWComplex.openCell n j = ∅

The 0-skeleton is disjoint from any open cell of positive dimension.

theorem CWComplex.SkeletonHomology.skeleton_zero_inter_closedCell_finite {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) (j : Topology.RelCWComplex.cell Set.univ n) : (↑(skeleton X 0) ∩ Topology.RelCWComplex.closedCell n j).Finite

The intersection of the 0-skeleton with any closed cell of X is a finite set.

theorem CWComplex.SkeletonHomology.isClosed_subset_skeleton_zero {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (A : Set X) (hA : A ⊆ ↑(skeleton X 0)) : IsClosed A

Every subset of the 0-skeleton of a CW complex is closed in X (the 0-skeleton inherits the discrete topology).

theorem CWComplex.SkeletonHomology.skeleton_zero_totallyDisconnected {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] : TotallyDisconnectedSpace ↑↑(skeleton X 0)

The 0-skeleton of a CW complex is totally disconnected (in fact, discrete).

theorem CWComplex.SkeletonHomology.excision_CW_pair_vanishing {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q n : ℕ) : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup q (SphereHomology.Disk n) (SphereHomology.diskBoundarySubset n)) → CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup q (↑↑(skeleton X ↑n)) (Subtype.val ⁻¹' ↑(skeleton X (↑n - 1))))

Excision input: vanishing of the relative homology of the disk pair (D^n, S^{n-1}) implies the analogous vanishing for the CW pair (X_n, X_{n-1}).

theorem CWComplex.SkeletonHomology.relativeHomology_CW_pair_isZero {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) (hqk : q ≠ k + 1) : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup q (↑↑(skeleton X (↑k + 1))) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))

For q ≠ k+1, the relative homology H_q(X_{k+1}, X_k) vanishes. This is the key input to the cellular-vs-singular homology comparison.

theorem CWComplex.SkeletonHomology.les_pair_isZero {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) (hk : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q ↑↑(skeleton X ↑k))) (hrel : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup q (↑↑(skeleton X (↑k + 1))) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))) : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q ↑↑(skeleton X (↑k + 1)))

Long exact sequence argument: if both H_q(X_k) = 0 and the relative homology H_q(X_{k+1}, X_k) = 0, then H_q(X_{k+1}) = 0.

theorem CWComplex.SkeletonHomology.singularHomology_skeleton_succ_isZero_of_isZero {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) (hkq : k + 1 < q) (hk : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q ↑↑(skeleton X ↑k))) : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q ↑↑(skeleton X (↑k + 1)))

Inductive step: if H_q(X_k) = 0 and k+1 < q, then H_q(X_{k+1}) = 0.

theorem CWComplex.SkeletonHomology.singularHomology_skeleton_isZero {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) (hkq : k < q) : CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q ↑↑(skeleton X ↑k))

Proposition 16.2 (first half). If k < q, then H_q(X_k) = 0.

theorem CWComplex.SkeletonHomology.skeletonStepHomologyMap_isIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) (hkq : q + 1 ≤ k) : CategoryTheory.IsIso (skeletonStepHomologyMap X q k)

When q + 1 ≤ k, the homology map H_q(X_k) → H_q(X_{k+1}) induced by the one-step skeleton inclusion is an isomorphism.

def CWComplex.SkeletonHomology.skeletonPreimageHomeo {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (m : ℕ) : ↑(Subtype.val ⁻¹' ↑(skeleton X ↑m)) ≃ₜ ↑↑(skeleton X ↑m)

The preimage of X_m under the inclusion X_{m+1} ↪ X is homeomorphic to X_m.

def CWComplex.SkeletonHomology.skeletonPreimageIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (m : ℕ) : TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑m)) ≅ TopCat.of ↑↑(skeleton X ↑m)

The TopCat-isomorphism corresponding to skeletonPreimageHomeo.

def CWComplex.SkeletonHomology.skeletonPreimageInclusion {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k)) ⟶ TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑m))

For k ≤ m, the inclusion of preimages: viewing X_k and X_m as subsets of X_{m+1}, the inclusion (X_k \text{ in } X_{m+1}) ↪ (X_m \text{ in } X_{m+1}).

theorem CWComplex.SkeletonHomology.subspaceTopInclusion_factor {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : Excision.subspaceTopInclusion (Subtype.val ⁻¹' ↑(skeleton X ↑k)) = CategoryTheory.CategoryStruct.comp (skeletonPreimageInclusion k m hkm) (Excision.subspaceTopInclusion (Subtype.val ⁻¹' ↑(skeleton X ↑m)))

Factorisation of subspace inclusions: the inclusion of the preimage of X_k factors through the preimage of X_m whenever k ≤ m.

theorem CWComplex.SkeletonHomology.subspaceChainInclusion_factor {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : Excision.subspaceChainInclusion (↑↑(skeleton X (↑m + 1))) (Subtype.val ⁻¹' ↑(skeleton X ↑k)) = CategoryTheory.CategoryStruct.comp (Excision.singularChainZ.map (skeletonPreimageInclusion k m hkm)) (Excision.subspaceChainInclusion (↑↑(skeleton X (↑m + 1))) (Subtype.val ⁻¹' ↑(skeleton X ↑m)))

Singular-chain version of subspaceTopInclusion_factor: the chain-inclusion factors through the analogous chain-inclusion for the intermediate skeleton.

def CWComplex.SkeletonHomology.skeletonPreimageSubHomeo {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : ↑(Subtype.val ⁻¹' (Subtype.val ⁻¹' ↑(skeleton X ↑k))) ≃ₜ ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k))

The preimage-of-a-preimage homeomorphism identifying the nested preimage of X_k inside X_m ⊆ X_{m+1} with the direct preimage of X_k inside X_m.

def CWComplex.SkeletonHomology.skeletonPreimageSubIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : TopCat.of ↑(Subtype.val ⁻¹' (Subtype.val ⁻¹' ↑(skeleton X ↑k))) ≅ TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k))

The TopCat-iso corresponding to skeletonPreimageSubHomeo.

noncomputable def CWComplex.SkeletonHomology.skeletonPreimageChainIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (m : ℕ) : Excision.singularChainZ.obj (TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑m))) ≅ Excision.singularChainZ.obj (TopCat.of ↑↑(skeleton X ↑m))

The induced isomorphism between singular chain complexes corresponding to skeletonPreimageIso.

noncomputable def CWComplex.SkeletonHomology.skeletonPreimageSubChainIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : Excision.singularChainZ.obj (TopCat.of ↑(Subtype.val ⁻¹' (Subtype.val ⁻¹' ↑(skeleton X ↑k)))) ≅ Excision.singularChainZ.obj (TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k)))

The induced isomorphism between singular chain complexes corresponding to skeletonPreimageSubIso.

noncomputable def CWComplex.SkeletonHomology.skeletonPreimageHomologyIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n m : ℕ) : HomologicalComplex.homology (Excision.singularChainZ.obj (TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑m)))) n ≅ AlgebraicTopologyI.SingularHomologyGroup n ↑↑(skeleton X ↑m)

The induced isomorphism on singular homology corresponding to skeletonPreimageIso.

def CWComplex.SkeletonHomology.skeletonPreimageAkHomeo {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k)) ≃ₜ ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k))

The homeomorphism between two presentations of X_k as a subspace: as the preimage of X_k inside X_{m+1} and as the preimage of X_k inside X_m.

def CWComplex.SkeletonHomology.skeletonPreimageAkIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k)) ≅ TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k))

The TopCat-iso corresponding to skeletonPreimageAkHomeo.

noncomputable def CWComplex.SkeletonHomology.skeletonPreimageAkChainIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : Excision.singularChainZ.obj (TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k))) ≅ Excision.singularChainZ.obj (TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k)))

The induced isomorphism between singular chain complexes corresponding to skeletonPreimageAkIso.

theorem CWComplex.SkeletonHomology.skeletonPreimageInclusion_comm {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) (hkm : k ≤ m) : CategoryTheory.CategoryStruct.comp (Excision.singularChainZ.map (skeletonPreimageInclusion k m hkm)) (skeletonPreimageChainIso m).hom = CategoryTheory.CategoryStruct.comp (skeletonPreimageAkChainIso k m hkm).hom (Excision.subspaceChainInclusion (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))

Commutativity of the square relating the preimage inclusion to the subspace chain inclusion through the relevant chain isomorphisms.

theorem CWComplex.SkeletonHomology.triple_exact {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n k m : ℕ) (hkm : k ≤ m) : ∃ (S : CategoryTheory.ShortComplex AddCommGrpCat), S.X₁ = Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)) ∧ S.X₂ = Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X (↑m + 1))) (Subtype.val ⁻¹' ↑(skeleton X ↑k)) ∧ S.X₃ = Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X (↑m + 1))) (Subtype.val ⁻¹' ↑(skeleton X ↑m)) ∧ S.Exact

The exact sequence of the triple (X_{m+1}, X_m, X_k): there is an exact short complex relating the three relative homology groups H_n(X_m, X_k) → H_n(X_{m+1}, X_k) → H_n(X_{m+1}, X_m).

theorem CWComplex.SkeletonHomology.relativeHomology_triple_step {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n k m : ℕ) (hkm : k ≤ m) (h_step : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X (↑m + 1))) (Subtype.val ⁻¹' ↑(skeleton X ↑m)))) (h_prev : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))) (_h_prev_lo : ∀ (j : ℕ), (ComplexShape.down ℕ).Rel n j → CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup j (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))) : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X (↑m + 1))) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))

One inductive step using the triple long exact sequence: if both H_n(X_{m+1}, X_m) and H_n(X_m, X_k) vanish, then so does H_n(X_{m+1}, X_k).

theorem CWComplex.SkeletonHomology.relativeHomology_self_isZero {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n k : ℕ) : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X ↑k)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))

The relative homology of a pair with itself, H_n(X_k, X_k), vanishes.

@[irreducible]

theorem CWComplex.SkeletonHomology.relativeHomology_finiteSkeleton_isZero {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n k m : ℕ) (hnk : n ≤ k) (hkm : k ≤ m) : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))

For n ≤ k ≤ m, the relative homology H_n(X_m, X_k) = 0. Proved by induction on the gap m - k using the triple exact sequence.

def CWComplex.SkeletonHomology.skelPairSubspaceMap {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) : TopCat.of ↑(Subtype.val ⁻¹' ↑(skeleton X ↑k)) ⟶ TopCat.of ↑↑(skeleton X ↑k)

The continuous map sending a point of the preimage of X_k inside X_m to the corresponding point of X_k ⊆ X.

theorem CWComplex.SkeletonHomology.skelPairSquare_comm {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) : CategoryTheory.CategoryStruct.comp (Excision.subspaceTopInclusion (Subtype.val ⁻¹' ↑(skeleton X ↑k))) (skeletonInclusion X m) = CategoryTheory.CategoryStruct.comp (skelPairSubspaceMap k m) (Excision.subspaceTopInclusion ↑(skeleton X ↑k))

Commutativity of the natural square for the pair maps: the subspace inclusion of X_k (as a preimage in X_m) into X_m, then into X, equals the composition through X_k ⊆ X.

noncomputable def CWComplex.SkeletonHomology.skelPairRelativeChainMap {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (k m : ℕ) : Excision.relativeSingularChainComplex (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)) ⟶ Excision.relativeSingularChainComplex X ↑(skeleton X ↑k)

The induced map of relative singular chain complexes from the pair (X_m, X_k) to the pair (X, X_k).

noncomputable def CWComplex.SkeletonHomology.skelPairHomologyMap {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n k m : ℕ) : Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)) ⟶ Excision.RelativeSingularHomologyGroup n X ↑(skeleton X ↑k)

The induced map on relative singular homology H_n(X_m, X_k) → H_n(X, X_k).

theorem CWComplex.SkeletonHomology.skelPairCyclesMap_jointly_surjective {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n k : ℕ) (z : ↑(HomologicalComplex.cycles (Excision.relativeSingularChainComplex X ↑(skeleton X ↑k)) n)) : ∃ (m : ℕ) (_ : k ≤ m) (z' : ↑(HomologicalComplex.cycles (Excision.relativeSingularChainComplex (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k))) n)), (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.cyclesMap (skelPairRelativeChainMap k m) n)) z' = z

Every relative cycle of the pair (X, X_k) lifts to a relative cycle of some pair (X_m, X_k) with k ≤ m, since singular chains are supported on compact (hence finite-skeleton) subsets.

theorem CWComplex.SkeletonHomology.skelPairHomologyMap_jointly_surjective {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n k : ℕ) (x : ↑(Excision.RelativeSingularHomologyGroup n X ↑(skeleton X ↑k))) : ∃ (m : ℕ) (_ : k ≤ m) (y : ↑(Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))), (CategoryTheory.ConcreteCategory.hom (skelPairHomologyMap n k m)) y = x

Every class in H_n(X, X_k) is the image of a class in some H_n(X_m, X_k) for k ≤ m.

theorem CWComplex.SkeletonHomology.relativeHomology_colimit_passage {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n k : ℕ) (h : ∀ (m : ℕ), k ≤ m → CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup n (↑↑(skeleton X ↑m)) (Subtype.val ⁻¹' ↑(skeleton X ↑k)))) : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup n X ↑(skeleton X ↑k))

Colimit passage: if H_n(X_m, X_k) = 0 for all m ≥ k, then H_n(X, X_k) = 0.

theorem CWComplex.SkeletonHomology.relativeHomology_skeleton_isZero {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n k : ℕ) (hnk : n ≤ k) : CategoryTheory.Limits.IsZero (Excision.RelativeSingularHomologyGroup n X ↑(skeleton X ↑k))

For n ≤ k, the relative homology H_n(X, X_k) vanishes.

theorem CWComplex.SkeletonHomology.skeletonHomologyMap_base_isIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q : ℕ) : CategoryTheory.IsIso (skeletonHomologyMap X q (q + 1))

Base case of Proposition 16.2 (second half): the map H_q(X_{q+1}) → H_q(X) is an isomorphism.

theorem CWComplex.SkeletonHomology.skeletonHomologyMap_isIso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) (hkq : q < k) : CategoryTheory.IsIso (skeletonHomologyMap X q k)

Proposition 16.2 (second half). For q < k, the inclusion-induced map H_q(X_k) → H_q(X) is an isomorphism.

theorem CWComplex.SkeletonHomology.skeleton_homology_properties {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (q k : ℕ) : (k < q → CategoryTheory.Limits.IsZero (AlgebraicTopologyI.SingularHomologyGroup q ↑↑(skeleton X ↑k))) ∧ (q < k → CategoryTheory.IsIso (skeletonHomologyMap X q k))

Proposition 16.2. Combined statement: H_q(X_k) = 0 for k < q, and the inclusion induces an isomorphism H_q(X_k) → H_q(X) for k > q.

noncomputable def CWHomology.cellularChainObj (X : Type u_1) [TopologicalSpace X] [Topology.CWComplex Set.univ] (n : ℕ) : AddCommGrpCat

The cellular chain group C_n(X) packaged as an object of the category AddCommGrpCat.

noncomputable def CWHomology.relHomologySkeleton (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n q : ℕ) : AddCommGrpCat

The relative singular homology H_q(X_n, X_{n-1}) of the CW pair, packaged as an object of AddCommGrpCat.

noncomputable def CWHomology.skeletonHomology (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n q : ℕ) : AddCommGrpCat

The singular homology H_q(X_n) of the n-skeleton, packaged as an object of AddCommGrpCat.

noncomputable def CWHomology.excision_CW_pair_finsupp_equiv {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : ↑(relHomologySkeleton X n n) ≃+ (Topology.CWComplex.cell Set.univ n →₀ ℤ)

Excision-based identification: the relative homology H_n(X_n, X_{n-1}) is isomorphic to the finsupp cell n →₀ ℤ, exhibiting it as the free abelian group on the set of n-cells.

noncomputable def CWHomology.excision_CW_pair_quotient_iso {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : relHomologySkeleton X n n ≅ cellularChainObj X n

Categorical isomorphism H_n(X_n, X_{n-1}) ≅ C_n(X) obtained from excision_CW_pair_finsupp_equiv and the equivalence between finsupps and free abelian groups.

noncomputable def CWHomology.excision_CW_pair_freeAbelianGroup {X : Type} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : ↑(relHomologySkeleton X n n) ≃+ FreeAbelianGroup (Topology.CWComplex.cell Set.univ n)

Additive-equivalence form of excision_CW_pair_quotient_iso: identification of H_n(X_n, X_{n-1}) with the free abelian group on the set of n-cells.

noncomputable def CWHomology.cellularChainIso (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : cellularChainObj X n ≅ relHomologySkeleton X n n

Categorical isomorphism C_n(X) ≅ H_n(X_n, X_{n-1}) (the inverse of excision_CW_pair_quotient_iso).

noncomputable def CWHomology.skeletonConnectingHom (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : relHomologySkeleton X (n + 1) (n + 1) ⟶ skeletonHomology X n n

The connecting homomorphism H_{n+1}(X_{n+1}, X_n) → H_n(X_n) arising from the short exact sequence of the pair (X_{n+1}, X_n).

noncomputable def CWHomology.skeletonInclusionMap (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : skeletonHomology X n n ⟶ relHomologySkeleton X n n

The map H_n(X_n) → H_n(X_n, X_{n-1}) induced by the quotient of chain complexes.

noncomputable def CWHomology.cellularBoundary (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : cellularChainObj X (n + 1) ⟶ cellularChainObj X n

The cellular boundary map d_n : C_{n+1}(X) → C_n(X) built from the connecting homomorphism and the inclusion map, transported along the cellularChainIso.

theorem CWHomology.skeletonInclusionMap_comp_skeletonConnectingHom (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : CategoryTheory.CategoryStruct.comp (skeletonInclusionMap X (n + 1)) (skeletonConnectingHom X n) = 0

The composition H_{n+1}(X_{n+1}) → H_{n+1}(X_{n+1}, X_n) → H_n(X_n) vanishes by exactness of the long exact sequence of the pair.

theorem CWHomology.cellularBoundary_comp (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : CategoryTheory.CategoryStruct.comp (cellularBoundary X (n + 1)) (cellularBoundary X n) = 0

The cellular boundary squares to zero: d_n ∘ d_{n+1} = 0, making C_*(X) a chain complex.

noncomputable def CWHomology.cellularChainComplex (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] : ChainComplex AddCommGrpCat ℕ

The cellular chain complex C_*(X) of a CW complex X, with chain groups C_n(X) and differentials given by cellularBoundary.

noncomputable def CWHomology.cellularHomologyGroup (n : ℕ) (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] : AddCommGrpCat

The n-th cellular homology group H_n(C_*(X)) of a CW complex X.

noncomputable def CWHomology.skeletonStepMap (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : skeletonHomology X n n ⟶ skeletonHomology X (n + 1) n

The inclusion-induced map H_n(X_n) → H_n(X_{n+1}).

theorem CWHomology.skeletonConnectingHom_comp_skeletonStepMap (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : CategoryTheory.CategoryStruct.comp (skeletonConnectingHom X n) (skeletonStepMap X n) = 0

The composition H_{n+1}(X_{n+1}, X_n) → H_n(X_n) → H_n(X_{n+1}) vanishes by exactness of the long exact sequence of the pair.

noncomputable def CWHomology.skeletonSC_cokernelIsoH (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : skeletonHomology X (n + 1) n ≅ (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel { X₁ := relHomologySkeleton X (n + 1) (n + 1), X₂ := skeletonHomology X n n, X₃ := skeletonHomology X (n + 1) n, f := skeletonConnectingHom X n, g := skeletonStepMap X n, zero := ⋯ }).H

The identification of H_n(X_{n+1}) with the cokernel of the connecting map (the "H" of the left-homology data of the skeleton short complex).

noncomputable def CWHomology.skeletonSC_leftHomologyData (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : { X₁ := relHomologySkeleton X (n + 1) (n + 1), X₂ := skeletonHomology X n n, X₃ := skeletonHomology X (n + 1) n, f := skeletonConnectingHom X n, g := skeletonStepMap X n, zero := ⋯ }.LeftHomologyData

A choice of left-homology data for the short complex H_{n+1}(X_{n+1}, X_n) → H_n(X_n) → H_n(X_{n+1}), with H identified with H_n(X_{n+1}) via skeletonSC_cokernelIsoH.

theorem CWHomology.skeletonSC_leftHomologyData_H (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : (skeletonSC_leftHomologyData X n).H = skeletonHomology X (n + 1) n

The H field of skeletonSC_leftHomologyData is definitionally H_n(X_{n+1}).

noncomputable def CWHomology.skeletonCokernelIso (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : { X₁ := relHomologySkeleton X (n + 1) (n + 1), X₂ := skeletonHomology X n n, X₃ := skeletonHomology X (n + 1) n, f := skeletonConnectingHom X n, g := skeletonStepMap X n, zero := ⋯ }.homology ≅ skeletonHomology X (n + 1) n

Identification of the homology of the skeleton short complex with H_n(X_{n+1}).

theorem CWHomology.skeletonInclusionMap_mono (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : CategoryTheory.Mono (skeletonInclusionMap X n)

The map H_n(X_n) → H_n(X_n, X_{n-1}) is a monomorphism (equivalently, injective).

theorem CWHomology.skeletonPair_exact (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : { X₁ := skeletonHomology X (n + 1) (n + 1), X₂ := relHomologySkeleton X (n + 1) (n + 1), X₃ := skeletonHomology X n n, f := skeletonInclusionMap X (n + 1), g := skeletonConnectingHom X n, zero := ⋯ }.Exact

Exactness of the short complex H_{n+1}(X_{n+1}) → H_{n+1}(X_{n+1}, X_n) → H_n(X_n) from the long exact sequence of the CW pair.

noncomputable def CWHomology.cellularHomology_skeletonHomology_to_abH (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : skeletonHomology X (n + 1) n ≅ (HomologicalComplex.sc' (cellularChainComplex X) (n + 1) n ((ComplexShape.down ℕ).next n)).abLeftHomologyData.H

Identification of H_n(X_{n+1}) with the H of the abelian-group left-homology data of the relevant short complex of the cellular chain complex.

noncomputable def CWHomology.cellularSC_homologyQuotientIso (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : { X₁ := relHomologySkeleton X (n + 1) (n + 1), X₂ := skeletonHomology X n n, X₃ := skeletonHomology X (n + 1) n, f := skeletonConnectingHom X n, g := skeletonStepMap X n, zero := ⋯ }.homology ≅ (HomologicalComplex.sc' (cellularChainComplex X) (n + 1) n ((ComplexShape.down ℕ).next n)).abLeftHomologyData.H

Composite isomorphism between the homology of the skeleton short complex and the H of the cellular short complex.

noncomputable def CWHomology.cellularSC_leftHomologyData (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : (HomologicalComplex.sc' (cellularChainComplex X) (n + 1) n ((ComplexShape.down ℕ).next n)).LeftHomologyData

Alternative left-homology data for the cellular short complex obtained by copying the abelian-group data along the isomorphism with the skeleton homology.

theorem CWHomology.cellularSC_leftHomologyData_H (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : (cellularSC_leftHomologyData X n).H = (skeletonSC_leftHomologyData X n).H

The underlying object H of cellularSC_leftHomologyData agrees with the one of skeletonSC_leftHomologyData.

noncomputable def CWHomology.skeletonShortComplexHomologyIso (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (n : ℕ) : cellularHomologyGroup n X ≅ { X₁ := relHomologySkeleton X (n + 1) (n + 1), X₂ := skeletonHomology X n n, X₃ := skeletonHomology X (n + 1) n, f := skeletonConnectingHom X n, g := skeletonStepMap X n, zero := ⋯ }.homology

Identification of the cellular homology group H_n(C_*(X)) with the homology of the short complex H_{n+1}(X_{n+1}, X_n) → H_n(X_n) → H_n(X_{n+1}).

noncomputable def CWHomology.cellularHomology_iso_skeletonHomology_succ (n : ℕ) (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] : cellularHomologyGroup n X ≅ skeletonHomology X (n + 1) n

Intermediate isomorphism in the proof of Theorem 16.3: cellular homology is identified with the singular homology of the (n+1)-skeleton, H_n(C_*(X)) ≅ H_n(X_{n+1}).

noncomputable def CWHomology.cellularHomologyGroup_iso_singularHomologyGroup (n : ℕ) (X : Type) [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] : cellularHomologyGroup n X ≅ AlgebraicTopologyI.SingularHomologyGroup n X

Theorem 16.3. For a CW complex X, the cellular homology is isomorphic to the singular homology: H_n(C_*(X)) ≅ H_n(X).

structure CWHomology.IsCellularMap {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) : Prop

A continuous map f : X → Y between CW complexes is cellular if it sends the n-skeleton of X into the n-skeleton of Y for every n.

• mapsTo_skeleton (n : ℕ) : Set.MapsTo ⇑f ↑(CWComplex.skeleton X ↑n) ↑(CWComplex.skeleton Y ↑n)

def CWHomology.cellularMapOnSkeleton {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : TopCat.of ↑↑(CWComplex.skeleton X ↑n) ⟶ TopCat.of ↑↑(CWComplex.skeleton Y ↑n)

The restriction of a cellular map f : X → Y to the n-skeletons, viewed as a morphism X_n ⟶ Y_n in TopCat.

def CWHomology.cellularMapOnPrevSkeleton {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : TopCat.of ↑(Subtype.val ⁻¹' ↑(CWComplex.skeleton X ↑(n - 1))) ⟶ TopCat.of ↑(Subtype.val ⁻¹' ↑(CWComplex.skeleton Y ↑(n - 1)))

The restriction of a cellular map f to the previous-skeleton subspace, viewed as a morphism between the preimages of X_{n-1} (in X_n) and Y_{n-1} (in Y_n).

theorem CWHomology.cellularMapSquare_comm {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : CategoryTheory.CategoryStruct.comp (Excision.subspaceTopInclusion (Subtype.val ⁻¹' ↑(CWComplex.skeleton X ↑(n - 1)))) (cellularMapOnSkeleton f hf n) = CategoryTheory.CategoryStruct.comp (cellularMapOnPrevSkeleton f hf n) (Excision.subspaceTopInclusion (Subtype.val ⁻¹' ↑(CWComplex.skeleton Y ↑(n - 1))))

The naturality square between the inclusion of the previous-skeleton subspace into the n-skeleton, and the cellular map restricted to skeletons, commutes.

noncomputable def CWHomology.cellularRelativeChainMap {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : Excision.relativeSingularChainComplex (↑↑(CWComplex.skeleton X ↑n)) (Subtype.val ⁻¹' ↑(CWComplex.skeleton X ↑(n - 1))) ⟶ Excision.relativeSingularChainComplex (↑↑(CWComplex.skeleton Y ↑n)) (Subtype.val ⁻¹' ↑(CWComplex.skeleton Y ↑(n - 1)))

The induced map between relative singular chain complexes of the CW pairs (X_n, X_{n-1}) and (Y_n, Y_{n-1}) arising from a cellular map.

noncomputable def CWHomology.relHomologySkeletonMap {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : relHomologySkeleton X n n ⟶ relHomologySkeleton Y n n

The induced map on relative singular homology H_n(X_n, X_{n-1}) → H_n(Y_n, Y_{n-1}) arising from a cellular map.

noncomputable def CWHomology.cellularChainMapComponent {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : cellularChainObj X n ⟶ cellularChainObj Y n

The induced map on cellular chains C_n(X) → C_n(Y) arising from a cellular map, obtained by transporting relHomologySkeletonMap along the cellular-chain isomorphisms.

noncomputable def CWHomology.skeletonAbsHomologyMap {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : skeletonHomology X n n ⟶ skeletonHomology Y n n

The induced map on absolute singular homology of the skeletons, H_n(X_n) → H_n(Y_n), arising from a cellular map.

theorem CWHomology.skeletonConnectingHom_naturality {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : CategoryTheory.CategoryStruct.comp (relHomologySkeletonMap f hf (n + 1)) (skeletonConnectingHom Y n) = CategoryTheory.CategoryStruct.comp (skeletonConnectingHom X n) (skeletonAbsHomologyMap f hf n)

Naturality of the connecting homomorphism with respect to cellular maps.

theorem CWHomology.skeletonInclusionMap_naturality {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : CategoryTheory.CategoryStruct.comp (skeletonAbsHomologyMap f hf n) (skeletonInclusionMap Y n) = CategoryTheory.CategoryStruct.comp (skeletonInclusionMap X n) (relHomologySkeletonMap f hf n)

Naturality of the inclusion map H_n(X_n) → H_n(X_n, X_{n-1}) with respect to cellular maps.

theorem CWHomology.skeletonConnectingHom_inclusionMap_naturality {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : CategoryTheory.CategoryStruct.comp (relHomologySkeletonMap f hf (n + 1)) (CategoryTheory.CategoryStruct.comp (skeletonConnectingHom Y n) (skeletonInclusionMap Y n)) = CategoryTheory.CategoryStruct.comp (skeletonConnectingHom X n) (CategoryTheory.CategoryStruct.comp (skeletonInclusionMap X n) (relHomologySkeletonMap f hf n))

Combined naturality: the composite connecting ∘ inclusion is natural with respect to cellular maps.

theorem CWHomology.cellularChainMapComponent_comm {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) (n : ℕ) : CategoryTheory.CategoryStruct.comp (cellularChainMapComponent f hf (n + 1)) (cellularBoundary Y n) = CategoryTheory.CategoryStruct.comp (cellularBoundary X n) (cellularChainMapComponent f hf n)

The components C_n(f) : C_n(X) → C_n(Y) are compatible with the cellular boundary maps, i.e. they assemble into a chain map.

noncomputable def CWHomology.cellularChainMap {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) : cellularChainComplex X ⟶ cellularChainComplex Y

The chain map C_*(X) → C_*(Y) induced by a cellular map f : X → Y.

noncomputable def CWHomology.singularHomologyMap (n : ℕ) {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : AlgebraicTopologyI.SingularHomologyGroup n X ⟶ AlgebraicTopologyI.SingularHomologyGroup n Y

The map on singular homology H_n(X) → H_n(Y) induced by a continuous map.

noncomputable def CWHomology.cellularHomologyMap (n : ℕ) {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) : cellularHomologyGroup n X ⟶ cellularHomologyGroup n Y

The map on cellular homology H_n(C_*(X)) → H_n(C_*(Y)) induced by a cellular map.

noncomputable def CWHomology.skeletonHomologyMapInduced (n : ℕ) {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) : skeletonHomology X (n + 1) n ⟶ skeletonHomology Y (n + 1) n

The induced map H_n(X_{n+1}) → H_n(Y_{n+1}) from the restriction of a cellular map to (n+1)-skeletons.

theorem CWHomology.skeletonInclusion_cellularMap_comm (n : ℕ) {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) : CategoryTheory.CategoryStruct.comp (CWComplex.SkeletonHomology.skeletonInclusion X (n + 1)) (TopCat.ofHom f) = CategoryTheory.CategoryStruct.comp (cellularMapOnSkeleton f hf (n + 1)) (CWComplex.SkeletonHomology.skeletonInclusion Y (n + 1))

Topological commutativity of the square: inclusion of the (n+1)-skeleton followed by f equals the restriction of f to skeletons followed by inclusion into Y.

theorem CWHomology.skeletonHomologyMap_naturality (n : ℕ) {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) : CategoryTheory.CategoryStruct.comp (skeletonHomologyMapInduced n f hf) (CWComplex.SkeletonHomology.skeletonHomologyMap Y n (n + 1)) = CategoryTheory.CategoryStruct.comp (CWComplex.SkeletonHomology.skeletonHomologyMap X n (n + 1)) (singularHomologyMap n f)

Naturality of the H_n(X_{n+1}) → H_n(X) map with respect to cellular maps.

theorem CWHomology.cellularHomology_iso_skeletonHomology_succ_natural (n : ℕ) {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] [T2Space Y] [Topology.CWComplex Set.univ] [Topology.CWComplex Set.univ] (f : C(X, Y)) (hf : IsCellularMap f) : CategoryTheory.CategoryStruct.comp (cellularHomologyMap n f hf) (cellularHomology_iso_skeletonHomology_succ n Y).hom = CategoryTheory.CategoryStruct.comp (cellularHomology_iso_skeletonHomology_succ n X).hom (skeletonHomologyMapInduced n f hf)

Naturality of the intermediate isomorphism H_n(C_*(X)) ≅ H_n(X_{n+1}) with respect to cellular maps — this gives the filtration-preserving-naturality statement of Theorem 16.3.

def CellularHomology.HasOnlyEvenCells (X : Type) [TopologicalSpace X] [Topology.CWComplex Set.univ] : Prop

A CW complex has only even cells if there are no cells of odd dimension.

theorem CellularHomology.cellularChains_odd_subsingleton (X : Type) [TopologicalSpace X] [Topology.CWComplex Set.univ] (heven : HasOnlyEvenCells X) (k : ℕ) : Subsingleton (CWComplex.cellularChains X (2 * k + 1))

If X has only even cells, the cellular chain group C_{2k+1}(X) in odd degree is trivial (a subsingleton).

noncomputable def CellularHomology.singularHomology_iso_cellularChainGroup (X : Type) [TopologicalSpace X] [Topology.CWComplex Set.univ] (heven : HasOnlyEvenCells X) (n : ℕ) : AlgebraicTopologyI.SingularHomologyGroup n X ≅ AddCommGrpCat.of (CWComplex.cellularChains X n)

Corollary 16.4. For a CW complex X with only even cells, all cellular boundary maps vanish, so the singular homology in degree n is isomorphic to the cellular chain group C_n(X) = ℤ^{(\text{cells in deg } n)}. In particular, H_n(X) = 0 for n odd, is free abelian for all n, and has rank equal to the number of n-cells in even degrees.