The ordered simplicial chain complex

For a simplicial complex with linearly ordered vertices, its simplicial chains are the free modules on the faces of each dimension. The boundary of a face with increasing vertex list [v₀, ..., vₙ] is the alternating sum of the faces obtained by deleting one vertex:

∂[v₀, ..., vₙ] = ∑ j, (-1) ^ j [v₀, ..., v̂ⱼ, ..., vₙ].

This file packages the alternating boundary as a chain complex over any coefficient ring. The signs are central, so the coefficient ring need not be commutative.

The comparison with the cellular chain complex of the realization is separate. Both complexes are indexed by RealizationCell, so that comparison reduces to computing the cellular incidence coefficients in these ordered coordinates. The support of each simplicial cell boundary is identified explicitly with its codimension-one faces.

Main definitions

• TauCeti.OrderedSimplicialChain: finite linear combinations of ordered simplicial cells.
• TauCeti.OrderedSimplicialChain.boundary: the alternating simplicial boundary.
• TauCeti.orderedSimplicialChainComplex: the resulting chain complex of modules.
• TauCeti.orderedSimplicialChainComplexAugmentation: the augmentation of the ordered chain complex, a chain map to the coefficient ring in degree 0.

References

• A. Hatcher, Algebraic Topology, Section 2.1.

@[reducible, inline]

abbrev TauCeti.OrderedSimplicialChain {ι : Type u} (K : AbstractSimplicialComplex ι) (R : Type v) [Semiring R] (n : ℕ) : Type (max u v)

Ordered simplicial n-chains with coefficients in R: finite linear combinations of the n-dimensional faces, oriented by their increasing vertex enumerations.

noncomputable def TauCeti.OrderedSimplicialChain.boundaryCell {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] {n : ℕ} (c : K.RealizationCell (n + 1)) : OrderedSimplicialChain K R n

The boundary of a single (n + 1)-dimensional simplicial cell is the alternating sum of its deleted-vertex faces.

@[simp]

theorem TauCeti.OrderedSimplicialChain.boundaryCell_apply_face {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] {n : ℕ} (c : K.RealizationCell (n + 1)) (j : Fin (n + 2)) : (boundaryCell R c) (c.face j) = (-1) ^ ↑j

The coefficient of a codimension-one face in the boundary of a cell is its alternating sign.

theorem TauCeti.OrderedSimplicialChain.boundaryCell_apply_eq_zero_of_not_subset {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] {n : ℕ} (c : K.RealizationCell (n + 1)) (d : K.RealizationCell n) (h : ¬↑↑d ⊆ ↑↑c) : (boundaryCell R c) d = 0

A cell which is not a codimension-one subface has coefficient zero in the boundary.

@[simp]

theorem TauCeti.OrderedSimplicialChain.boundaryCell_apply_ne_zero_iff {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] [Nontrivial R] {n : ℕ} (c : K.RealizationCell (n + 1)) (d : K.RealizationCell n) : (boundaryCell R c) d ≠ 0 ↔ ↑↑d ⊆ ↑↑c

A cell has nonzero boundary coefficient exactly when it is a codimension-one subface.

theorem TauCeti.OrderedSimplicialChain.support_boundaryCell {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] [Nontrivial R] {n : ℕ} (c : K.RealizationCell (n + 1)) : (boundaryCell R c).support = Finset.image c.face Finset.univ

The support of a cell boundary is precisely the set of its codimension-one faces.

theorem TauCeti.OrderedSimplicialChain.boundaryCell_def {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] {n : ℕ} (c : K.RealizationCell (n + 1)) : boundaryCell R c = ∑ j : Fin (n + 2), (-1) ^ ↑j • Finsupp.single (c.face j) 1

The explicit alternating-sum formula for the boundary of one cell.

noncomputable def TauCeti.OrderedSimplicialChain.boundary {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] (n : ℕ) : OrderedSimplicialChain K R (n + 1) →ₗ[R] OrderedSimplicialChain K R n

The ordered simplicial boundary, extended linearly from cells.

theorem TauCeti.OrderedSimplicialChain.boundary_single_one {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] {n : ℕ} (c : K.RealizationCell (n + 1)) : (boundary R n) (Finsupp.single c 1) = boundaryCell R c

