Cup graded-commutativity in characteristic 2 #
The (1,1) cup product is graded-commutative: c ∪_μ d = (-1)^{1·1} d ∪_{μᵀ} c, where μᵀ is
the transposed pairing. In characteristic 2 the sign disappears, giving
cup11 μ c d = cup11 μ.flip d c (for a 2-torsion target P).
The proof is a clean cochain homotopy that holds over ℤ at the cocycle level:
cup11Fun μ a b + cup11Fun μᵀ b a = δ¹(g ↦ −μ(a g)(b g)) (cup11Fun_add_flip_eq_dOne);
2-torsion of P is used only to turn the class difference α − β into the sum α + β.
This is the general form of GQ2.HilbertLedger.trivialCupPairing_comm (the Hilbert-ledger proof), which is the
special case μ = AddMonoidHom.mul on the trivial 𝔽₂-module (μ.flip = μ by mul_comm); a
future refactor can derive that lemma from cup11_comm here. Designed to live in
GQ2/CupProduct.lean (kept in a separate file for now to avoid churn on the shared foundation).
The transposed pairing μᵀ = μ.flip is G-equivariant when μ is.
The graded-commutativity homotopy (valid over ℤ): for cocycles a, b,
(a ∪_μ b) + (b ∪_{μᵀ} a) = δ¹(g ↦ −μ(a g)(b g)). Expanding δ¹ with the cocycle identities
for a, b and the equivariance hμ leaves exactly a ∪_μ b + b ∪_{μᵀ} a.
Cup graded-commutativity in characteristic 2: for a 2-torsion target P,
cup11 μ c d = cup11 μ.flip d c in H².
Graded-commutativity for the (0,2)/(2,0) pair (no characteristic hypothesis needed):
cup02 μ c d = cup20 μᵀ d c. The (g·h)-twist in cup20 is absorbed because the H⁰ element
c is invariant, so the two cup cochains are equal — no homotopy.
Graded-commutativity for the (2,0)/(0,2) pair (the transpose of cup02_eq_cup20_flip):
cup20 μ c d = cup02 μᵀ d c. Again the (g·h)-twist is absorbed by invariance of the H⁰
element d, so the cochains are equal on the nose.
Class formula for the (0,2) cup (definitional, like cup11_mk_mk).
Class formula for the (2,0) cup (definitional, like cup11_mk_mk).
Cohomology transport along a G-equivariant module isomorphism #
The repo's mapCoeff1/mapCoeff2 have no functoriality lemmas; these package a G-equivariant
AddEquiv of coefficients into AddEquivs on H¹/H², which the duality transport needs.
The inverse of a G-equivariant coefficient equivalence is G-equivariant.
H¹ transport: a G-equivariant AddEquiv of coefficients induces one on H¹.
Equations
- One or more equations did not get rendered due to their size.
Instances For
H1congr on a class is post-composition of a cocycle representative (definitional).
mapCoeff2 on a class: post-composition of a 2-cocycle representative.
H² transport: a G-equivariant AddEquiv of coefficients induces one on H².
Equations
- One or more equations did not get rendered due to their size.
Instances For
H2congr on a class is post-composition of a 2-cocycle representative (definitional).
H⁰ transport: a G-equivariant AddEquiv of coefficients induces one on the invariants
H⁰ (needed for the degree-(2,0) duality clause).
Equations
- GQ2.ContCoh.H0congr e he = { toFun := ⇑(GQ2.ContCoh.mapCoeff0 e.toAddMonoidHom he), invFun := ⇑(GQ2.ContCoh.mapCoeff0 e.symm.toAddMonoidHom ⋯), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }