Cochain-level singular cup product (Alexander–Whitney formula)

This file builds a genuine, formalized cochain-level singular cup product from the Alexander–Whitney front/back faces of AlexanderWhitney.lean. There are

What is and is not here

Pinned Mathlib (v4.28.0, commit 8f9d9cff6bd728b17a24e163c9402775d9e6a365) has no cup product. The genuine topological input — the Alexander–Whitney front/back faces — is supplied by AlexanderWhitney.lean. Using the definitional facts

• a singular chain group in degree n is the coproduct C_n(X) = ∐_{σ : n-simplex} R (rfl), so an R-linear map out of it is determined by its values on the generators (cochain_ext);
• a singular cochain in degree p is exactly a morphism C_p(X) ⟶ R (rfl);
• the pullback of a cochain is precomposition with the singular chain map (rfl),

we define the cochain cup product by the classical Alexander–Whitney formula

(φ ⌣ ψ)(σ) = φ(front_p σ) · ψ(back_q σ) (σ a (p+q)-simplex)

with coefficients in the ring R itself (M = R, which covers the downstream R = ZMod 2 case). The operation is genuine, R-bilinear, natural in the space, strictly unital on the right, and assembled into degree-n powers of a degree-one cochain.

What is NOT here (the exact required input). The descent to cohomology (H^p × H^q → H^{p+q}) requires the Leibniz / coboundary identity

δ(φ ⌣ ψ) = (δφ) ⌣ ψ + (-1)^p φ ⌣ (δψ),

