Alexander–Whitney cochain chain-map (Leibniz) identity

This file proves the formalized Alexander–Whitney chain-map / Leibniz identity for the cochain-level singular cup product, over ZMod 2 coefficients (where the Koszul signs are trivial):

δ(φ ⌣ ψ) = δφ ⌣ ψ + φ ⌣ δψ.

This is the central algebraic identity that descends the cochain cup product cochainCup of CupProduct.lean to a cohomology-level product. Every statement in this module is proved.

Strategy

The singular cochain coboundary δ = d^p : C^p → C^{p+1} is, by construction, precomposition with the singular chain boundary ∂ = Σ_i (-1)^i d_i (cochainCoboundary_eval). Telescoping δ(φ ⌣ ψ) over the boundary faces and splitting by the position of the deleted vertex relative to the cup split point p uses the four face-composition identities of AlexanderWhitneyFaceMaps.lean (frontFace_comp_δ_of_le/_gt, backFace_comp_δ_of_le/_gt) and the two endpoint identities (aw_endpoint_front, aw_endpoint_back). The two endpoint faces produce the same restriction pair and cancel; over ZMod 2 they coincide and cancel mod 2.

Degree bookkeeping

The three terms naturally live in degrees (p+q)+1, (p+1)+q and p+(q+1). Now p+(q+1) is definitionally (p+q)+1, but (p+1)+q is only propositionally equal to it, so the δφ ⌣ ψ term is transported along the degree equality via the cochain degree cast cochainCast.

Main results

• cochainCoboundary / cochainCoboundary_eval — the cochain coboundary and its alternating-face evaluation formula.
• aw_cochain_leibniz_zmod2 — the Leibniz / chain-map identity over ZMod 2.

0. The underlying simplicial module of the singular chain complex

noncomputable def SphereOddDegree.singularChainSimplicialModule (R : Type) [CommRing R] (Z : TopCat) : CategoryTheory.SimplicialObject (ModuleCat R)

The free R-module simplicial object whose alternating face map complex is the singular chain complex C_•(Z; R). Its value in degree n is the coproduct ∐_{σ : n-simplex} R.

Equations

• SphereOddDegree.singularChainSimplicialModule R Z = ((CategoryTheory.Limits.sigmaConst.comp (CategoryTheory.SimplicialObject.whiskering Type (ModuleCat R))).obj ↧R).obj (TopCat.toSSet.obj Z)

theorem SphereOddDegree.singularChainSimplicialModule_map_generator (R : Type) [CommRing R] (X : TopCat) (m m' : ℕ) (g : Opposite.op { len := m' } ⟶ Opposite.op { len := m }) (σ : singularSimplices X m') : (ModuleCat.Hom.hom ((singularChainSimplicialModule R X).map g)) ((ModuleCat.Hom.hom (CategoryTheory.Limits.Sigma.ι (fun (x : singularSimplices X m') => ↧R) σ)) 1) = (ModuleCat.Hom.hom (CategoryTheory.Limits.Sigma.ι (fun (x : singularSimplices X m) => ↧R) ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map g)) σ))) 1

A morphism in SimplexCategoryᵒᵖ acts on the singular chain simplicial module by sending a basis generator to the basis generator at the restricted simplex.

theorem SphereOddDegree.singularChainSimplicialModule_δ_generator (R : Type) [CommRing R] (Z : TopCat) (n : ℕ) (i : Fin (n + 2)) (σ : singularSimplices Z (n + 1)) : (ModuleCat.Hom.hom ((singularChainSimplicialModule R Z).δ i)) ((ModuleCat.Hom.hom (CategoryTheory.Limits.Sigma.ι (fun (x : singularSimplices Z (n + 1)) => ↧R) σ)) 1) = (ModuleCat.Hom.hom (CategoryTheory.Limits.Sigma.ι (fun (x : singularSimplices Z n) => ↧R) (AlexanderWhitney.faceSimplex Z n i σ))) 1

The simplicial face map δ i of the singular chain simplicial module sends the basis generator at a simplex σ to the basis generator at its i-th boundary face d_i σ = faceSimplex Z n i σ.

1. The cochain coboundary and its evaluation formula

noncomputable def SphereOddDegree.cochainCoboundary (R : Type) [CommRing R] (Z : TopCat) (p : ℕ) (φ : singularCochainGroup R Z p) : singularCochainGroup R Z (p + 1)

The cochain coboundary δ = d^p : C^p(Z; R) → C^{p+1}(Z; R), the differential of the singular cochain complex. By construction it is precomposition with the singular chain boundary.

Equations

• SphereOddDegree.cochainCoboundary R Z p φ = (ModuleCat.Hom.hom (((SphereOddDegree.singularCochainComplexFunctor R ↧R).obj (Opposite.op Z)).d p (p + 1))) φ

theorem SphereOddDegree.cochainCoboundary_eval (R : Type) [CommRing R] (Z : TopCat) (n : ℕ) (φ : singularCochainGroup R Z n) (σ : singularSimplices Z (n + 1)) : cochainEval (n + 1) (cochainCoboundary R Z n φ) σ = ∑ i : Fin (n + 2), (-1) ^ ↑i * cochainEval n φ (AlexanderWhitney.faceSimplex Z n i σ)

Coboundary evaluation formula. The coboundary δφ of a p-cochain φ, evaluated on a (p+1)-simplex σ, is the alternating sum of φ over the boundary faces: (δφ)(σ) = Σ_i (-1)^i φ(d_i σ).

2. The degree cast on cochains and the cast singular simplex

noncomputable def SphereOddDegree.cochainCast {R : Type} [CommRing R] {Z : TopCat} {m m' : ℕ} (h : m = m') (φ : singularCochainGroup R Z m) : singularCochainGroup R Z m'

