Cellular incidence coefficients

The cellular chain groups with coefficients in a ring have bases indexed by the actual cells. This file puts the cellular differential in those coordinates. Each boundary column is a finitely supported function on the cells in the preceding dimension, even for an infinite CW complex. The incidence coefficients reconstruct the differential, and consecutive columns satisfy the finite-sum relation expressing that its square is zero. In a degree with a single cell, the chain group is the coefficient ring itself (TauCeti.cellularChainCoord), and between two such degrees the differential is right multiplication by the incidence coefficient (TauCeti.cellularChainCoord_d).

The columns are also identified with the attaching maps: send the reduced fundamental class of the boundary sphere through the attaching map, pass to skeletal relative homology, and take cellular coordinates. This is the homological coefficient formula; identifying it with the geometric degree of a sphere map obtained by collapsing the other cells is a separate result. The bases use the disk and sphere generators of cellularChainGroupIso. The sphere generator in reducedSingularHomologyTopCatSphereIso is fixed by the ordered standard orthonormal basis, starting with the reduced degree-zero class [-e₀] - [e₀]. The disk generator maps to it under the connecting morphism, as expressed by singularHomologyDiskBoundaryPairIso_inv_comp_singularHomologyδ.

The coefficient ring and the ambient space lie in the same universe, as in Mathlib's exact coproduct interface for modules. No finite-cell or finite-dimensional hypothesis is imposed.

References

• A. Hatcher, Algebraic Topology, Section 2.2, the cellular boundary formula.

noncomputable def TauCeti.cellularChainBasis {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) : Module.Basis (Topology.RelCWComplex.cell C n) R ↑(cellularChainGroup C (↧R) n)

The cellular basis over R: the vector of a cell is the image of the fundamental class of its characteristic disk pair.

theorem TauCeti.cellularChainBasis_repr {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) : (cellularChainBasis C R n).repr = (cellularChainGroupIso C (↧R) n ≪≫ ModuleCat.coprodIsoDirectSum fun (x : Topology.RelCWComplex.cell C n) => ↧R).toLinearEquiv ≪≫ₗ (finsuppLEquivDirectSum R R (Topology.RelCWComplex.cell C n)).symm

The cellular basis coordinates are the coproduct coordinates of the characteristic cells.

@[simp]

theorem TauCeti.cellularChainBasis_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (j : Topology.RelCWComplex.cell C n) : (cellularChainBasis C R n) j = (CategoryTheory.ConcreteCategory.hom (cellularChainGroupIso C (↧R) n).inv) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C n) => ↧R) j)) 1)

A cellular basis vector is the image of 1 in its cell's coproduct summand.

