Coning off ordered simplicial chains

Let K be a simplicial complex with linearly ordered vertices, and let v be a vertex. A cell c of K all of whose vertices are smaller than v, and such that adjoining v to c gives a face of K, has a cone c * v, the cell with vertex set c ∪ {v}, in which v is the last vertex. Extending linearly, and sending the cells that cannot be coned off to zero, gives the cone operator TauCeti.OrderedSimplicialChain.cone over any coefficient semiring, built from the cone on a cell AbstractSimplicialComplex.RealizationCell.cone. Over a coefficient ring, on chains supported on cells that can be coned off it satisfies the cone identities

• ∂ (z * v) = ε(z) [v] - z in degree 0, where ε sums the coefficients;
• ∂ (z * v) = (∂ z) * v + (-1) ^ (n + 1) z in degree n ≥ 1.

If every finite set of vertices admits such a cone vertex, every cycle is supported on finitely many vertices and is therefore the boundary of a multiple of its cone: the augmented ordered chain complex of K is exact. The cone vertex is allowed to depend on the cycle, so the argument proves exactness without producing a chain contraction. The main example is Milnor's countable join, where a vertex over an index larger than every index in sight is a cone vertex.

Main definitions

• TauCeti.OrderedSimplicialChain.cone: the cone operator on ordered simplicial chains.

Main results

• TauCeti.OrderedSimplicialChain.boundary_cone_zero, TauCeti.OrderedSimplicialChain.boundary_cone_succ: the cone identities.
• TauCeti.exactAt_orderedSimplicialChainComplex_of_cone: the ordered chain complex is exact in positive degrees when every finite set of vertices has a cone vertex.
• TauCeti.exists_boundary_eq_of_boundary_eq_zero_of_cone, TauCeti.exists_boundary_eq_of_augmentation_eq_zero_of_cone: the same statements for individual chains, in positive degrees and in degree 0.
• TauCeti.quasiIso_orderedSimplicialChainComplexAugmentation_of_cone: the augmentation is a quasi-isomorphism, so the ordered chain complex is a resolution of the coefficient ring.

The proof that the augmentation is a quasi-isomorphism follows the proof of Rep.FiniteCyclicGroup.resolution_quasiIso in Mathlib/RepresentationTheory/Homological/FiniteCyclic.lean.

References

• J. R. Munkres, Elements of Algebraic Topology, Addison-Wesley, 1984, Section 8, the bracket operation and the acyclicity of cones.
• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.

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

The cone operator with cone vertex v on ordered simplicial n-chains: a cell all of whose vertices are smaller than v, and to which v can be adjoined, goes to its cone RealizationCell.cone; every other cell goes to 0.

@[simp]