equivalently that the assembled cochain map C^•(X) ⊗ C^•(X) → C^•(X) is a morphism of cochain complexes. That identity is the standard telescoping argument over the front/back simplicial identities (frontFace_last_eq_backFace_zero, frontFace_succ, backFace_succ_square); it is not proved here, so no cohomology-level cup is introduced (per the project's no-unsupported-declarations policy). See the module footer and

Coefficients

Everything is stated for a general CommRing R, with coefficients in R itself (ModuleCat.of R R). The ZMod 2 specializations (cochainCupZMod2, …) are thin abbreviations; over ZMod 2 the Koszul sign in the Leibniz rule is trivial.

0. Singular simplices and cochains as concrete objects

@[reducible, inline]

abbrev SphereOddDegree.singularSimplices (Z : TopCat) (n : ℕ) : Type

The set of singular n-simplices of a space Z (an element of the singular simplicial set in degree n).

Equations

• SphereOddDegree.singularSimplices Z n = (TopCat.toSSet.obj Z).obj (Opposite.op { len := n })

@[reducible, inline]

abbrev SphereOddDegree.singularCochainGroup (R : Type) [CommRing R] (Z : TopCat) (p : ℕ) : Type

A singular p-cochain of Z with coefficients in the ring R: an R-linear map from the singular chain group C_p(Z) = ∐_{σ} R to R. This is definitionally the degree-p object of the singular cochain complex with coefficients in ModuleCat.of R R.

Equations

• SphereOddDegree.singularCochainGroup R Z p = ((((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj ↧R).obj Z).X p ⟶ ↧R)

1. Evaluation of a cochain on a simplex

noncomputable def SphereOddDegree.cochainEval {R : Type} [CommRing R] {Z : TopCat} (p : ℕ) (φ : singularCochainGroup R Z p) (τ : singularSimplices Z p) : R

Evaluate a singular p-cochain φ on a singular p-simplex τ, i.e. on the basis chain τ (the image of 1 ∈ R under the coproduct inclusion at τ).

Equations

• SphereOddDegree.cochainEval p φ τ = (ModuleCat.Hom.hom φ) ((ModuleCat.Hom.hom (CategoryTheory.Limits.Sigma.ι (fun (x : SphereOddDegree.singularSimplices Z p) => ↧R) τ)) 1)

theorem SphereOddDegree.cochain_ext {R : Type} [CommRing R] {Z : TopCat} {p : ℕ} {φ ψ : singularCochainGroup R Z p} (h : ∀ (τ : singularSimplices Z p), cochainEval p φ τ = cochainEval p ψ τ) : φ = ψ

Cochain extensionality. Two p-cochains are equal iff they agree on every singular p-simplex. (The chain group is a coproduct of copies of R, so a map out of it is determined by its values on the generators.)

@[simp]

theorem SphereOddDegree.cochainEval_add {R : Type} [CommRing R] {Z : TopCat} (p : ℕ) (φ ψ : singularCochainGroup R Z p) (τ : singularSimplices Z p) : cochainEval p (φ + ψ) τ = cochainEval p φ τ + cochainEval p ψ τ

@[simp]

theorem SphereOddDegree.cochainEval_smul {R : Type} [CommRing R] {Z : TopCat} (p : ℕ) (s : R) (φ : singularCochainGroup R Z p) (τ : singularSimplices Z p) : cochainEval p (s • φ) τ = s * cochainEval p φ τ

@[simp]

theorem SphereOddDegree.cochainEval_zero {R : Type} [CommRing R] {Z : TopCat} (p : ℕ) (τ : singularSimplices Z p) : cochainEval p 0 τ = 0

2. The cochain cup product

noncomputable def SphereOddDegree.cochainCup {R : Type} [CommRing R] {Z : TopCat} (p q : ℕ) (φ : singularCochainGroup R Z p) (ψ : singularCochainGroup R Z q) : singularCochainGroup R Z (p + q)

The cochain-level cup product ⌣ : C^p(Z; R) → C^q(Z; R) → C^{p+q}(Z; R), defined by the Alexander–Whitney formula (φ ⌣ ψ)(σ) = φ(front_p σ)·ψ(back_q σ). Built degree-wise out of the singular-chain coproduct via Limits.Sigma.desc.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SphereOddDegree.cochainCup_eval {R : Type} [CommRing R] {Z : TopCat} (p q : ℕ) (φ : singularCochainGroup R Z p) (ψ : singularCochainGroup R Z q) (σ : singularSimplices Z (p + q)) : cochainEval (p + q) (cochainCup p q φ ψ) σ = cochainEval p φ (AlexanderWhitney.frontSimplex Z p q σ) * cochainEval q ψ (AlexanderWhitney.backSimplex Z p q σ)

Defining formula of the cup product. The value of φ ⌣ ψ on a singular (p+q)-simplex σ is φ(front_p σ) · ψ(back_q σ).

Bilinearity

theorem SphereOddDegree.cochainCup_add_left {R : Type} [CommRing R] {Z : TopCat} (p q : ℕ) (φ φ' : singularCochainGroup R Z p) (ψ : singularCochainGroup R Z q) : cochainCup p q (φ + φ') ψ = cochainCup p q φ ψ + cochainCup p q φ' ψ

The cup product is additive in its left argument.

theorem SphereOddDegree.cochainCup_add_right {R : Type} [CommRing R] {Z : TopCat} (p q : ℕ) (φ : singularCochainGroup R Z p) (ψ ψ' : singularCochainGroup R Z q) : cochainCup p q φ (ψ + ψ') = cochainCup p q φ ψ + cochainCup p q φ ψ'

The cup product is additive in its right argument.

theorem SphereOddDegree.cochainCup_smul_left {R : Type} [CommRing R] {Z : TopCat} (p q : ℕ) (s : R) (φ : singularCochainGroup R Z p) (ψ : singularCochainGroup R Z q) : cochainCup p q (s • φ) ψ = s • cochainCup p q φ ψ

The cup product is R-linear in its left argument.

theorem SphereOddDegree.cochainCup_smul_right {R : Type} [CommRing R] {Z : TopCat} (p q : ℕ) (s : R) (φ : singularCochainGroup R Z p) (ψ : singularCochainGroup R Z q) : cochainCup p q φ (s • ψ) = s • cochainCup p q φ ψ

The cup product is R-linear in its right argument.

@[simp]

theorem SphereOddDegree.cochainCup_zero_left {R : Type} [CommRing R] {Z : TopCat} (p q : ℕ) (ψ : singularCochainGroup R Z q) : cochainCup p q 0 ψ = 0

@[simp]

theorem SphereOddDegree.cochainCup_zero_right {R : Type} [CommRing R] {Z : TopCat} (p q : ℕ) (φ : singularCochainGroup R Z p) : cochainCup p q φ 0 = 0

3. Pullback of cochains and naturality of the cup product

noncomputable def SphereOddDegree.cochainPullback {R : Type} [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (p : ℕ) (φ : singularCochainGroup R Y p) : singularCochainGroup R X p

The pullback f^* of a singular p-cochain along a continuous map f : X ⟶ Y, i.e. precomposition with the induced singular chain map.

Equations

• SphereOddDegree.cochainPullback f p φ = (ModuleCat.Hom.hom (((SphereOddDegree.singularCochainComplexFunctor R ↧R).map f.op).f p)) φ

theorem SphereOddDegree.chainmap_generator {R : Type} [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (τ : singularSimplices X n) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : singularSimplices X n) => ↧R) τ) ((((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj ↧R).map f).f n) = CategoryTheory.Limits.Sigma.ι (fun (x : singularSimplices Y n) => ↧R) ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := n }))) τ)

