Naturality of the cup product on continuous cohomology

Let φ : H →ₜ* G be a continuous homomorphism of topological groups, P : TopPairing X Y Z a coefficient pairing of topological G-representations and P' : TopPairing X' Y' Z' one of topological H-representations. Morphisms fX : res φ X ⟶ X', fY : res φ Y ⟶ Y' and fZ : res φ Z ⟶ Z' intertwining the two pairings, fZ (P.bil x y) = P'.bil (fX x) (fY y), make the maps ContinuousCohomology.map φ f of the three compatible pairs multiplicative for the cup products of TauCeti.TopPairing.cup:

map φ fZ (a ⌣ b) = map φ fX a ⌣ map φ fY b.

The identity is available at every level of the construction, not only on cohomology classes: on the coinduced resolution, for the Alexander–Whitney pairing TauCeti.TopPairing.resolutionCup and the map F ↦ f ∘ F ∘ φ of the compatible pair; on homogeneous cochains, for TauCeti.TopPairing.cupCochain and ContinuousCohomology.cochainsMap; and on cocycles, for TauCeti.TopPairing.cupCocycles and ContinuousCohomology.cocyclesMap. Arguments that work with explicit representatives can therefore compare the images of a cup product and the cup product of the images before passing to classes.

The three named instances of ContinuousCohomology.map give the three compatibilities of the cup product with the change-of-group and change-of-coefficient maps: restriction to a subgroup, inflation from a quotient, and a coefficient map. In each, the second pairing is supplied together with its defining relation to the first, since restriction leaves the coefficient map unchanged while inflation compares the pairings after including the invariants into the ambient objects. The restricted pairing TauCeti.TopPairing.res is the canonical choice in the first case.

Main results

• TauCeti.TopPairing.resolutionCup_resolutionMap, TauCeti.TopPairing.cupCochain_cochainsMap, TauCeti.TopPairing.cupCocycles_cocyclesMap: naturality on the resolution, on homogeneous cochains and on cocycles.
• TauCeti.TopPairing.cup_map: naturality of the cup product in compatible pairs.
• TauCeti.TopPairing.cup_res, TauCeti.TopPairing.cup_infl, TauCeti.TopPairing.cup_coeffMap: compatibility with restriction, inflation and coefficient maps; TauCeti.TopPairing.cup_coeffMap_left_id is the case of a coefficient map on the right factor only.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), Chapter I, §4, (1.4.2), and §5, (1.5.3).
• K. S. Brown, Cohomology of Groups, GTM 87, Springer (1982), Chapter V, §3.

Naturality in compatible pairs

theorem TauCeti.TopPairing.pointwise_resolutionMap {R : Type u} [CommRing R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X Y Z : TopRep R G} {X' Y' Z' : TopRep R H} (P : TopPairing X Y Z) (P' : TopPairing X' Y' Z') (φ : H →ₜ* G) (fX : TopRep.res (↑φ) X ⟶ X') (fY : TopRep.res (↑φ) Y ⟶ Y') (fZ : TopRep.res (↑φ) Z ⟶ Z') (hpair : ∀ (x : ↑X) (y : ↑Y), (CategoryTheory.ConcreteCategory.hom fZ) ((P.bil x) y) = (P'.bil ((CategoryTheory.ConcreteCategory.hom fX) x)) ((CategoryTheory.ConcreteCategory.hom fY) y)) (n k : ℕ) (hk : k = n) (x : ↑X) (F : ↑(Y.resolutionX n)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.resolutionMap φ fZ k)) ((P.pointwise n k hk) (x, F)) = (P'.pointwise n k hk) ((CategoryTheory.ConcreteCategory.hom fX) x, (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.resolutionMap φ fY n)) F)

The pointwise pairing is natural in compatible pairs.

theorem TauCeti.TopPairing.resolutionCup_resolutionMap {R : Type u} [CommRing R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X Y Z : TopRep R G} {X' Y' Z' : TopRep R H} (P : TopPairing X Y Z) (P' : TopPairing X' Y' Z') (φ : H →ₜ* G) (fX : TopRep.res (↑φ) X ⟶ X') (fY : TopRep.res (↑φ) Y ⟶ Y') (fZ : TopRep.res (↑φ) Z ⟶ Z') (hpair : ∀ (x : ↑X) (y : ↑Y), (CategoryTheory.ConcreteCategory.hom fZ) ((P.bil x) y) = (P'.bil ((CategoryTheory.ConcreteCategory.hom fX) x)) ((CategoryTheory.ConcreteCategory.hom fY) y)) (m n k : ℕ) (hk : k = n + m) (a : ↑(X.resolutionX (m + 1))) (b : ↑(Y.resolutionX (n + 1))) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.resolutionMap φ fZ (k + 1))) ((P.resolutionCup m n k hk) (a, b)) = (P'.resolutionCup m n k hk) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.resolutionMap φ fX (m + 1))) a, (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.resolutionMap φ fY (n + 1))) b)