The cochain degree cast transporting a cochain along an equality of degrees m = m'. Needed because (p+1)+q and (p+q)+1 are only propositionally equal.

Equations

• SphereOddDegree.cochainCast h φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) φ

noncomputable def SphereOddDegree.awCastSimplex (X : TopCat) (p q : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q + 1 })) : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + 1 + q })

The singular (p+q+1)-simplex σ relabelled as a (p+1+q)-simplex via the degree cast awCastLeft. This is the cast simplex on which the δφ ⌣ ψ term is evaluated.

Equations

• SphereOddDegree.awCastSimplex X p q σ = (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map (SphereOddDegree.AlexanderWhitney.awCastLeft p q).op)) σ

theorem SphereOddDegree.cochainCast_eval_awCastSimplex (R : Type) [CommRing R] (X : TopCat) (p q : ℕ) (χ : singularCochainGroup R X (p + 1 + q)) (σ : singularSimplices X (p + q + 1)) : cochainEval (p + q + 1) (cochainCast ⋯ χ) σ = cochainEval (p + 1 + q) χ (awCastSimplex X p q σ)

Evaluation of the degree-cast cochain. Evaluating cochainCast of the δφ ⌣ ψ term on σ equals evaluating the original cochain on the cast simplex awCastSimplex X p q σ.

theorem SphereOddDegree.cochainCast_eval_right (R : Type) [CommRing R] (X : TopCat) (p q : ℕ) (χ : singularCochainGroup R X (p + (q + 1))) (σ : singularSimplices X (p + q + 1)) : cochainEval (p + q + 1) (cochainCast ⋯ χ) σ = cochainEval (p + (q + 1)) χ σ

Evaluation of the right (definitional) degree cast. Since p+(q+1) is definitionally (p+q)+1, the φ ⌣ δψ cast is the identity.

3. Simplex-level face identities (cast versions)

The two k > p cases are already cast-free in AlexanderWhitneyFaceMaps.lean (frontSimplex_faceSimplex_of_gt, backSimplex_faceSimplex_of_gt). Here we add the k ≤ p cases and the two endpoint identities, both of which involve the degree cast simplex awCastSimplex.

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

Simplex-level internal front face, k ≤ p.

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

Simplex-level internal back face, k ≤ p. Independent of k.

theorem SphereOddDegree.frontSimplex_faceSimplex_endpoint (X : TopCat) (p q : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q + 1 })) : AlexanderWhitney.faceSimplex X p (Fin.last (p + 1)) (AlexanderWhitney.frontSimplex X (p + 1) q (awCastSimplex X p q σ)) = AlexanderWhitney.frontSimplex X p (q + 1) σ

Front endpoint identity (simplex level). The top boundary face of the front (p+1)-face of the cast simplex recovers the front p-face of σ.

theorem SphereOddDegree.backSimplex_faceSimplex_endpoint (X : TopCat) (p q : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q + 1 })) : AlexanderWhitney.faceSimplex X q 0 (AlexanderWhitney.backSimplex X p (q + 1) σ) = AlexanderWhitney.backSimplex X (p + 1) q (awCastSimplex X p q σ)

Back endpoint identity (simplex level). The bottom boundary face of the back (q+1)-face of σ recovers the back q-face of the cast simplex.

4. An abstract char-2 sum-splitting lemma

theorem SphereOddDegree.sum_split_char2 {M : Type} [AddCommGroup M] (htwo : ∀ (x : M), x + x = 0) (p q : ℕ) (L : Fin (p + q + 2) → M) (A : Fin (p + 2) → M) (B : Fin (q + 2) → M) (hle : ∀ (k : Fin (p + q + 2)) (hk : ↑k ≤ p), L k = A ⟨↑k, ⋯⟩) (hgt : ∀ (k : Fin (p + q + 2)) (hk : p < ↑k), L k = B ⟨↑k - p, ⋯⟩) (hend : A (Fin.last (p + 1)) = B 0) : ∑ k : Fin (p + q + 2), L k = ∑ i : Fin (p + 2), A i + ∑ j : Fin (q + 2), B j

Abstract characteristic-two sum split. If a function L on Fin (p+q+2) matches A on the front block k ≤ p, matches B on the back block k > p, and the two endpoints A (last) and B 0 coincide, then in a 2-torsion abelian group ∑ L = ∑ A + ∑ B (the endpoints cancel mod 2).

5. The Leibniz identity over ZMod 2

theorem SphereOddDegree.neg_one_pow_zmod2 (k : ℕ) : (-1) ^ k = 1

Over ZMod 2, the coefficient sign (-1)^k is 1.

theorem SphereOddDegree.aw_cochain_leibniz_zmod2 {X : TopCat} (p q : ℕ) (φ : singularCochainGroup (ZMod 2) X p) (ψ : singularCochainGroup (ZMod 2) X q) : cochainCoboundary (ZMod 2) X (p + q) (cochainCup p q φ ψ) = cochainCast ⋯ (cochainCup (p + 1) q (cochainCoboundary (ZMod 2) X p φ) ψ) + cochainCast ⋯ (cochainCup p (q + 1) φ (cochainCoboundary (ZMod 2) X q ψ))

Alexander–Whitney cochain Leibniz identity over ZMod 2.

The cochain coboundary is a derivation for the cup product (over ZMod 2, where all Koszul signs are trivial):

δ(φ ⌣ ψ) = δφ ⌣ ψ + φ ⌣ δψ.

This is the chain-map identity that lets the cup product descend to cohomology. The δφ ⌣ ψ term, naturally of degree (p+1)+q, and the φ ⌣ δψ term, of degree p+(q+1), are transported to degree (p+q)+1 via the cochain degree cast.