The singular chain map sends the generator at a simplex τ to the generator at its pushforward f ∘ τ.

theorem SphereOddDegree.cochainPullback_eval {R : Type} [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (p : ℕ) (φ : singularCochainGroup R Y p) (τ : singularSimplices X p) : cochainEval p (cochainPullback f p φ) τ = cochainEval p φ ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := p }))) τ)

Pullback evaluation. (f^* φ)(τ) = φ(f ∘ τ).

theorem SphereOddDegree.cochainCup_naturality {R : Type} [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (p q : ℕ) (φ : singularCochainGroup R Y p) (ψ : singularCochainGroup R Y q) : cochainPullback f (p + q) (cochainCup p q φ ψ) = cochainCup p q (cochainPullback f p φ) (cochainPullback f q ψ)

Naturality of the cup product (cochain level). f^*(φ ⌣ ψ) = (f^* φ) ⌣ (f^* ψ). This is the cochain-level substrate for the eventual cohomology-level f^*(a ⌣ b) = f^* a ⌣ f^* b.

4. The unit cochain and right unitality

noncomputable def SphereOddDegree.cochainOne {R : Type} [CommRing R] {Z : TopCat} : singularCochainGroup R Z 0

The unit cochain 1 ∈ C^0(Z; R): the augmentation cochain taking the value 1 on every singular 0-simplex.

Equations

• SphereOddDegree.cochainOne = CategoryTheory.Limits.Sigma.desc fun (x : (TopCat.toSSet.obj Z).obj (Opposite.op { len := 0 })) => CategoryTheory.CategoryStruct.id ↧R

@[simp]

theorem SphereOddDegree.cochainOne_eval {R : Type} [CommRing R] {Z : TopCat} (τ : singularSimplices Z 0) : cochainEval 0 cochainOne τ = 1

@[simp]

theorem SphereOddDegree.frontSimplex_q_zero {Z : TopCat} (p : ℕ) (σ : singularSimplices Z (p + 0)) : AlexanderWhitney.frontSimplex Z p 0 σ = σ

The front p-face inclusion with empty back part is the identity, so the front p-face of a p-simplex is the simplex itself.

@[simp]

theorem SphereOddDegree.cochainCup_one {R : Type} [CommRing R] {Z : TopCat} (p : ℕ) (φ : singularCochainGroup R Z p) : cochainCup p 0 φ cochainOne = φ

Right unitality. φ ⌣ 1 = φ.

5. Powers of a degree-one cochain

noncomputable def SphereOddDegree.cochainPow {R : Type} [CommRing R] {Z : TopCat} (φ : singularCochainGroup R Z 1) (n : ℕ) : singularCochainGroup R Z n

The n-th cup power φ^{⌣ n} ∈ C^n(Z; R) of a degree-one cochain φ ∈ C^1(Z; R), defined by φ^0 = 1 and φ^{n+1} = φ^n ⌣ φ. This is the cochain-level scaffolding for the powers αⁿ of a degree-one cohomology class.

Equations

• SphereOddDegree.cochainPow φ 0 = SphereOddDegree.cochainOne
• SphereOddDegree.cochainPow φ n.succ = SphereOddDegree.cochainCup n 1 (SphereOddDegree.cochainPow φ n) φ

@[simp]

theorem SphereOddDegree.cochainPow_zero {R : Type} [CommRing R] {Z : TopCat} (φ : singularCochainGroup R Z 1) : cochainPow φ 0 = cochainOne

@[simp]

theorem SphereOddDegree.cochainPow_succ {R : Type} [CommRing R] {Z : TopCat} (φ : singularCochainGroup R Z 1) (n : ℕ) : cochainPow φ (n + 1) = cochainCup n 1 (cochainPow φ n) φ

theorem SphereOddDegree.cochainPow_naturality {R : Type} [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (φ : singularCochainGroup R Y 1) (n : ℕ) : cochainPullback f n (cochainPow φ n) = cochainPow (cochainPullback f 1 φ) n

Naturality of powers (cochain level). f^*(φ^n) = (f^* φ)^n.

6. ZMod 2 specializations

The downstream RPⁿ cohomology computation uses ZMod 2 coefficients. These are thin abbreviations of the general definitions.

@[reducible, inline]

noncomputable abbrev SphereOddDegree.cochainCupZMod2 {Z : TopCat} (p q : ℕ) (φ : singularCochainGroup (ZMod 2) Z p) (ψ : singularCochainGroup (ZMod 2) Z q) : singularCochainGroup (ZMod 2) Z (p + q)

The cochain cup product with ZMod 2 coefficients.

Equations

• SphereOddDegree.cochainCupZMod2 p q φ ψ = SphereOddDegree.cochainCup p q φ ψ

@[reducible, inline]

noncomputable abbrev SphereOddDegree.cochainOneZMod2 {Z : TopCat} : singularCochainGroup (ZMod 2) Z 0

The unit cochain with ZMod 2 coefficients.

Equations

• SphereOddDegree.cochainOneZMod2 = SphereOddDegree.cochainOne

@[reducible, inline]

noncomputable abbrev SphereOddDegree.cochainPowZMod2 {Z : TopCat} (φ : singularCochainGroup (ZMod 2) Z 1) (n : ℕ) : singularCochainGroup (ZMod 2) Z n

Cup powers of a degree-one cochain with ZMod 2 coefficients.

Equations

• SphereOddDegree.cochainPowZMod2 φ n = SphereOddDegree.cochainPow φ n

theorem SphereOddDegree.cochainCupZMod2_naturality {X Y : TopCat} (f : X ⟶ Y) (p q : ℕ) (φ : singularCochainGroup (ZMod 2) Y p) (ψ : singularCochainGroup (ZMod 2) Y q) : cochainPullback f (p + q) (cochainCupZMod2 p q φ ψ) = cochainCupZMod2 p q (cochainPullback f p φ) (cochainPullback f q ψ)

Naturality of the ZMod 2 cochain cup product.

Cohomology-level descent

This file supplies the Alexander--Whitney cochain product, bilinearity, naturality, unit, and powers. The Leibniz identity and the induced cohomology product are implemented in CohomologyCupProduct.lean, which exports cupZMod2, its naturality, and cup powers.