The cellular chain complex of a relative CW complex

The skeleta of a relative CW complex filter it by closed subspaces, and the relative singular homology of consecutive skeleta assembles into a chain complex: the cellular chain complex. Its group in degree n is Hₙ(Xⁿ, Xⁿ⁻¹), and its differential is the connecting morphism of the long exact sequence of the triple (Xⁿ⁺¹, Xⁿ, Xⁿ⁻¹) of three consecutive skeleta. That connecting morphism factors as Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹) through the singular homology of the middle skeleton. Composing two consecutive differentials puts the map Hₙ₊₁(Xⁿ⁺¹) ⟶ Hₙ₊₁(Xⁿ⁺¹, Xⁿ) next to the connecting morphism Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ); those two are consecutive in the long exact sequence of the pair (Xⁿ⁺¹, Xⁿ), so they compose to zero, and hence so do the two differentials.

A degree carrying no cells has equal consecutive skeleta, hence a zero cellular chain group, so the cellular chain complex of a finite-dimensional complex vanishes in high degrees.

Inclusions between arbitrary skeleta and into the whole complex give maps of pairs relative to the base. Their induced homology maps connect skeletal relative homology to the homology of the whole pair (X, X⁻¹) and are used in the cellular-to-singular comparison.

Coefficients are an object R of an abelian category with coproducts, as everywhere in relative singular homology; no ring or module structure is needed.

Main definitions

• TauCeti.skeletonPair, TauCeti.skeletonTriple: the pair and the triple of consecutive skeleta.
• TauCeti.skeletonBasePair, TauCeti.skeletonBaseTriple: the pair (Xⁿ, X⁻¹) of a skeleton relative to the base, and the triple (Xⁿ⁺¹, Xⁿ, X⁻¹).
• TauCeti.skeletonBasePairToSucc, TauCeti.skeletonBasePairToSkeletonPair: the maps of pairs (Xⁿ, X⁻¹) ⟶ (Xⁿ⁺¹, X⁻¹) and (Xⁿ, X⁻¹) ⟶ (Xⁿ, Xⁿ⁻¹).
• TauCeti.skeletonBasePairInclusion: the inclusion (Xⁿ, X⁻¹) ⟶ (Xᵐ, X⁻¹) for n ≤ m.
• TauCeti.complexBasePair: the whole relative CW complex as the pair (X, X⁻¹).
• TauCeti.skeletonBasePairToComplex: the inclusion (Xⁿ, X⁻¹) ⟶ (X, X⁻¹).
• TauCeti.cellularChainGroup: the relative homology Hₙ(Xⁿ, Xⁿ⁻¹).
• TauCeti.cellularDifferential: the cellular differential.
• TauCeti.cellularChainComplex: the resulting chain complex.

Main results

• TauCeti.cellularDifferential_eq_singularHomologyδ: the cellular differential is the connecting morphism of the triple of three consecutive skeleta.
• TauCeti.cellularDifferential_comp_cellularDifferential: consecutive cellular differentials compose to zero.
• TauCeti.isZero_cellularChainGroup and TauCeti.eventually_isZero_cellularChainGroup: vanishing of the cellular chain groups in degrees without cells, and in all high degrees of a finite-dimensional complex.

The source is Hatcher, Algebraic Topology, Section 2.2.

theorem TauCeti.skeletonLT_subset_skeletonLT_succ {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : ↑(Topology.RelCWComplex.skeletonLT C ↑n) ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))

Consecutive skeleta of a relative CW complex are nested. This is skeletonLT_mono in the natural-number indexing used by the skeletal filtration below.

@[reducible, inline]

abbrev TauCeti.skeletonPair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair

The topological pair of consecutive skeleta of a relative CW complex. In the indexing used here skeletonPair C n is the pair (Xⁿ, Xⁿ⁻¹): its ambient space is skeletonLT C (n + 1), the n-skeleton, and its subspace is skeletonLT C n.

Equations

• TauCeti.skeletonPair C n = TopPair.ofInclusion ⋯

@[reducible, inline]

