Graded commutativity of the cup product

Let P : TopPairing X Y Z be a coefficient pairing of topological representations of a topological group G, and let P.flip : TopPairing Y X Z be the opposite pairing TauCeti.TopPairing.flip, P.flip.bil y x = P.bil x y. On continuous cohomology the cup products in the two orders are related by graded commutativity,

a ⌣_P b = (-1)^(m n) (b ⌣_{P.flip} a),     a ∈ Hᵐ(G, X), b ∈ Hⁿ(G, Y),

which this file proves in every bidegree (TauCeti.TopPairing.cup_gradedComm). In bidegree (1, 1) it reads cup P 1 1 a b = - cup P.flip 1 1 b a, the identity against which the cup square H¹(G, M) × H¹(G, M) → H²(G, M) of a commutative coefficient ring is stated.

In bidegree (0, n) the identity already holds on cocycles. A homogeneous zero-cocycle is a constant function, and the two Alexander–Whitney products therefore pair the same constant coefficient with the same value of the n-cochain. The recursion on Mathlib's iterated-curried coinduction resolution is recorded by TauCeti.TopPairing.resolutionCupPairing_zero_eq_flip; its restrictions to homogeneous cochains and cohomology are TauCeti.TopPairing.cupCochain_zero_eq_flip and TauCeti.TopPairing.cup_zero_eq_flip.

In general the identity fails on cochains, and the proof is a homotopy: Steenrod's cup-one product TauCeti.TopPairing.cupOne. For a of degree m and b of degree n + 1 it has degree m + n and, in homogeneous coordinates,

(a ∪₁ b) (g₀, …, g_{m+n}) =
  ∑_{i < m} (-1)^((m - 1 - i) n) μ (a (g₀, …, gᵢ, g_{i+n+1}, …, g_{m+n})) (b (gᵢ, …, g_{i+n+1})).

On the curried resolution this is a recursion on the first vertex: a ∪₁ b = 0 when a has degree zero, and (a ∪₁ b) g = (a g) ∪₁ b + (-1)^(m n) ((b g) ⌣_{P.flip} (a g)) when a has degree m + 1, the second term collecting the summand i = 0. Its boundary is (TauCeti.TopPairing.d_cupOne)

d (a ∪₁ b) = (d a) ∪₁ b - (-1)^m (a ∪₁ d b) + (-1)^m (a ⌣ b) - (-1)^(m n) (b ⌣_{P.flip} a),

For cocycles only the last two terms survive, so (-1)^m (a ∪₁ b) is a primitive of (a ⌣ b) - (-1)^(m (n + 1)) (b ⌣_{P.flip} a), which is graded commutativity in bidegree (m, n + 1). Bidegree (m, 0) is the case (0, m) for the opposite pairing.

The same homotopy in bidegree (1, 1) is formalized on the explicit inhomogeneous model of TauCeti.RepresentationTheory.Homological.ContCohomology.Cup.Product as TauCeti.ContCohomology.cup11_add_cup11_flip_eq_d1, with descent TauCeti.ContCohomology.explicitCup11_eq_neg_flip; this file works on Mathlib's continuousCohomology, so that it applies to TauCeti.TopPairing.cup.

Main definitions

• TauCeti.TopPairing.cupOne: the cup-one product on the coinduced resolution, with explicit total degree.
• TauCeti.TopPairing.cupOneCochain: the cup-one product of homogeneous cochains, as a bilinear map.

Main results

• TauCeti.TopPairing.cup_zero_eq_flip: graded commutativity in bidegree (0, n), without a sign.
• TauCeti.TopPairing.d_cupOne: the boundary of the cup-one product.
• TauCeti.TopPairing.d_cupOneCochain: the boundary of the cup-one product of two cocycles is (-1)^m (a ⌣ b) - (-1)^(m n) (b ⌣ᵒᵖ a).
• TauCeti.TopPairing.cup_gradedComm: graded commutativity in every bidegree, a ⌣_P b = (-1)^(m n) (b ⌣_{P.flip} a), with the degree transport between n + m and m + n explicit.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer (1982), Chapter V, §3, (3.6).
• N. E. Steenrod, Products of cocycles and extensions of mappings, Ann. of Math. 48 (1947), 290–320, for the ∪₁ product.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Chapter I, §4, (1.4.4).

Graded commutativity with a degree-zero cocycle