The Alexander–Whitney pairing on the resolution is natural in compatible pairs: the map F ↦ f ∘ F ∘ φ induced on the resolution takes a ⌣ b to the pairing of the images.

theorem TauCeti.TopPairing.resolutionCupPairing_resolutionMap {R : Type u} [CommRing R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X Y Z : TopRep R G} {X' Y' Z' : TopRep R H} (P : TopPairing X Y Z) (P' : TopPairing X' Y' Z') (φ : H →ₜ* G) (fX : TopRep.res (↑φ) X ⟶ X') (fY : TopRep.res (↑φ) Y ⟶ Y') (fZ : TopRep.res (↑φ) Z ⟶ Z') (hpair : ∀ (x : ↑X) (y : ↑Y), (CategoryTheory.ConcreteCategory.hom fZ) ((P.bil x) y) = (P'.bil ((CategoryTheory.ConcreteCategory.hom fX) x)) ((CategoryTheory.ConcreteCategory.hom fY) y)) (m n : ℕ) (a : ↑(X.resolution'X m)) (b : ↑(Y.resolution'X n)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.resolutionMap φ fZ (m + n + 1))) (((P.resolutionCupPairing m n) a) b) = ((P'.resolutionCupPairing m n) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.resolutionMap φ fX (m + 1))) a)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.resolutionMap φ fY (n + 1))) b)

The resolution pairing in degree m + n is natural in compatible pairs.

theorem TauCeti.TopPairing.cupCochain_cochainsMap {R : Type u} [CommRing R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X Y Z : TopRep R G} {X' Y' Z' : TopRep R H} (P : TopPairing X Y Z) (P' : TopPairing X' Y' Z') (φ : H →ₜ* G) (fX : TopRep.res (↑φ) X ⟶ X') (fY : TopRep.res (↑φ) Y ⟶ Y') (fZ : TopRep.res (↑φ) Z ⟶ Z') (hpair : ∀ (x : ↑X) (y : ↑Y), (CategoryTheory.ConcreteCategory.hom fZ) ((P.bil x) y) = (P'.bil ((CategoryTheory.ConcreteCategory.hom fX) x)) ((CategoryTheory.ConcreteCategory.hom fY) y)) (m n : ℕ) (a : ↑(X.homogeneousCochains.X m).toModuleCat) (b : ↑(Y.homogeneousCochains.X n).toModuleCat) : (CategoryTheory.ConcreteCategory.hom ((ContinuousCohomology.cochainsMap φ fZ).f (m + n))) (((P.cupCochain m n) a) b) = ((P'.cupCochain m n) ((CategoryTheory.ConcreteCategory.hom ((ContinuousCohomology.cochainsMap φ fX).f m)) a)) ((CategoryTheory.ConcreteCategory.hom ((ContinuousCohomology.cochainsMap φ fY).f n)) b)

The cup product of homogeneous cochains is natural in compatible pairs.

theorem TauCeti.TopPairing.cupCocycles_cocyclesMap {R : Type u} [CommRing R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X Y Z : TopRep R G} {X' Y' Z' : TopRep R H} (P : TopPairing X Y Z) (P' : TopPairing X' Y' Z') (φ : H →ₜ* G) (fX : TopRep.res (↑φ) X ⟶ X') (fY : TopRep.res (↑φ) Y ⟶ Y') (fZ : TopRep.res (↑φ) Z ⟶ Z') (hpair : ∀ (x : ↑X) (y : ↑Y), (CategoryTheory.ConcreteCategory.hom fZ) ((P.bil x) y) = (P'.bil ((CategoryTheory.ConcreteCategory.hom fX) x)) ((CategoryTheory.ConcreteCategory.hom fY) y)) (m n : ℕ) (a : ↑(ContinuousCohomology.cocycles X m).toModuleCat) (b : ↑(ContinuousCohomology.cocycles Y n).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.cocyclesMap φ fZ (m + n))) (((P.cupCocycles m n) a) b) = ((P'.cupCocycles m n) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.cocyclesMap φ fX m)) a)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.cocyclesMap φ fY n)) b)

The cup product of cocycles is natural in compatible pairs.

theorem TauCeti.TopPairing.cup_map {R : Type u} [CommRing R] [TopologicalSpace R] {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X Y Z : TopRep R G} {X' Y' Z' : TopRep R H} (P : TopPairing X Y Z) (P' : TopPairing X' Y' Z') (φ : H →ₜ* G) (fX : TopRep.res (↑φ) X ⟶ X') (fY : TopRep.res (↑φ) Y ⟶ Y') (fZ : TopRep.res (↑φ) Z ⟶ Z') (hpair : ∀ (x : ↑X) (y : ↑Y), (CategoryTheory.ConcreteCategory.hom fZ) ((P.bil x) y) = (P'.bil ((CategoryTheory.ConcreteCategory.hom fX) x)) ((CategoryTheory.ConcreteCategory.hom fY) y)) (m n : ℕ) (a : ↑(continuousCohomology m X).toModuleCat) (b : ↑(continuousCohomology n Y).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ fZ (m + n))) (((P.cup m n) a) b) = ((P'.cup m n) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ fX m)) a)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ fY n)) b)