The boundary of a cell with coefficient one is its alternating deleted-face sum.

@[simp]

theorem TauCeti.OrderedSimplicialChain.boundary_single {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] {n : ℕ} (c : K.RealizationCell (n + 1)) (a : R) : (boundary R n) (Finsupp.single c a) = ∑ j : Fin (n + 2), (-1) ^ ↑j • Finsupp.single (c.face j) a

The boundary of a scalar multiple of a cell is the corresponding alternating sum with that coefficient on every face.

theorem TauCeti.OrderedSimplicialChain.boundary_boundary {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] (n : ℕ) : boundary R n ∘ₗ boundary R (n + 1) = 0

The boundary of a boundary vanishes.

theorem TauCeti.OrderedSimplicialChain.augmentation_comp_boundary {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] : (Finsupp.linearCombination R fun (x : K.RealizationCell 0) => 1) ∘ₗ boundary R 0 = 0

The coefficients of the boundary of a 1-chain sum to zero.

noncomputable def TauCeti.orderedSimplicialChainComplex {ι : Type u} [LinearOrder ι] (K : AbstractSimplicialComplex ι) (R : Type v) [Ring R] : ChainComplex (ModuleCat R) ℕ

The ordered simplicial chain complex of K, with one basis vector for every face and the usual alternating deleted-vertex boundary.

@[simp]

theorem TauCeti.orderedSimplicialChainComplex_X {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] (n : ℕ) : (orderedSimplicialChainComplex K R).X n = ↧(OrderedSimplicialChain K R n)

The object in degree n of the ordered simplicial chain complex is the free module on the n-dimensional faces.

@[simp]

theorem TauCeti.orderedSimplicialChainComplex_d {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] (n : ℕ) : (orderedSimplicialChainComplex K R).d (n + 1) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (OrderedSimplicialChain.boundary R n)) (CategoryTheory.eqToHom ⋯))

After identifying the objects with the free modules on cells, the differential of the ordered simplicial chain complex is the alternating simplicial boundary.

theorem TauCeti.exact_orderedSimplicialChainComplex_d_iff {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (R : Type v) [Ring R] {n : ℕ} {M N : ModuleCat R} {g : (orderedSimplicialChainComplex K R).X n ⟶ M} (w : CategoryTheory.CategoryStruct.comp ((orderedSimplicialChainComplex K R).d (n + 1) n) g = 0) (e : M ≅ N) {g' : OrderedSimplicialChain K R n →ₗ[R] ↑N} (hg : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp g e.hom) = ModuleCat.ofHom g') : { X₁ := (orderedSimplicialChainComplex K R).X (n + 1), X₂ := (orderedSimplicialChainComplex K R).X n, X₃ := M, f := (orderedSimplicialChainComplex K R).d (n + 1) n, g := g, zero := w }.Exact ↔ ∀ (z : OrderedSimplicialChain K R n), g' z = 0 → ∃ (y : OrderedSimplicialChain K R (n + 1)), (OrderedSimplicialChain.boundary R n) y = z

A short complex of modules whose first map is the differential X (n + 1) ⟶ X n of the ordered chain complex is exact exactly when every n-chain killed by its second map is a boundary. Here the second map is read on chains as g', through an isomorphism e of its target.

noncomputable def TauCeti.orderedSimplicialChainComplexAugmentation {ι : Type u} [LinearOrder ι] (K : AbstractSimplicialComplex ι) (R : Type u) [Ring R] : orderedSimplicialChainComplex K R ⟶ (ChainComplex.single₀ (ModuleCat R)).obj ↧R

The augmentation of the ordered chain complex: the chain map to R, placed in degree 0, that sums the coefficients of a 0-chain.

@[simp]

theorem TauCeti.orderedSimplicialChainComplexAugmentation_f_zero {ι : Type u} [LinearOrder ι] (K : AbstractSimplicialComplex ι) (R : Type u) [Ring R] : (orderedSimplicialChainComplexAugmentation K R).f 0 = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.linearCombination R fun (x : K.RealizationCell 0) => 1)) (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 ↧R).inv)

In degree 0 the augmentation sums the coefficients.