theorem TauCeti.TopPairing.resolutionCupPairing_zero_eq_flip {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (n : ℕ) (x : ↑X) (b : ↑(Y.resolution'X n)) : ((P.resolutionCupPairing 0 n) ((TopRep.Hom.hom (X.d 0)) x)) b = (TopRep.Hom.hom (HomologicalComplex.XIsoOfEq Z.resolution ⋯).hom) (((P.flip.resolutionCupPairing n 0) b) ((TopRep.Hom.hom (X.d 0)) x))

Graded commutativity on the resolution in bidegree (0, n), for a constant zero-degree element. The opposite product is transported from degree n + 0 to degree 0 + n.

theorem TauCeti.TopPairing.cupCochain_zero_eq_flip {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (n : ℕ) {a : ↑(X.homogeneousCochains.X 0).toModuleCat} (ha : (TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1)) a = 0) (b : ↑(Y.homogeneousCochains.X n).toModuleCat) : ((P.cupCochain 0 n) a) b = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq Z.homogeneousCochains ⋯).hom) (((P.flip.cupCochain n 0) b) a)

Graded commutativity of homogeneous cochains in bidegree (0, n): if a is a zero-cocycle, then a ⌣_P b is the degree transport of b ⌣_{P.flip} a. No cocycle condition on b is needed.

theorem TauCeti.TopPairing.cup_zero_eq_flip {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (n : ℕ) (a : ↑(continuousCohomology 0 X).toModuleCat) (b : ↑(continuousCohomology n Y).toModuleCat) : ((P.cup 0 n) a) b = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.degreeCast Z ⋯).hom) (((P.flip.cup n 0) b) a)

Graded commutativity of the cup product in bidegree (0, n): a ⌣_P b = b ⌣_{P.flip} a, with the opposite product transported from degree n + 0 to degree 0 + n. This is the zero-degree base case of the all-bidegree graded-commutativity homotopy.

The cup-one product on the resolution

def TauCeti.TopPairing.cupOne {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n k : ℕ) : k = n + m → C(↑(X.resolutionX (m + 1)) × ↑(Y.resolutionX (n + 2)), ↑(Z.resolutionX (k + 1)))

The cup-one product on the coinduced resolution, Steenrod's ∪₁, with explicit total degree: an element a of the (m + 1)-st term of the resolution of X (a degree-m element) paired with an element b of the (n + 2)-nd term of the resolution of Y (a degree-(n + 1) element) gives an element of the (k + 1)-st term of the resolution of Z, for k = n + m.

It vanishes for m = 0, and otherwise fixes the first vertex: (a ∪₁ b) g = (a g) ∪₁ b + (-1)^(m n) ((b g) ⌣_{P.flip} (a g)) for a of degree m + 1. In homogeneous coordinates this is Steenrod's sum ∑_{i < m} (-1)^((m - 1 - i) n) μ (a (g₀, …, gᵢ, g_{i+n+1}, …, g_{m+n})) (b (gᵢ, …, g_{i+n+1})). Its boundary is TauCeti.TopPairing.d_cupOne.

Equations

• One or more equations did not get rendered due to their size.
• P.cupOne 0 x✝² x✝¹ x✝ = 0
• P.cupOne n.succ x✝ 0 hk = absurd hk ⋯

@[simp]

theorem TauCeti.TopPairing.cupOne_zero {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) {n k : ℕ} (hk : k = n + 0) : P.cupOne 0 n k hk = 0

The cup-one product vanishes when the first factor has degree zero.

@[simp]

theorem TauCeti.TopPairing.cupOne_succ_apply {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) {m n k : ℕ} (hk : k + 1 = n + (m + 1)) (a : C(G, ↑(X.resolutionX (m + 1)))) (b : ↑(Y.resolutionX (n + 2))) (g : G) : ((P.cupOne (m + 1) n (k + 1) hk) (a, b)) g = (P.cupOne m n k ⋯) (a g, b) + (-1) ^ (m * n) • (P.flip.resolutionCup n m k ⋯) (b g, a g)

The recursion of the cup-one product: fixing the first vertex g leaves the cup-one product of a g with b, plus the signed opposite Alexander–Whitney product of b g with a g.

theorem TauCeti.TopPairing.cupOne_add_left {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n k : ℕ) (hk : k = n + m) (a a' : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 2))) : (P.cupOne m n k hk) (a + a', b) = (P.cupOne m n k hk) (a, b) + (P.cupOne m n k hk) (a', b)

theorem TauCeti.TopPairing.cupOne_smul_left {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n k : ℕ) (hk : k = n + m) (r : R) (a : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 2))) : (P.cupOne m n k hk) (r • a, b) = r • (P.cupOne m n k hk) (a, b)

theorem TauCeti.TopPairing.cupOne_add_right {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n k : ℕ) (hk : k = n + m) (a : ↑(X.resolutionX (m + 1))) (b b' : ↑(Y.resolutionX (n + 2))) : (P.cupOne m n k hk) (a, b + b') = (P.cupOne m n k hk) (a, b) + (P.cupOne m n k hk) (a, b')

theorem TauCeti.TopPairing.cupOne_smul_right {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n k : ℕ) (hk : k = n + m) (r : R) (a : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 2))) : (P.cupOne m n k hk) (a, r • b) = r • (P.cupOne m n k hk) (a, b)

