Relative CW complexes with all cells attached along the base

Suppose each cell of a relative CW complex (C, D) is attached directly along the base, ∂eᵢ ⊆ D. Such a complex is D with a family of discs glued on independently, as happens across a critical level of a Morse function, where one disc is attached along the lower sublevel at each critical point. All of its cellular differentials vanish (TauCeti.cellularChainComplex_d_eq_zero_of_cellFrontier_subset), so its relative homology is the cellular chain group: Hₙ(C, D; R) is the coproduct of one copy of R for each n-cell (TauCeti.nonempty_singularHomology_complexBasePair_iso_sigma), and over a division ring its dimension is the number of n-cells times the dimension of the coefficients (TauCeti.finrank_singularHomology_complexBasePair_of_cellFrontier_subset). This sharpens the weak Morse inequality TauCeti.finrank_singularHomology_complexBasePair_le of a general CW pair to an equality.

Main results

• TauCeti.nonempty_singularHomology_complexBasePair_iso_sigma and TauCeti.finrank_singularHomology_complexBasePair_of_cellFrontier_subset: the relative homology of such a complex is free on its cells.

References

• A. Hatcher, Algebraic Topology, Section 2.2, the cellular boundary formula and Theorem 2.35.
• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton University Press, 1963, Section 5, for the homology of a space with cells attached along a subspace.

theorem TauCeti.nonempty_singularHomology_complexBasePair_iso_sigma {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [∀ (m : ℕ), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C m)) A] (h : ∀ (m : ℕ) (j : Topology.RelCWComplex.cell C m), Topology.RelCWComplex.cellFrontier m j ⊆ D) (n : ℕ) [CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonBasePairToComplex C (n + 1)) R n)] : Nonempty ((complexBasePair C).singularHomology R n ≅ ∐ fun (x : Topology.RelCWComplex.cell C n) => R)

The relative homology of a complex attached along its base. If the boundary sphere of every cell of the relative CW complex (C, D) lies in D, then Hₙ(C, D; R) is the coproduct of one copy of R for each n-cell. As for TauCeti.cellularSingularHomologyIso, the inclusion of the (n + 1)-skeleton must induce an isomorphism on Hₙ, which holds for every finite-dimensional complex and, when sequential colimits are exact in A, for every complex.

theorem TauCeti.finrank_singularHomology_complexBasePair_of_cellFrontier_subset {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {k : Type w} [DivisionRing k] (M : ModuleCat k) [Module.Finite k ↑M] (h : ∀ (m : ℕ) (j : Topology.RelCWComplex.cell C m), Topology.RelCWComplex.cellFrontier m j ⊆ D) (n : ℕ) [Finite (Topology.RelCWComplex.cell C n)] : Module.finrank k ↑((complexBasePair C).singularHomology M n) = Nat.card (Topology.RelCWComplex.cell C n) * Module.finrank k ↑M

The relative homology of a complex attached along its base is free on its cells. If the boundary sphere of every cell of the relative CW complex (C, D) lies in D, and there are finitely many n-cells, then Hₙ(C, D; M) has dimension the number of n-cells times dim M, for a finite-dimensional module M over a division ring.