Alexander–Whitney face maps and degree bookkeeping

This file finishes the formalized combinatorial / simplex-level setup needed for the Alexander–Whitney chain-map (Leibniz) identity

δ(φ ⌣ ψ) = δφ ⌣ ψ + (-1)^p φ ⌣ δψ (over ZMod 2 : δ(φ⌣ψ) = δφ⌣ψ + φ⌣δψ)

to be proved in the following modules. It builds directly on the front/back face maps frontFace, backFace of AlexanderWhitney.lean, and on the cochain cup product cochainCup of CupProduct.lean. Every statement below is proved.

What this file supplies

The Leibniz proof telescopes the singular coboundary (δφ)(σ) = Σ_i (-1)^i φ(d_i σ) over the front/back faces. The combinatorial heart is the interaction of the simplicial face maps SimplexCategory.δ k with the front/back inclusions, split by whether the deleted vertex index k is ≤ p (an internal front face) or > p (an internal back face), together with the two endpoint faces whose contributions cancel. This file proves every such identity.

1. Value lemmas succAbove_val', δ_toOrderHom_val, awCastLeft_val: pointwise (vertex-value) descriptions of Fin.succAbove, the face map SimplexCategory.δ, and the degree-cast isomorphism.

2. Degree bookkeeping aw_degree_left_succ, aw_degree_right_succ, cochainCup_degree, and the object-level cast awDegLeft / awCastLeft bridging ⦋p+1+q⦌ and ⦋p+q+1⦌ (these are propositionally but not definitionally equal, while ⦋p+(q+1)⦌ = ⦋p+q+1⦌ is definitional).

3. Internal face-composition identities frontFace_comp_δ_of_le, frontFace_comp_δ_of_gt, backFace_comp_δ_of_le, backFace_comp_δ_of_gt: for a deleted vertex k : Fin (p+q+2) of a (p+q+1)-simplex, how the front p-face / back q-face of the k-th boundary face is expressed via a front/back face of σ itself, with the k ≤ p vs p < k split.

4. Endpoint identities aw_endpoint_front, aw_endpoint_back and their combination aw_internal_face_cancel_pair: the two boundary faces (the top face of the front, and the bottom face of the back) that produce the same front/back restriction pair (frontFace p (q+1), backFace (p+1) q), hence cancel in the Leibniz sum.

5. Simplex-level corollaries faceSimplex, frontSimplex_faceSimplex_of_gt, backSimplex_faceSimplex_of_le: the cast-free restriction identities on singular simplices that the project plugs directly into the cochain computation.

Sign convention

The combinatorial identities here are sign-free; the Koszul signs (-1)^i enter only at the cochain coboundary level. Over ZMod 2 all signs are 1, so the same identities give the characteristic-two Leibniz rule with no extra work.

1. Value lemmas for Fin.succAbove and the face map

theorem SphereOddDegree.AlexanderWhitney.succAbove_val' (n : ℕ) (k : Fin (n + 1)) (i : Fin n) : ↑(k.succAbove i) = if ↑i < ↑k then ↑i else ↑i + 1

The vertex value of Fin.succAbove k i: it is i if i < k and i + 1 otherwise. This is the arithmetic content of "delete the k-th vertex".

@[simp]

theorem SphereOddDegree.AlexanderWhitney.δ_toOrderHom_val {n : ℕ} (k : Fin (n + 2)) (x : Fin (n + 1)) : ↑((SimplexCategory.Hom.toOrderHom (SimplexCategory.δ k)) x) = if ↑x < ↑k then ↑x else ↑x + 1

The vertex value of the face map SimplexCategory.δ k applied to a vertex x: it deletes the k-th vertex, sending x to x if x < k and to x + 1 otherwise.

2. Degree bookkeeping

theorem SphereOddDegree.AlexanderWhitney.aw_degree_left_succ (p q : ℕ) : p + 1 + q = p + q + 1

Degree arithmetic for the left (front) coboundary term: incrementing the front degree p raises the total (p+q)-degree by one. Stated as p+1+q (the degree of δφ ⌣ ψ) equals (p+q)+1 (the degree of δ(φ ⌣ ψ)).

theorem SphereOddDegree.AlexanderWhitney.aw_degree_right_succ (p q : ℕ) : p + (q + 1) = p + q + 1

Degree arithmetic for the right (back) coboundary term: incrementing the back degree q raises the total (p+q)-degree by one. Here p+(q+1) (the degree of φ ⌣ δψ) is definitionally (p+q)+1.