theorem TauCeti.TopPairing.cupOne_ρ {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n k : ℕ) (hk : k = n + m) (g : G) (a : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 2))) : (P.cupOne m n k hk) (((X.resolutionX (m + 1)).ρ g) a, ((Y.resolutionX (n + 2)).ρ g) b) = ((Z.resolutionX (k + 1)).ρ g) ((P.cupOne m n k hk) (a, b))

The cup-one product is equivariant.

The boundary of the cup-one product

theorem TauCeti.TopPairing.d_cupOne {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n k : ℕ) (hk : k = n + m) (a : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 2))) : (TopRep.Hom.hom (Z.d (k + 1))) ((P.cupOne m n k hk) (a, b)) = (P.cupOne (m + 1) n (k + 1) ⋯) ((TopRep.Hom.hom (X.d (m + 1))) a, b) - (-1) ^ m • (P.cupOne m (n + 1) (k + 1) ⋯) (a, (TopRep.Hom.hom (Y.d (n + 2))) b) + (-1) ^ m • (P.resolutionCup m (n + 1) (k + 1) ⋯) (a, b) - (-1) ^ (m * n) • (P.flip.resolutionCup (n + 1) m (k + 1) ⋯) (b, a)

The cup-one boundary formula on the resolution. For a of degree m and b of degree n + 1, d (a ∪₁ b) = (d a) ∪₁ b - (-1)^m (a ∪₁ d b) + (-1)^m (a ⌣ b) - (-1)^(m n) (b ⌣_{P.flip} a). On cocycles only the last two terms survive, so the cup-one product is a homotopy between (-1)^m (a ⌣ b) and (-1)^(m n) (b ⌣_{P.flip} a).

The cup-one product of homogeneous cochains

def TauCeti.TopPairing.cupOneCochain {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n : ℕ) : ↑(X.homogeneousCochains.X m).toModuleCat →ₗ[R] ↑(Y.homogeneousCochains.X (n + 1)).toModuleCat →ₗ[R] ↑(Z.homogeneousCochains.X (m + n)).toModuleCat

The cup-one product of homogeneous cochains, as an R-bilinear map from m-cochains of X and (n + 1)-cochains of Y to (m + n)-cochains of Z: the cup-one product of the underlying elements of the resolution, which is invariant by equivariance.

Equations

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

theorem TauCeti.TopPairing.coe_cupOneCochain {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n : ℕ) (a : ↑(X.homogeneousCochains.X m).toModuleCat) (b : ↑(Y.homogeneousCochains.X (n + 1)).toModuleCat) : ↑(((P.cupOneCochain m n) a) b) = (P.cupOne m n (m + n) ⋯) (↑a, ↑b)

The underlying resolution element of cupOneCochain is cupOne.

theorem TauCeti.TopPairing.d_cupOneCochain {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n : ℕ) {a : ↑(X.homogeneousCochains.X m).toModuleCat} (ha : (TopModuleCat.Hom.hom (X.homogeneousCochains.d m (m + 1))) a = 0) {b : ↑(Y.homogeneousCochains.X (n + 1)).toModuleCat} (hb : (TopModuleCat.Hom.hom (Y.homogeneousCochains.d (n + 1) (n + 1 + 1))) b = 0) : (TopModuleCat.Hom.hom (Z.homogeneousCochains.d (m + n) (m + n + 1))) (((P.cupOneCochain m n) a) b) = (-1) ^ m • (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq Z.homogeneousCochains ⋯).hom) (((P.cupCochain m (n + 1)) a) b) - (-1) ^ (m * n) • (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq Z.homogeneousCochains ⋯).hom) (((P.flip.cupCochain (n + 1) m) b) a)

The differential of the cup-one product of two cocycles: for a cocycle a of degree m and a cocycle b of degree n + 1, d (a ∪₁ b) = (-1)^m (a ⌣ b) - (-1)^(m n) (b ⌣ᵒᵖ a), both products transported to degree m + n + 1.

Graded commutativity on classes

theorem TauCeti.TopPairing.cup_gradedComm {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y Z : TopRep R G} (P : TopPairing X Y Z) (m n : ℕ) (a : ↑(continuousCohomology m X).toModuleCat) (b : ↑(continuousCohomology n Y).toModuleCat) : ((P.cup m n) a) b = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.degreeCast Z ⋯).hom) ((-1) ^ (m * n) • ((P.flip.cup n m) b) a)

Graded commutativity of the cup product: a ⌣_P b = (-1)^(m n) (b ⌣_{P.flip} a) for a of degree m and b of degree n, with the opposite product transported from degree n + m to degree m + n.