noncomputable def TauCeti.cellularBoundaryColumn {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (j : Topology.RelCWComplex.cell C (n + 1)) : Topology.RelCWComplex.cell C n →₀ R

The boundary column of an (n + 1)-cell, with finite support on the n-cells.

theorem TauCeti.cellularBoundaryColumn_def {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (j : Topology.RelCWComplex.cell C (n + 1)) : cellularBoundaryColumn C R n j = (cellularChainBasis C R n).repr ((CategoryTheory.ConcreteCategory.hom (cellularDifferential C (↧R) n)) ((cellularChainBasis C R (n + 1)) j))

Boundary columns are the cellular coordinates of the differential on basis vectors.

noncomputable def TauCeti.cellularIncidence {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (i : Topology.RelCWComplex.cell C n) (j : Topology.RelCWComplex.cell C (n + 1)) : R

The incidence coefficient in row i and column j of the cellular differential. Over ℤ these are the integral cellular incidence numbers.

theorem TauCeti.cellularIncidence_def {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (i : Topology.RelCWComplex.cell C n) (j : Topology.RelCWComplex.cell C (n + 1)) : cellularIncidence C R n i j = ((cellularChainBasis C R n).repr ((CategoryTheory.ConcreteCategory.hom (cellularDifferential C (↧R) n)) ((cellularChainBasis C R (n + 1)) j))) i

An incidence coefficient is the corresponding coordinate of the differential of a cell.

@[simp]

theorem TauCeti.cellularBoundaryColumn_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (i : Topology.RelCWComplex.cell C n) (j : Topology.RelCWComplex.cell C (n + 1)) : (cellularBoundaryColumn C R n j) i = cellularIncidence C R n i j

theorem TauCeti.cellularBoundaryColumn_eq_attaching {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (j : Topology.RelCWComplex.cell C (n + 1)) : cellularBoundaryColumn C R n j = (cellularChainBasis C R n).repr ((CategoryTheory.ConcreteCategory.hom (skeletonPairπ C (↧R) n)) ((CategoryTheory.ConcreteCategory.hom (SSet.homologyMap (TopCat.toSSet.map (cellAttachingMap j)) (↧R) n)) ((CategoryTheory.ConcreteCategory.hom ((reducedSingularHomologyι (↧R) n).app (TopCat.diskBoundary (n + 1)))) ((CategoryTheory.ConcreteCategory.hom (reducedSingularHomologyTopCatSphereIso (↧R) n).inv) 1))))

The attaching-map formula in cellular coordinates. A boundary column is obtained by sending the reduced sphere generator through the attaching map and into skeletal relative homology, then taking cellular coordinates.

theorem TauCeti.cellularDifferential_basis {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (j : Topology.RelCWComplex.cell C (n + 1)) : (CategoryTheory.ConcreteCategory.hom (cellularDifferential C (↧R) n)) ((cellularChainBasis C R (n + 1)) j) = (cellularBoundaryColumn C R n j).sum fun (i : Topology.RelCWComplex.cell C n) (a : R) => a • (cellularChainBasis C R n) i

The differential on a cell is the finite sum of its incidence coefficients times the basis vectors of the preceding dimension.

theorem TauCeti.cellularChainBasis_repr_differential {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (x : ↑(cellularChainGroup C (↧R) (n + 1))) : (cellularChainBasis C R n).repr ((CategoryTheory.ConcreteCategory.hom (cellularDifferential C (↧R) n)) x) = ((cellularChainBasis C R (n + 1)).repr x).sum fun (j : Topology.RelCWComplex.cell C (n + 1)) (a : R) => a • cellularBoundaryColumn C R n j

Cellular coordinates of the differential of an arbitrary chain are the finite linear combination of its boundary columns.

theorem TauCeti.cellularChainBasis_repr_differential_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (x : ↑(cellularChainGroup C (↧R) (n + 1))) (i : Topology.RelCWComplex.cell C n) : ((cellularChainBasis C R n).repr ((CategoryTheory.ConcreteCategory.hom (cellularDifferential C (↧R) n)) x)) i = ∑ j ∈ ((cellularChainBasis C R (n + 1)).repr x).support, ((cellularChainBasis C R (n + 1)).repr x) j * cellularIncidence C R n i j

Each coordinate of a cellular boundary is the finite sum of the source coordinates times the corresponding incidence coefficients.

@[simp]

theorem TauCeti.cellularDifferential_eq_zero_iff {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) : cellularDifferential C (↧R) n = 0 ↔ ∀ (i : Topology.RelCWComplex.cell C n) (j : Topology.RelCWComplex.cell C (n + 1)), cellularIncidence C R n i j = 0

The cellular differential vanishes exactly when all its incidence coefficients vanish.

theorem TauCeti.cellularBoundaryColumn_sum_smul {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (j : Topology.RelCWComplex.cell C (n + 2)) : ((cellularBoundaryColumn C R (n + 1) j).sum fun (i : Topology.RelCWComplex.cell C (n + 1)) (a : R) => a • cellularBoundaryColumn C R n i) = 0

The finite-support column formula for d² = 0.

theorem TauCeti.sum_cellularIncidence_mul {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] (n : ℕ) (k : Topology.RelCWComplex.cell C n) (j : Topology.RelCWComplex.cell C (n + 2)) : ∑ i ∈ (cellularBoundaryColumn C R (n + 1) j).support, cellularIncidence C R (n + 1) i j * cellularIncidence C R n k i = 0

For each pair of cells two dimensions apart, the finite sum of the products of the two intermediate incidence coefficients is zero. The order of multiplication also works over noncommutative coefficient rings.

noncomputable def TauCeti.cellularChainCoord {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] {n : ℕ} [Subsingleton (Topology.RelCWComplex.cell C n)] (c : Topology.RelCWComplex.cell C n) : ↑((cellularChainComplex C ↧R).X n) ≃ₗ[R] R

In a degree n with a single cell c, the cellular chain group of C with coefficients in R is R, through the coordinate of c.

theorem TauCeti.cellularChainCoord_symm_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] {n : ℕ} [Subsingleton (Topology.RelCWComplex.cell C n)] (c : Topology.RelCWComplex.cell C n) (r : R) : (cellularChainCoord C R c).symm r = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) (r • (cellularChainBasis C R n) c)

The chain with coordinate r is r times the cellular basis vector of the unique cell.

theorem TauCeti.cellularChainCoord_cellularChainBasis {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] {n : ℕ} [Subsingleton (Topology.RelCWComplex.cell C n)] (c : Topology.RelCWComplex.cell C n) : (cellularChainCoord C R c) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((cellularChainBasis C R n) c)) = 1

The cellular basis vector of the unique cell has coordinate 1.

theorem TauCeti.cellularChainCoord_d {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (R : Type w) [Ring R] {n : ℕ} [Subsingleton (Topology.RelCWComplex.cell C n)] [Subsingleton (Topology.RelCWComplex.cell C (n + 1))] (c : Topology.RelCWComplex.cell C n) (c' : Topology.RelCWComplex.cell C (n + 1)) (x : ↑((cellularChainComplex C ↧R).X (n + 1))) : (cellularChainCoord C R c) ((CategoryTheory.ConcreteCategory.hom ((cellularChainComplex C ↧R).d (n + 1) n)) x) = (cellularChainCoord C R c') x * cellularIncidence C R n c c'

If C has a single cell c in degree n and a single cell c' in degree n + 1, then in the coordinates cellularChainCoord the cellular differential is right multiplication by the incidence coefficient of c in the boundary of c'.