Cup products in low degrees on the explicit model #

A cup product on continuous cochains is relative to a G-equivariant biadditive pairing μ : M →+ N →+ P, that is one with μ (g • m) (g • n) = g • μ m n, which is furthermore jointly continuous. This file builds the six low-degree shapes

(p, q) ∈ {(0,0), (0,1), (1,0), (0,2), (1,1), (2,0)},   p + q ≤ 2,

of the general inhomogeneous formula (a ⌣ b)(g₁, …, g_{p+q}) = μ (a (g₁, …, g_p)) ((g₁ ⋯ g_p) • b (g_{p+1}, …, g_{p+q})), namely

(0,0):  m ⌣ n = μ m n,                        (0,1):  (m ⌣ b) g = μ m (b g),
(1,0):  (a ⌣ n) g = μ (a g) (g • n),          (0,2):  (m ⌣ b) (g, h) = μ m (b (g, h)),
(1,1):  (a ⌣ b) (g, h) = μ (a g) (g • b h),   (2,0):  (a ⌣ n) (g, h) = μ (a (g, h)) ((g * h) • n).

Main definitions #

TauCeti.ContCohomology.pairingLeft and TauCeti.ContCohomology.pairingRight: partial application of the pairing at an invariant element, as an equivariant additive homomorphism. This is what makes the five shapes with a degree-0 factor instances of the coefficient maps TauCeti.ContCohomology.explicitCoeff0, explicitCoeff1 and explicitCoeff2.
TauCeti.ContCohomology.explicitCup00, explicitCup01, explicitCup10, explicitCup02, explicitCup11, explicitCup20: the six shapes, each biadditive by construction, with the _mk theorems fixing the cochain formula on classes of cocycles.

Main statements #

TauCeti.ContCohomology.cup01_mem_Z1, cup10_mem_Z1, cup02_mem_Z2, cup11_mem_Z2 and cup20_mem_Z2: a cocycle cupped with a cocycle is a cocycle, the cochain-level heart of each shape.
TauCeti.ContCohomology.cup11_mem_B2_left and cup11_mem_B2_right: the (1,1) cup descends through coboundaries in each variable. These are the only descent statements proved by hand: the other five shapes descend because they are coefficient maps, whose descent is TauCeti.ContCohomology.cochainsMap1_mem_B1 and cochainsMap2_mem_B2.
TauCeti.ContCohomology.explicitCup00_comm, explicitCup01_eq_cup10_flip, explicitCup02_eq_cup20_flip and explicitCup11_eq_neg_flip: graded commutativity a ⌣_μ b = (-1)^{pq} (b ⌣_{μᵒᵖ} a) in each bidegree with p + q ≤ 2, where μᵒᵖ n m = μ m n is Mathlib's AddMonoidHom.flip. With the sign 1 in the three shapes that have a degree-0 factor the identity already holds on cochains, and those three are stated at cochain level as well (cup01_eq_cup10_flip, cup02_eq_cup20_flip), a degree-0 class being invariant. In bidegree (1,1) it holds only on classes, with the sign -1.
TauCeti.ContCohomology.explicitCup11_comm_of_neg_eq_self: the 2-torsion specialization, in which the (1,1) cup is symmetric.
TauCeti.ContCohomology.explicitCup_assoc000 and its nine siblings: associativity (x ⌣_{μ₁} y) ⌣_{μ₂} z = x ⌣_{ν₂} (y ⌣_{ν₁} z), one theorem for each tridegree (p, q, r) with p + q + r ≤ 2, the three digits of the name being that tridegree. Each holds already on cochains.
TauCeti.ContCohomology.explicitCup_assoc000_mul and its nine siblings: the same ten identities for a topological G-ring R, all four pairings its multiplication.

Implementation notes #

The translation factor g • in the (1,0), (1,1) and (2,0) formulas is the one the general inhomogeneous formula carries, and it is kept in the statements even though a degree-0 class is invariant and the factor is therefore invisible in the (1,0) and (2,0) shapes. Keeping it is what makes those two shapes the specializations of the general formula that the roadmap's associativity instances need, rather than the (0,1) and (0,2) shapes read backwards.

The (1,1) shape is the only one that is not a coefficient map, and the only one whose descent through coboundaries needs a homotopy. Its two primitives are

a ∈ B¹, a = d⁰ m :  (a ⌣ b) = d¹ (x ↦ μ m (b x)),
b ∈ B¹, b = d⁰ n :  (a ⌣ b) = d¹ (x ↦ -μ (a x) (x • n)),

recorded here because the graded-commutativity statement refers to them.

The (1,1) graded-commutativity homotopy is fixed once, here, and every sign below is read off it: for continuous 1-cocycles a and b,

(a ⌣_μ b) + (b ⌣_{μᵒᵖ} a) = d¹ (g ↦ -μ (a g) (b g)),

which is TauCeti.ContCohomology.cup11_add_cup11_flip_eq_d1.

Each cocycle proof opens with a change. It only beta-reduces: groupCohomology.IsCocycle₁ and IsCocycle₂ are predicates on a function, so with the cup cochain supplied as a lambda the goal is stated with a redex and the identity to be proved is unreadable until it is contracted. No change below alters the goal by more than beta.

Continuity of the cup cochains is where joint continuity of μ is used. It is automatic when M and N are discrete, which is the case in every arithmetic application, but it is carried as a hypothesis rather than derived so that the shapes are available at the general topological coefficients the explicit complex is built for.

Associativity is stated relative to four G-equivariant biadditive pairings μ₁ : A →+ B →+ D, μ₂ : D →+ C →+ E, ν₁ : B →+ C →+ F and ν₂ : A →+ F →+ E: these four are what it takes to type the two composites, and the coefficient identity μ₂ (μ₁ a b) c = ν₂ a (ν₁ b c) is the hypothesis that identifies them. The (1,0) and (0,0) shapes are in the family because the instances explicitCup_assoc110 and explicitCup_assoc100 need them on their right-hand sides.

This implements the "six low-degree shapes", "graded commutativity" and "associativity" milestones of Layer 8 of the human-authored roadmap at TauCetiRoadmap/ProfiniteCohomology/README.md, whose §3 fixes the six formulas, whose Layer 8 fixes the ten associativity instances and the G-ring specialization, and whose Suggested.lean fixes the names explicitCup00, explicitCup01, explicitCup10, explicitCup02, explicitCup11 and explicitCup20.

References #

J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., I §4: the cup product on inhomogeneous cochains and its low-degree formulas, and (1.4.4) for graded commutativity.
K. Brown, Cohomology of Groups, V §3: the cochain-level cup product, (3.5) for associativity and (3.6) for graded commutativity.

Cup products in low degrees on the explicit model #

Main definitions #

Main statements #

Implementation notes #

References #

Associativity #

Associativity for a topological G-ring #

Associativity for a topological `G`-ring #