theorem SphereOddDegree.AlexanderWhitney.cochainCup_degree (p q : ℕ) : p + q + 1 = p + 1 + q ∧ p + q + 1 = p + (q + 1)

Output / coboundary degree bookkeeping for the cup product. The cup product cochainCup p q φ ψ has output degree p + q, and the coboundary δ(φ ⌣ ψ) lives in degree (p+q)+1, which equals both (p+1)+q (the degree of δφ ⌣ ψ) and p+(q+1) (the degree of φ ⌣ δψ). This is the degree compatibility that the Leibniz identity needs.

theorem SphereOddDegree.AlexanderWhitney.awDegLeft (p q : ℕ) : { len := p + 1 + q } = { len := p + q + 1 }

The object-level degree equality ⦋p+1+q⦌ = ⦋p+q+1⦌ in SimplexCategory (propositional, not definitional).

def SphereOddDegree.AlexanderWhitney.awCastLeft (p q : ℕ) : { len := p + 1 + q } ⟶ { len := p + q + 1 }

The degree-cast isomorphism ⦋p+1+q⦌ ⟶ ⦋p+q+1⦌, used to bridge the δφ ⌣ ψ summand (degree (p+1)+q) with the δ(φ ⌣ ψ) summand (degree (p+q)+1).

Equations

• SphereOddDegree.AlexanderWhitney.awCastLeft p q = CategoryTheory.eqToHom ⋯

@[simp]

theorem SphereOddDegree.AlexanderWhitney.awCastLeft_val (p q : ℕ) (x : Fin (p + 1 + q + 1)) : ↑((SimplexCategory.Hom.toOrderHom (awCastLeft p q)) x) = ↑x

The degree cast awCastLeft is a relabelling: it preserves vertex values.

3. Internal face-composition identities

For a (p+q+1)-simplex σ, deleting its k-th vertex (k : Fin (p+q+2)) gives a (p+q)-simplex d_k σ. The front p-face and back q-face of d_k σ are computed below by composing frontFace/backFace with SimplexCategory.δ k in SimplexCategory, split according to whether k ≤ p (deleted vertex lies in the front block) or p < k (deleted vertex lies in the back block).

theorem SphereOddDegree.AlexanderWhitney.frontFace_comp_δ_of_le (p q : ℕ) (k : Fin (p + q + 2)) (hk : ↑k ≤ p) : CategoryTheory.CategoryStruct.comp (frontFace p q) (SimplexCategory.δ k) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ ⟨↑k, ⋯⟩) (CategoryTheory.CategoryStruct.comp (frontFace (p + 1) q) (awCastLeft p q))

Internal front face, k ≤ p. Deleting a vertex k ≤ p from σ and then taking the front p-face is the same as taking the front (p+1)-face of σ and then deleting vertex k (reindexed into ⦋p⦌ ⟶ ⦋p+1⦌), up to the degree cast.

theorem SphereOddDegree.AlexanderWhitney.frontFace_comp_δ_of_gt (p q : ℕ) (k : Fin (p + q + 2)) (hk : p < ↑k) : CategoryTheory.CategoryStruct.comp (frontFace p q) (SimplexCategory.δ k) = frontFace p (q + 1)

Internal front face, p < k. Deleting a vertex k > p from σ does not disturb the front p-block, so the front p-face of d_k σ equals the front p-face of σ (now viewed inside the (p+(q+1))-simplex σ).

theorem SphereOddDegree.AlexanderWhitney.backFace_comp_δ_of_le (p q : ℕ) (k : Fin (p + q + 2)) (hk : ↑k ≤ p) : CategoryTheory.CategoryStruct.comp (backFace p q) (SimplexCategory.δ k) = CategoryTheory.CategoryStruct.comp (backFace (p + 1) q) (awCastLeft p q)

Internal back face, k ≤ p. Deleting a vertex k ≤ p from σ does not disturb the back q-block (its vertices are ≥ p), so the back q-face of d_k σ equals the back q-face of σ with the block shifted by one (backFace (p+1) q), up to the degree cast.

theorem SphereOddDegree.AlexanderWhitney.backFace_comp_δ_of_gt (p q : ℕ) (k : Fin (p + q + 2)) (hk : p < ↑k) : CategoryTheory.CategoryStruct.comp (backFace p q) (SimplexCategory.δ k) = CategoryTheory.CategoryStruct.comp (SimplexCategory.δ ⟨↑k - p, ⋯⟩) (backFace p (q + 1))