theorem TauCeti.OrderedSimplicialChain.cone_single {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {R : Type v} [Semiring R] {v : ι} {n : ℕ} (c : K.RealizationCell n) (hlt : ∀ w ∈ ↑↑c, w < v) (hK : insert v ↑↑c ∈ K) (a : R) : (cone R v n) (Finsupp.single c a) = Finsupp.single (c.cone v hlt hK) a

The cone operator sends a multiple of a cell that can be coned off at v to the same multiple of its cone.

@[simp]

theorem TauCeti.OrderedSimplicialChain.cone_single_of_not {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {R : Type v} [Semiring R] {v : ι} {n : ℕ} (c : K.RealizationCell n) (h : ¬((∀ w ∈ ↑↑c, w < v) ∧ insert v ↑↑c ∈ K)) (a : R) : (cone R v n) (Finsupp.single c a) = 0

The cone operator sends a multiple of a cell that cannot be coned off at v to 0.

theorem TauCeti.OrderedSimplicialChain.boundary_cone_zero {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {R : Type v} [Ring R] {v : ι} {z : OrderedSimplicialChain K R 0} (hz : ∀ c ∈ z.support, (∀ w ∈ ↑↑c, w < v) ∧ insert v ↑↑c ∈ K) : (boundary R 0) ((cone R v 0) z) = Finsupp.single (AbstractSimplicialComplex.RealizationCell.vertex K v) ((Finsupp.linearCombination R fun (x : K.RealizationCell 0) => 1) z) - z

The cone identity in degree 0. For a 0-chain supported on vertices smaller than v and joined to v by an edge, the boundary of its cone is its augmentation times [v], minus the chain.

theorem TauCeti.OrderedSimplicialChain.boundary_cone_succ {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {R : Type v} [Ring R] {v : ι} {n : ℕ} {z : OrderedSimplicialChain K R (n + 1)} (hz : ∀ c ∈ z.support, (∀ w ∈ ↑↑c, w < v) ∧ insert v ↑↑c ∈ K) : (boundary R (n + 1)) ((cone R v (n + 1)) z) = (cone R v n) ((boundary R n) z) + (-1) ^ (n + 2) • z

The cone identity in positive degrees. For an (n + 1)-chain supported on cells that can be coned off at v, the boundary of its cone is the cone on its boundary plus (-1) ^ (n + 2) times the chain.

theorem TauCeti.exists_boundary_eq_of_boundary_eq_zero_of_cone {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {R : Type v} [Ring R] (h : ∀ (s : Finset ι), ∃ (v : ι), (∀ w ∈ s, w < v) ∧ ∀ σ ∈ K, σ ⊆ s → insert v σ ∈ K) {n : ℕ} {z : OrderedSimplicialChain K R (n + 1)} (hz : (OrderedSimplicialChain.boundary R n) z = 0) : ∃ (y : OrderedSimplicialChain K R (n + 1 + 1)), (OrderedSimplicialChain.boundary R (n + 1)) y = z

Cycles are boundaries. If every finite set of vertices s has a cone vertex, a vertex v larger than every vertex of s that can be adjoined to every face of K on s, then every ordered (n + 1)-cycle of K is a boundary.

theorem TauCeti.exists_boundary_eq_of_augmentation_eq_zero_of_cone {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {R : Type v} [Ring R] (h : ∀ (s : Finset ι), ∃ (v : ι), (∀ w ∈ s, w < v) ∧ ∀ σ ∈ K, σ ⊆ s → insert v σ ∈ K) {z : OrderedSimplicialChain K R 0} (hz : (Finsupp.linearCombination R fun (x : K.RealizationCell 0) => 1) z = 0) : ∃ (y : OrderedSimplicialChain K R (0 + 1)), (OrderedSimplicialChain.boundary R 0) y = z

Exactness in degree 0. If every finite set of vertices has a cone vertex, every ordered 0-chain of K whose coefficients sum to zero is a boundary.

theorem TauCeti.exactAt_orderedSimplicialChainComplex_of_cone {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {R : Type v} [Ring R] (h : ∀ (s : Finset ι), ∃ (v : ι), (∀ w ∈ s, w < v) ∧ ∀ σ ∈ K, σ ⊆ s → insert v σ ∈ K) (n : ℕ) : HomologicalComplex.ExactAt (orderedSimplicialChainComplex K R) (n + 1)

The ordered chain complex of a complex in which every finite set of vertices has a cone vertex is exact in every positive degree.

theorem TauCeti.quasiIso_orderedSimplicialChainComplexAugmentation_of_cone {ι : Type u} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {R : Type u} [Ring R] (h : ∀ (s : Finset ι), ∃ (v : ι), (∀ w ∈ s, w < v) ∧ ∀ σ ∈ K, σ ⊆ s → insert v σ ∈ K) : QuasiIso (orderedSimplicialChainComplexAugmentation K R)

The ordered chain complex is a resolution. If every finite set of vertices of K has a cone vertex, a vertex larger than all of them that can be adjoined to every face of K on them, then the augmentation of the ordered chain complex of K is a quasi-isomorphism.