Naturality of the cup product in compatible pairs (NSW (1.4.2)): for a continuous homomorphism φ : H →ₜ* G and morphisms fX, fY, fZ of the coefficients intertwining the pairings P and P', the induced maps on continuous cohomology satisfy map φ fZ (a ⌣ b) = map φ fX a ⌣ map φ fY b.

Restriction, inflation and coefficient maps

theorem TauCeti.TopPairing.cup_coeffMap {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) {X' Y' Z' : TopRep R G} (P' : TopPairing X' Y' Z') (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') (hcompat : ∀ (x : ↑X) (y : ↑Y), (CategoryTheory.ConcreteCategory.hom h) ((P.bil x) y) = (P'.bil ((CategoryTheory.ConcreteCategory.hom f) x)) ((CategoryTheory.ConcreteCategory.hom g) y)) (m n : ℕ) (a : ↑(continuousCohomology m X).toModuleCat) (b : ↑(continuousCohomology n Y).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap h (m + n))) (((P.cup m n) a) b) = ((P'.cup m n) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap f m)) a)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap g n)) b)

Naturality of the cup product in the coefficients (NSW (1.4.2)): coefficient morphisms f, g, h intertwining the pairings P and P' satisfy coeffMap h (a ⌣ b) = coeffMap f a ⌣ coeffMap g b.

theorem TauCeti.TopPairing.cup_coeffMap_left_id {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) {Y' Z' : TopRep R G} (P' : TopPairing X Y' Z') (g : Y ⟶ Y') (h : Z ⟶ Z') (hcompat : ∀ (x : ↑X) (y : ↑Y), (CategoryTheory.ConcreteCategory.hom h) ((P.bil x) y) = (P'.bil x) ((CategoryTheory.ConcreteCategory.hom g) y)) (m n : ℕ) (a : ↑(continuousCohomology m X).toModuleCat) (b : ↑(continuousCohomology n Y).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap h (m + n))) (((P.cup m n) a) b) = ((P'.cup m n) a) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap g n)) b)

Naturality of the cup product in the coefficients of the right factor only: coefficient morphisms g, h with h (P.bil x y) = P'.bil x (g y) satisfy coeffMap h (a ⌣ b) = a ⌣' coeffMap g b. This is cup_coeffMap with f = 𝟙 X.

theorem TauCeti.TopPairing.cup_res {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) (S : Subgroup G) (Pres : TopPairing (TopRep.res S.subtype X) (TopRep.res S.subtype Y) (TopRep.res S.subtype Z)) (hPres : Pres.bil = P.bil) (m n : ℕ) (a : ↑(continuousCohomology m X).toModuleCat) (b : ↑(continuousCohomology n Y).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.res S Z (m + n))) (((P.cup m n) a) b) = ((Pres.cup m n) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.res S X m)) a)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.res S Y n)) b)

Restriction preserves cup products (NSW (1.5.3)(i)): for a subgroup S ≤ G and a pairing Pres of the restricted coefficients with the same underlying bilinear map as P, res S (a ⌣ b) = res S a ⌣ res S b.

theorem TauCeti.TopPairing.cup_infl {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 : Subgroup G) [N.Normal] (Pinv : TopPairing (X.quotientToInvariants N) (Y.quotientToInvariants N) (Z.quotientToInvariants N)) (hPinv : ∀ (x : ↑(X.quotientToInvariants N)) (y : ↑(Y.quotientToInvariants N)), (CategoryTheory.ConcreteCategory.hom (Z.quotientToInvariantsι N)) ((Pinv.bil x) y) = (P.bil ((CategoryTheory.ConcreteCategory.hom (X.quotientToInvariantsι N)) x)) ((CategoryTheory.ConcreteCategory.hom (Y.quotientToInvariantsι N)) y)) (m n : ℕ) (a : ↑(continuousCohomology m (X.quotientToInvariants N)).toModuleCat) (b : ↑(continuousCohomology n (Y.quotientToInvariants N)).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.infl N Z (m + n))) (((Pinv.cup m n) a) b) = ((P.cup m n) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.infl N X m)) a)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.infl N Y n)) b)

Inflation preserves cup products (NSW (1.5.3)(iii)): for a normal subgroup N ≤ G and a pairing Pinv of the N-invariants that agrees with P after inclusion of the invariants into the ambient objects, infl N (a ⌣ b) = infl N a ⌣ infl N b.