Definition 7: Cell Complex #

A regular cell complex X consists of finite sets X_n for each n ∈ ℤ (with X_n = ∅ for all but finitely many n), whose elements are called n-cells, together with for each n-cell σ ∈ X_n a subset ∂σ ⊆ X_{n-1} (the set of (n-1)-cells in the boundary of σ).

The associated chain complex C(X) = (C_•(X), ∂) is defined by C_i(X) = ⊕_{σ ∈ X_i} 𝔽₂ σ (the free 𝔽₂-vector space on X_i) and the differential ∂_n(σ) = Σ_{τ ∈ ∂σ} τ for each n-cell σ ∈ X_n, extended linearly. This satisfies the chain complex condition ∂_{n-1} ∘ ∂_n = 0.

The homology of the cell complex is H_i(X) = H_i(C(X)).

Main Definitions #

CellComplex — a regular cell complex with finite cell sets and boundary maps
CellComplex.differentialMap — the differential ∂_n : C_n(X) → C_{n-1}(X) as a linear map
CellComplex.differentialMap_comp — proof that ∂_{n-1} ∘ ∂_n = 0
CellComplex.chainComplex — the associated chain complex C(X)
CellComplex.cellHomology — the homology H_i(X) = H_i(C(X))

Cell Complex Structure #

source

structure CellComplex :

Type 1

A regular cell complex X consists of finite sets X_n for each n ∈ ℤ, whose elements are called n-cells, together with for each n-cell σ ∈ X_n a subset ∂σ ⊆ X_{n-1} (the boundary of σ). The chain complex condition requires ∂_{n-1} ∘ ∂_n = 0, which is encoded as: for every n-cell σ and every (n-2)-cell ρ, the number of (n-1)-cells τ with τ ∈ ∂σ and ρ ∈ ∂τ is even.

cells : ℤ → Type
The type of n-cells for each n ∈ ℤ.
cells_fintype (n : ℤ) : Fintype (self.cells n)
Each cells n is a finite type.
cells_deceq (n : ℤ) : DecidableEq (self.cells n)
Each cells n has decidable equality.
bdry {n : ℤ} : self.cells n → Finset (self.cells (n - 1))
The boundary map: for each n-cell σ, the set of (n-1)-cells in ∂σ.
bdry_bdry (n : ℤ) (σ : self.cells n) (ρ : self.cells (n - 1 - 1)) : Even {τ ∈ self.bdry σ | ρ ∈ self.bdry τ}.card
The chain complex condition: for every n-cell σ and every (n-2)-cell ρ, the number of (n-1)-cells τ with τ ∈ ∂σ and ρ ∈ ∂τ is even.

Instances For

The differential as a linear map #

source

noncomputable def CellComplex.differentialMap (X : CellComplex) (n : ℤ) :

(X.cells n → 𝔽₂) →ₗ[𝔽₂ ] X.cells (n - 1) → 𝔽₂

The differential ∂_n : C_n(X) → C_{n-1}(X) of the cell complex, defined by ∂_n(f)(τ) = Σ_{σ : X_n | τ ∈ ∂σ} f(σ) for τ ∈ X_{n-1}. Equivalently, on a basis element eσ, ∂_n(eσ) = Σ_{τ ∈ ∂σ} eτ. Here C_i(X) = cells i → 𝔽₂ is the free 𝔽₂-vector space on X_i.

Equations

X.differentialMap n = LinearMap.pi fun (τ : X.cells (n - 1)) => ∑ σ : X.cells n with τ ∈ X.bdry σ, LinearMap.proj σ

Instances For

source

@[simp]

theorem CellComplex.differentialMap_apply (X : CellComplex) (n : ℤ) (f : X.cells n → 𝔽₂) (τ : X.cells (n - 1)) :

(X.differentialMap n) f τ = ∑ σ : X.cells n with τ ∈ X.bdry σ, f σ

Chain complex condition: ∂_{n-1} ∘ ∂_n = 0 #

source

theorem CellComplex.differentialMap_comp (X : CellComplex) (n : ℤ) :

X.differentialMap (n - 1) ∘ₗ X.differentialMap n = 0

The chain complex condition ∂_{n-1} ∘ ∂_n = 0. This follows from the even boundary condition: for every n-cell σ and every (n-2)-cell ρ, the number of (n-1)-cells τ with τ ∈ ∂σ and ρ ∈ ∂τ is even.

The chain complex C(X) #

source

noncomputable def CellComplex.chainComplex (X : CellComplex) :

ChainComplex𝔽₂

The associated chain complex C(X) = (C_•(X), ∂) of a cell complex X. The module in degree i is C_i(X) = cells i → 𝔽₂ (the free 𝔽₂-vector space on the i-cells), and the differential ∂_n maps eσ ↦ Σ_{τ ∈ ∂σ} eτ.

Equations