Cohomology-level singular cup product over ZMod 2 #
This file descends the genuine cochain-level Alexander–Whitney cup product
(cochainCup, CupProduct.lean) to a cohomology-level cup product on the
singular cohomology with ZMod 2 coefficients constructed in
SingularCohomology.lean:
cupZMod2 : H^p(X; F₂) → H^q(X; F₂) → H^{p+q}(X; F₂).
The descent uses the cochain Leibniz / coboundary identity of
CochainCupLeibniz.lean (cup of cocycles is a cocycle; cup with a coboundary is a
coboundary). The well-definedness on cohomology classes is cupZMod2_mk: the cup
of the classes of two cocycles is the class of their cochain cup.
Construction outline #
cohomologyZMod2 X nisH^n(X; F₂), definitionally(singularCohomologyZMod2 n).obj (op X).cocycleClasssends a cocycle to its cohomology class (homologyπ ∘ cyclesMk); it is additive, scalar-linear, surjective, and annihilates coboundaries.- For a fixed cocycle
ψ(resp.φ) the cup· ⌣ ψ(resp.φ ⌣ ·) is a cochain map of cocycles; it descends to aModuleCatmorphism on homology by the cokernel universal property (cupHomologyLeft/cupHomologyRight). cupZMod2 a bcupsaagainst a chosen cocycle representative ofbviacupHomologyLeft.cupZMod2_mkshows this is representative-independent, giving the class of the cochain cup.
The module exports the cohomology-level product and its functoriality laws.
The singular F₂-cochain complex of X.
Equations
Instances For
The n-th singular cohomology H^n(X; F₂), definitionally
(singularCohomologyZMod2 n).obj (op X).
Equations
Instances For
cohomologyZMod2 is the constructed singular cohomology object.
1. Cohomology class of a cocycle #
The cohomology class of a cocycle φ (a p-cochain with δφ = 0):
homologyπ applied to the cycle cyclesMk φ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The class only depends on the cochain, not on the cocycle proof.
The iCycles of a cycle is a cocycle.
cyclesMk (iCycles c) = c.
Every cohomology class is the class of a cocycle.
The zero cochain has zero class.
A degree-cast coboundary has zero cohomology class.
2. Cup with a fixed cocycle on the left #
The cochain map φ ↦ φ ⌣ ψ as a ModuleCat morphism C^p ⟶ C^{p+q}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cochain map ψ ↦ φ ⌣ ψ as a ModuleCat morphism C^q ⟶ C^{p+q}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cup with a fixed cocycle on the left sends cycles to cocycles.
The cup with a fixed cocycle on the right sends cycles to cocycles.
Cup with a fixed left cocycle, as a map cycles p ⟶ H^{p+q}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cup with a fixed right cocycle, as a map cycles q ⟶ H^{p+q}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
cupLeftMor evaluated on a general cycle is the class of its iCycles cupped
with ψ.
cupRightMor' evaluated on a general cycle is the class of φ cupped with its
iCycles.
If two cochains are equal and one has zero class, so does the other.
The cup of a coboundary δη (left factor) with a cocycle ψ has zero class.
The cup of a cocycle φ with a coboundary δη (right factor) has zero class.
The cup of (d_i p).hom η (left factor, in the image of a differential into
degree p) with a cocycle ψ has zero class, for any source index i.
The cup of a cocycle φ with (d_i q).hom η (right factor) has zero class.
The cup-with-left-cocycle map kills coboundaries (cokernel condition).
The cup-with-right-cocycle map kills coboundaries (cokernel condition).
3. Descent to homology in each variable #
Cup with a fixed left cocycle, descended to H^p ⟶ H^{p+q}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cup with a fixed right cocycle, descended to H^q ⟶ H^{p+q}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
cupHomologyLeft on the class of φ is the class of φ ⌣ ψ.
cupHomologyRight on the class of ψ is the class of φ ⌣ ψ.
4. The cohomology cup product #
The chosen cycle representative of a cohomology class.
Equations
- SphereOddDegree.classCycleRepr X n a = Function.surjInv ⋯ a
Instances For
A chosen cocycle representative of a cohomology class.
Equations
Instances For
The cohomology-level cup product H^p(X; F₂) → H^q(X; F₂) → H^{p+q}(X; F₂).
Equations
- SphereOddDegree.cupZMod2 a b = (ModuleCat.Hom.hom (SphereOddDegree.cupHomologyLeft X p q (SphereOddDegree.classRepr X q b) ⋯)) a
Instances For
Well-definedness / computation rule. The cup of the classes of two cocycles is the class of their cochain cup.
5. Naturality of the cohomology cup product #
The pullback f^* : H^n(Y; F₂) ⟶ H^n(X; F₂) of a continuous map f : X ⟶ Y,
as the action of the singular cohomology functor.
Equations
Instances For
The cochain pullback commutes with the coboundary (it is a cochain map).
The cochain pullback of a cocycle is a cocycle.
Naturality of the cohomology cup product. f^*(a ⌣ b) = f^* a ⌣ f^* b.
6. Powers of a degree-one class #
The unit class 1 ∈ H^0(X; F₂).
Equations
Instances For
The n-th cup power a^n ∈ H^n(X; F₂) of a degree-one class a ∈ H^1(X; F₂).
Equations
Instances For
Each cup power of a degree-one cocycle is a cocycle.
The cup power of the class of a degree-one cochain is the class of its cochain power.
Naturality of cup powers. f^*(a^n) = (f^* a)^n.
Fixed-point cup powers. If f^* a = a (a degree-one class fixed by the
pullback of a self-map), then f^*(a^n) = a^n for all n.