Cochain cup Leibniz identity and its descent consequences

This file records the cochain-level Leibniz / coboundary formula for the singular cup product over ZMod 2 and derives the immediate consequences needed to descend the cup product to singular cohomology.

The headline identity itself,

δ(φ ⌣ ψ) = δφ ⌣ ψ + φ ⌣ δψ (over `ZMod 2`)

is aw_cochain_leibniz_zmod2 from AlexanderWhitneyChainMap.lean; here it is restated as cochainCupZMod2_differential, and the following descent facts are proved:

• cochainCupZMod2_respects_cocycles — the cup of two cocycles is a cocycle, so the cup product is defined on cocycle representatives;
• cochainCupZMod2_coboundary_left / cochainCupZMod2_coboundary_right — if one factor is a cocycle, the coboundary of the cup is the cup of that factor with the coboundary of the other (the cup of a cocycle with a coboundary is itself a coboundary, up to the degree relabelling cast);
• cochainCupZMod2_coboundary_left' / cochainCupZMod2_coboundary_right' — the same facts in the "is a coboundary" direction (δη ⌣ ψ = cast (δ(η ⌣ ψ))), exhibiting the cup with a coboundary explicitly as the coboundary of a cochain;
• cochainCupZMod2_respects_coboundaries — changing a cocycle factor by a coboundary changes the cup product by a coboundary, i.e. the cup product respects the cohomology equivalence relation at the cochain level.

Together these are exactly the inputs needed to define the cohomology-level cup product H^p(X; ZMod 2) × H^q(X; ZMod 2) → H^{p+q}(X; ZMod 2): the cup descends to a well-defined bilinear pairing on cohomology classes.

Degree bookkeeping

The δφ ⌣ ψ term naturally lives in degree (p+1)+q and the φ ⌣ δψ term in degree p+(q+1); both are transported to the common degree (p+q)+1 via the cochain degree cast cochainCast (with p+(q+1) = (p+q)+1 definitional and (p+1)+q = (p+q)+1 propositional via aw_degree_left_succ).

0. Cast lemmas for the cochain degree cast

@[simp]

theorem SphereOddDegree.cochainCast_zero {R : Type} [CommRing R] {Z : TopCat} {m m' : ℕ} (h : m = m') : cochainCast h 0 = 0

The degree cast of the zero cochain is zero.

theorem SphereOddDegree.cochainCast_add {R : Type} [CommRing R] {Z : TopCat} {m m' : ℕ} (h : m = m') (φ ψ : singularCochainGroup R Z m) : cochainCast h (φ + ψ) = cochainCast h φ + cochainCast h ψ

The degree cast is additive.

@[simp]

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

The degree cast along h followed by the cast along h.symm is the identity.

1. The Leibniz / coboundary identity (restated)

theorem SphereOddDegree.cochainCupZMod2_differential {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 ψ))

Cochain cup Leibniz identity over ZMod 2 (restatement of aw_cochain_leibniz_zmod2). The cochain coboundary is a derivation for the cup product:

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

The two right-hand terms, of degrees (p+1)+q and p+(q+1), are transported to the common degree (p+q)+1 via the cochain degree cast.

2. Cup of cocycles is a cocycle

theorem SphereOddDegree.cochainCupZMod2_respects_cocycles {X : TopCat} (p q : ℕ) (φ : singularCochainGroup (ZMod 2) X p) (ψ : singularCochainGroup (ZMod 2) X q) (hφ : cochainCoboundary (ZMod 2) X p φ = 0) (hψ : cochainCoboundary (ZMod 2) X q ψ = 0) : cochainCoboundary (ZMod 2) X (p + q) (cochainCup p q φ ψ) = 0

The cup of two cocycles is a cocycle. If δφ = 0 and δψ = 0 then δ(φ ⌣ ψ) = 0. This is what makes the cup product defined on cocycle representatives.

3. Cup with a coboundary is a coboundary

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

Coboundary of a cup, left factor a cocycle. If δa = 0 then δ(a ⌣ ψ) = cast (a ⌣ δψ). Equivalently, the cup of the cocycle a with the coboundary δψ is itself a coboundary.

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

Coboundary of a cup, right factor a cocycle. If δψ = 0 then δ(η ⌣ ψ) = cast (δη ⌣ ψ). Equivalently, the cup of the coboundary δη with the cocycle ψ is itself a coboundary.

theorem SphereOddDegree.cochainCupZMod2_coboundary_left' {X : TopCat} (p q : ℕ) (η : singularCochainGroup (ZMod 2) X p) (ψ : singularCochainGroup (ZMod 2) X q) (hψ : cochainCoboundary (ZMod 2) X q ψ = 0) : cochainCup (p + 1) q (cochainCoboundary (ZMod 2) X p η) ψ = cochainCast ⋯ (cochainCoboundary (ZMod 2) X (p + q) (cochainCup p q η ψ))

δη ⌣ ψ is a coboundary (explicit form). When ψ is a cocycle, δη ⌣ ψ equals the degree-relabelled coboundary cast (δ(η ⌣ ψ)), exhibiting it explicitly as a coboundary.

theorem SphereOddDegree.cochainCupZMod2_coboundary_right' {X : TopCat} (p q : ℕ) (a : singularCochainGroup (ZMod 2) X p) (η : singularCochainGroup (ZMod 2) X q) (ha : cochainCoboundary (ZMod 2) X p a = 0) : cochainCup p (q + 1) a (cochainCoboundary (ZMod 2) X q η) = cochainCast ⋯ (cochainCoboundary (ZMod 2) X (p + q) (cochainCup p q a η))

a ⌣ δη is a coboundary (explicit form). When a is a cocycle, a ⌣ δη equals the degree-relabelled coboundary cast (δ(a ⌣ η)), exhibiting it explicitly as a coboundary.

4. The cup respects cohomology equivalence

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

The cup product respects coboundaries in the left factor. If ψ is a cocycle, then changing the left factor by a coboundary δη changes the cup product by the coboundary cast (δ(η ⌣ ψ)):

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

Thus cohomologous left factors yield cohomologous cups: the cup product descends to cohomology classes in the left variable.

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

The cup product respects coboundaries in the right factor. If φ is a cocycle, then changing the right factor by a coboundary δη changes the cup product by the coboundary cast (δ(φ ⌣ η)):

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

Thus cohomologous right factors yield cohomologous cups: the cup product descends to cohomology classes in the right variable.