Internal back face, p < k. Deleting a vertex k > p from σ and then taking the back q-face is the same as taking the back q-face of the (p+(q+1))-simplex σ and then deleting vertex k - p (reindexed into ⦋q⦌ ⟶ ⦋q+1⦌).

4. Endpoint identities and their cancellation

In the Leibniz sum the term i = p+1 of δφ ⌣ ψ and the term j = 0 of φ ⌣ δψ both produce the restriction pair (frontFace p (q+1), backFace (p+1) q) (up to the degree cast), with opposite Koszul signs, and so cancel. The two identities below witness exactly this matching.

theorem SphereOddDegree.AlexanderWhitney.aw_endpoint_front (p q : ℕ) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.last (p + 1))) (CategoryTheory.CategoryStruct.comp (frontFace (p + 1) q) (awCastLeft p q)) = frontFace p (q + 1)

Front endpoint. Deleting the top vertex of the front (p+1)-face recovers the front p-face: δ (last) ≫ frontFace (p+1) q ≫ cast = frontFace p (q+1).

theorem SphereOddDegree.AlexanderWhitney.aw_endpoint_back (p q : ℕ) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ 0) (backFace p (q + 1)) = CategoryTheory.CategoryStruct.comp (backFace (p + 1) q) (awCastLeft p q)

Back endpoint. Deleting the bottom vertex of the back (q+1)-face recovers the back q-face (block shifted by one): δ 0 ≫ backFace p (q+1) = backFace (p+1) q ≫ cast.

theorem SphereOddDegree.AlexanderWhitney.aw_internal_face_cancel_pair (p q : ℕ) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ (Fin.last (p + 1))) (CategoryTheory.CategoryStruct.comp (frontFace (p + 1) q) (awCastLeft p q)) = frontFace p (q + 1) ∧ CategoryTheory.CategoryStruct.comp (SimplexCategory.δ 0) (backFace p (q + 1)) = CategoryTheory.CategoryStruct.comp (backFace (p + 1) q) (awCastLeft p q)

Endpoint cancellation pair. The front endpoint (top face of the front (p+1)-block) and the back endpoint (bottom face of the back (q+1)-block) produce the same front/back restriction pair (frontFace p (q+1), backFace (p+1) q). In the signed Leibniz sum these two contributions carry opposite signs and cancel; over ZMod 2 they coincide and cancel mod 2.

5. Simplex-level restriction corollaries

Applying (TopCat.toSSet.obj X).map to the cast-free face-composition identities gives the restriction identities on singular simplices that the cochain computation of the project uses directly. The two k > p cases (front and back) are cast-free (no degree relabelling), so they are recorded here in their cleanest form. The cast-involving (k ≤ p, endpoint) cases are obtained in the project by applying (TopCat.toSSet.obj X).map to the morphism identities of §3–§4.

noncomputable def SphereOddDegree.AlexanderWhitney.faceSimplex (X : TopCat) (n : ℕ) (k : Fin (n + 2)) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n + 1 })) : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })

The k-th boundary face of a singular (n+1)-simplex σ, obtained by restricting σ along SimplexCategory.δ k.

Equations

• SphereOddDegree.AlexanderWhitney.faceSimplex X n k σ = (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map (SimplexCategory.δ k).op)) σ

theorem SphereOddDegree.AlexanderWhitney.frontSimplex_faceSimplex_of_gt (X : TopCat) (p q : ℕ) (k : Fin (p + q + 2)) (hk : p < ↑k) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q + 1 })) : frontSimplex X p q (faceSimplex X (p + q) k σ) = frontSimplex X p (q + 1) σ

Simplex-level internal front face, p < k. The front p-face of the k-th boundary face of σ (for k > p) equals the front p-face of σ.

theorem SphereOddDegree.AlexanderWhitney.backSimplex_faceSimplex_of_gt (X : TopCat) (p q : ℕ) (k : Fin (p + q + 2)) (hk : p < ↑k) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q + 1 })) : backSimplex X p q (faceSimplex X (p + q) k σ) = faceSimplex X q ⟨↑k - p, ⋯⟩ (backSimplex X p (q + 1) σ)

Simplex-level internal back face, p < k. The back q-face of the k-th boundary face of σ (for k > p) equals the (k-p)-th boundary face of the back (q+1)-face of σ.