abbrev TauCeti.skeletonTriple {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopTriple

The triple (Xⁿ⁺¹, Xⁿ, Xⁿ⁻¹) of three consecutive skeleta of a relative CW complex. Its outer pair is skeletonPair C (n + 1) and its inner pair is skeletonPair C n.

Equations

• TauCeti.skeletonTriple C n = TauCeti.TopTriple.ofInclusions ⋯ ⋯

@[simp]

theorem TauCeti.skeletonPair_snd {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair.snd = skeletonObj C n

The subspace of the n-th skeletal pair is the (n-1)-skeleton.

@[simp]

theorem TauCeti.skeletonPair_fst {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair.fst = skeletonObj C (n + 1)

The ambient space of the n-th skeletal pair is the n-skeleton.

theorem TauCeti.skeletonLT_zero_subset_skeletonLT {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : ↑(Topology.RelCWComplex.skeletonLT C ↑0) ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑n)

The base X⁻¹ = skeletonLT C 0 of the skeletal filtration lies in every skeleton.

@[reducible, inline]

abbrev TauCeti.skeletonBasePair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair

The pair (Xⁿ, X⁻¹) of the n-skeleton relative to the base of a relative CW complex. Its ambient space is skeletonLT C (n + 1) and its subspace is skeletonLT C 0, which is the base of the complex (TauCeti.range_skeletonBasePair_snd).

Equations

• TauCeti.skeletonBasePair C n = TopPair.ofInclusion ⋯

theorem TauCeti.skeletonBasePair_snd {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair.snd = skeletonObj C 0

The subspace of the n-th base pair is the (-1)-skeleton.

theorem TauCeti.skeletonBasePair_fst {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair.fst = skeletonObj C (n + 1)

The ambient space of the n-th base pair is the n-skeleton.

theorem TauCeti.range_skeletonBasePair_snd {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : (Set.range fun (x : ↑TopPair.snd) => ↑x) = D

The subspace X⁻¹ of the base pair (Xⁿ, X⁻¹) is the base of the relative CW complex.

@[reducible, inline]

abbrev TauCeti.skeletonBaseTriple {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopTriple

The triple (Xⁿ⁺¹, Xⁿ, X⁻¹). Its inner pair is skeletonBasePair C n, its total pair is skeletonBasePair C (n + 1), and its outer pair is skeletonPair C (n + 1) (TauCeti.innerPair_obj_skeletonBaseTriple, TauCeti.totalPair_obj_skeletonBaseTriple, TauCeti.outerPair_obj_skeletonBaseTriple).

Equations

• TauCeti.skeletonBaseTriple C n = TauCeti.TopTriple.ofInclusions ⋯ ⋯

theorem TauCeti.innerPair_obj_skeletonBaseTriple {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopTriple.innerPair.obj (skeletonBaseTriple C n) = skeletonBasePair C n

The inner pair of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹) is the base pair (Xⁿ, X⁻¹).

theorem TauCeti.totalPair_obj_skeletonBaseTriple {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopTriple.totalPair.obj (skeletonBaseTriple C n) = skeletonBasePair C (n + 1)

The total pair of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹) is the base pair (Xⁿ⁺¹, X⁻¹).

theorem TauCeti.outerPair_obj_skeletonBaseTriple {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopTriple.outerPair.obj (skeletonBaseTriple C n) = skeletonPair C (n + 1)

The outer pair of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹) is the skeletal pair (Xⁿ⁺¹, Xⁿ).

def TauCeti.skeletonBasePairToSucc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : skeletonBasePair C n ⟶ skeletonBasePair C (n + 1)

The inclusion (Xⁿ, X⁻¹) ⟶ (Xⁿ⁺¹, X⁻¹) of consecutive base pairs. It is the map from the inner pair to the total pair of the triple TauCeti.skeletonBaseTriple C n (TauCeti.skeletonBasePairToSucc_def).

Equations

• TauCeti.skeletonBasePairToSucc C n = TauCeti.TopTriple.innerToTotal.app (TauCeti.skeletonBaseTriple C n)

theorem TauCeti.skeletonBasePairToSucc_def {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : skeletonBasePairToSucc C n = TopTriple.innerToTotal.app (skeletonBaseTriple C n)

TauCeti.skeletonBasePairToSucc is the map from the inner pair to the total pair of the triple TauCeti.skeletonBaseTriple C n.

def TauCeti.skeletonBasePairToSkeletonPair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : skeletonBasePair C n ⟶ skeletonPair C n

The map of pairs (Xⁿ, X⁻¹) ⟶ (Xⁿ, Xⁿ⁻¹) which is the identity on Xⁿ.

Equations

• TauCeti.skeletonBasePairToSkeletonPair C n = TopPair.ofInclusionMap ⋯ ⋯ (ContinuousMap.id ↑↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1))) ⋯

@[simp]

theorem TauCeti.skeletonBasePairToSkeletonPair_fst {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair.Hom.fst (skeletonBasePairToSkeletonPair C n) = CategoryTheory.CategoryStruct.id (skeletonObj C (n + 1))

The ambient component of the map to a skeletal pair is the identity.

@[simp]

theorem TauCeti.skeletonBasePairToSkeletonPair_snd {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair.Hom.snd (skeletonBasePairToSkeletonPair C n) = TopCat.ofHom (ContinuousMap.inclusion ⋯)

The base component of the map to a skeletal pair is inclusion into the lower skeleton.

@[simp]

theorem TauCeti.coe_skeletonBasePairToSucc_fst_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) (x : ↑TopPair.fst) : ↑((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst (skeletonBasePairToSucc C n))) x) = ↑x

On the ambient spaces, TauCeti.skeletonBasePairToSucc is the inclusion Xⁿ ⊆ Xⁿ⁺¹.

@[simp]

theorem TauCeti.skeletonBasePairToSucc_snd_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) (x : ↑TopPair.snd) : (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd (skeletonBasePairToSucc C n))) x = x

On the subspaces, TauCeti.skeletonBasePairToSucc is the identity of X⁻¹.

@[simp]

theorem TauCeti.skeletonBasePairToSkeletonPair_zero {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : skeletonBasePairToSkeletonPair C 0 = CategoryTheory.CategoryStruct.id (skeletonPair C 0)

In degree 0 the map (X⁰, X⁻¹) ⟶ (X⁰, X⁻¹) is the identity.

theorem TauCeti.skeletonBasePairToSkeletonPair_succ {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : skeletonBasePairToSkeletonPair C (n + 1) = TopTriple.totalToOuter.app (skeletonBaseTriple C n)

In positive degree the map (Xⁿ⁺¹, X⁻¹) ⟶ (Xⁿ⁺¹, Xⁿ) is the map from the total pair to the outer pair of the triple (Xⁿ⁺¹, Xⁿ, X⁻¹).

def TauCeti.skeletonBasePairInclusion {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n m : ℕ} (h : n ≤ m) : skeletonBasePair C n ⟶ skeletonBasePair C m

Inclusion of base pairs (Xⁿ, X⁻¹) ⟶ (Xᵐ, X⁻¹) for n ≤ m.

Equations

• TauCeti.skeletonBasePairInclusion C h = TopPair.ofInclusionMap ⋯ ⋯ (ContinuousMap.inclusion ⋯) ⋯

@[simp]

theorem TauCeti.coe_skeletonBasePairInclusion_fst_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n m : ℕ} (h : n ≤ m) (x : ↑TopPair.fst) : ↑((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst (skeletonBasePairInclusion C h))) x) = ↑x

@[simp]

theorem TauCeti.skeletonBasePairInclusion_snd_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n m : ℕ} (h : n ≤ m) (x : ↑TopPair.snd) : (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd (skeletonBasePairInclusion C h))) x = x

@[simp]

theorem TauCeti.skeletonBasePairInclusion_refl {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : skeletonBasePairInclusion C ⋯ = CategoryTheory.CategoryStruct.id (skeletonBasePair C n)

theorem TauCeti.skeletonBasePairInclusion_comp {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n m l : ℕ} (h : n ≤ m) (h' : m ≤ l) : CategoryTheory.CategoryStruct.comp (skeletonBasePairInclusion C h) (skeletonBasePairInclusion C h') = skeletonBasePairInclusion C ⋯

Inclusions of base pairs compose as inclusions.

theorem TauCeti.skeletonBasePairInclusion_comp_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n m l : ℕ} (h : n ≤ m) (h' : m ≤ l) {Z : TopPair} (h✝ : skeletonBasePair C l ⟶ Z) : CategoryTheory.CategoryStruct.comp (skeletonBasePairInclusion C h) (CategoryTheory.CategoryStruct.comp (skeletonBasePairInclusion C h') h✝) = CategoryTheory.CategoryStruct.comp (skeletonBasePairInclusion C ⋯) h✝

Inclusions of base pairs compose as inclusions.

theorem TauCeti.skeletonBasePairInclusion_succ {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : skeletonBasePairInclusion C ⋯ = skeletonBasePairToSucc C n

The inclusion into the next base pair is the map of the skeletal triple.

@[reducible, inline]

abbrev TauCeti.complexBasePair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : TopPair

The whole relative CW complex as a pair with its base X⁻¹ = skeletonLT C 0.

Equations

• TauCeti.complexBasePair C = TopPair.ofInclusion ⋯

theorem TauCeti.complexBasePair_eq_ofInclusion {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] : complexBasePair C = TopPair.ofInclusion ⋯

The base in complexBasePair is the actual base D of the relative CW complex.

instance TauCeti.isEmpty_complexBasePair_snd {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [IsEmpty ↑D] : IsEmpty ↑TopPair.snd

The topological pair of a CW complex with empty base has empty subspace.

def TauCeti.skeletonBasePairToComplex {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : skeletonBasePair C n ⟶ complexBasePair C

Inclusion of a skeleton relative to the base into the whole relative CW complex.

Equations

• TauCeti.skeletonBasePairToComplex C n = TopPair.ofInclusionMap ⋯ ⋯ (ContinuousMap.inclusion ⋯) ⋯

@[simp]

theorem TauCeti.skeletonBasePairToComplex_fst {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair.Hom.fst (skeletonBasePairToComplex C n) = TopCat.ofHom (ContinuousMap.inclusion ⋯)

The ambient component of the map to the whole pair is inclusion of the skeleton.

@[simp]

theorem TauCeti.skeletonBasePairToComplex_snd {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) : TopPair.Hom.snd (skeletonBasePairToComplex C n) = CategoryTheory.CategoryStruct.id (skeletonObj C 0)

The base component of the map to the whole pair is the identity.

@[simp]

theorem TauCeti.skeletonBasePairInclusion_comp_toComplex {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n m : ℕ} (h : n ≤ m) : CategoryTheory.CategoryStruct.comp (skeletonBasePairInclusion C h) (skeletonBasePairToComplex C m) = skeletonBasePairToComplex C n

Inclusion into the whole pair factors through any larger skeleton.

@[simp]

theorem TauCeti.skeletonBasePairInclusion_comp_toComplex_assoc {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {n m : ℕ} (h : n ≤ m) {Z : TopPair} (h✝ : complexBasePair C ⟶ Z) : CategoryTheory.CategoryStruct.comp (skeletonBasePairInclusion C h) (CategoryTheory.CategoryStruct.comp (skeletonBasePairToComplex C m) h✝) = CategoryTheory.CategoryStruct.comp (skeletonBasePairToComplex C n) h✝

Inclusion into the whole pair factors through any larger skeleton.

theorem TauCeti.isIso_skeletonBasePairToComplex_of_eq {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (m : ℕ) (hm : ↑(Topology.RelCWComplex.skeletonLT C ↑(m + 1)) = C) : CategoryTheory.IsIso (skeletonBasePairToComplex C m)

If a skeleton is the whole complex, its inclusion as a pair is an isomorphism.

@[reducible, inline]

noncomputable abbrev TauCeti.skeletonHomology {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) (n k : ℕ) : A

The singular homology, with coefficients in R, of the n-th stage of the skeletal filtration of a relative CW complex, in degree k.

Equations

• TauCeti.skeletonHomology C R n k = (TopCat.toSSet.obj (TauCeti.skeletonObj C n)).homology R k

@[reducible, inline]

noncomputable abbrev TauCeti.cellularChainGroup {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) (n : ℕ) : A

The cellular chain group of a relative CW complex in degree n with coefficients in R: the relative singular homology Hₙ(Xⁿ, Xⁿ⁻¹) of the pair of consecutive skeleta.

Equations

• TauCeti.cellularChainGroup C R n = (TauCeti.skeletonPair C n).singularHomology R n

@[reducible, inline]

noncomputable abbrev TauCeti.skeletonPairδ {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) (n : ℕ) : cellularChainGroup C R (n + 1) ⟶ skeletonHomology C R (n + 1) n

The connecting morphism Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ) of the long exact sequence of the skeletal pair.

Equations

• TauCeti.skeletonPairδ C R n = (TauCeti.skeletonPair C (n + 1)).singularHomologyδ R (n + 1) n ⋯

@[reducible, inline]

noncomputable abbrev TauCeti.skeletonPairπ {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) (n : ℕ) : skeletonHomology C R (n + 1) n ⟶ cellularChainGroup C R n

The map Hₙ(Xⁿ) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹) from the singular homology of the n-skeleton to the relative homology of the skeletal pair.

Equations

• TauCeti.skeletonPairπ C R n = (TauCeti.skeletonPair C n).singularHomologyπ R n

noncomputable def TauCeti.cellularDifferential {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) (n : ℕ) : cellularChainGroup C R (n + 1) ⟶ cellularChainGroup C R n

The cellular differential Hₙ₊₁(Xⁿ⁺¹, Xⁿ) ⟶ Hₙ(Xⁿ, Xⁿ⁻¹), namely the connecting morphism of the skeletal pair followed by the map to the relative homology of the next skeletal pair. It is the connecting morphism of the triple of three consecutive skeleta, by TauCeti.cellularDifferential_eq_singularHomologyδ.

Equations

• TauCeti.cellularDifferential C R n = CategoryTheory.CategoryStruct.comp (TauCeti.skeletonPairδ C R n) (TauCeti.skeletonPairπ C R n)

theorem TauCeti.cellularDifferential_eq_skeletonPairδ_comp_skeletonPairπ {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) (n : ℕ) : cellularDifferential C R n = CategoryTheory.CategoryStruct.comp (skeletonPairδ C R n) (skeletonPairπ C R n)

The cellular differential is the connecting morphism of the skeletal pair followed by the map to the relative homology of the next skeletal pair.

theorem TauCeti.cellularDifferential_eq_singularHomologyδ {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) (n : ℕ) : cellularDifferential C R n = (skeletonTriple C n).singularHomologyδ R (n + 1) n ⋯

The cellular differential is the connecting morphism of the long exact sequence of the triple (Xⁿ⁺¹, Xⁿ, Xⁿ⁻¹) of three consecutive skeleta.

@[simp]

theorem TauCeti.skeletonPairπ_comp_skeletonPairδ {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) (n : ℕ) : CategoryTheory.CategoryStruct.comp (skeletonPairπ C R (n + 1)) (skeletonPairδ C R n) = 0

The map from the singular homology of a skeleton to the relative homology of the skeletal pair below it, followed by the connecting morphism of that pair, is zero: these are consecutive maps in the long exact sequence of the pair (Xⁿ⁺¹, Xⁿ).

@[simp]

theorem TauCeti.cellularDifferential_comp_cellularDifferential {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) (n : ℕ) : CategoryTheory.CategoryStruct.comp (cellularDifferential C R (n + 1)) (cellularDifferential C R n) = 0

Two consecutive cellular differentials compose to zero.

noncomputable def TauCeti.cellularChainComplex {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) : ChainComplex A ℕ

The cellular chain complex of a relative CW complex with coefficients in R.

Equations

• TauCeti.cellularChainComplex C R = ChainComplex.of (TauCeti.cellularChainGroup C R) (TauCeti.cellularDifferential C R) ⋯

@[simp]

theorem TauCeti.cellularChainComplex_X {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) (n : ℕ) : (cellularChainComplex C R).X n = cellularChainGroup C R n

The objects of the cellular chain complex are the cellular chain groups.

@[simp]

theorem TauCeti.cellularChainComplex_d {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) (n : ℕ) : (cellularChainComplex C R).d (n + 1) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (cellularDifferential C R n) (CategoryTheory.eqToHom ⋯))

The differentials of the cellular chain complex are the cellular differentials, transported across TauCeti.cellularChainComplex_X.

theorem TauCeti.skeletonLT_succ_eq_of_isEmpty_cell {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) [IsEmpty (Topology.RelCWComplex.cell C n)] : ↑(Topology.RelCWComplex.skeletonLT C ↑(n + 1)) = ↑(Topology.RelCWComplex.skeletonLT C ↑n)

A relative CW complex with no n-cells has equal n-skeleton and (n-1)-skeleton.

theorem TauCeti.isIso_skeletonPair_map {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) [IsEmpty (Topology.RelCWComplex.cell C n)] : CategoryTheory.IsIso TopPair.map

With no n-cells the inclusion Xⁿ⁻¹ ⟶ Xⁿ of the skeletal pair is an isomorphism.

theorem TauCeti.isZero_cellularChainGroup {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) [IsEmpty (Topology.RelCWComplex.cell C n)] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : CategoryTheory.Limits.IsZero (cellularChainGroup C R n)

The cellular chain group of a degree carrying no cells is zero: the two skeleta of the skeletal pair agree, so its relative singular chain complex vanishes.

theorem TauCeti.eventually_isZero_cellularChainGroup {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] [Topology.RelCWComplex.FiniteDimensional C] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : ∀ᶠ (n : ℕ) in Filter.atTop, CategoryTheory.Limits.IsZero (cellularChainGroup C R n)

The cellular chain groups of a finite-dimensional relative CW complex vanish in all sufficiently large degrees.