The cup product on continuous cohomology

Let P : TopPairing X Y Z be an equivariant jointly continuous bilinear pairing of topological representations of a topological group G. The Alexander–Whitney cup product of homogeneous cochains TauCeti.TopPairing.cupCochain satisfies the Leibniz rule d (a ⌣ b) = d a ⌣ b + (-1)^m (a ⌣ d b), so a cocycle cupped with a cocycle is a cocycle, and a coboundary cupped with a cocycle, or a cocycle with a coboundary, is a coboundary. This file descends the cup product accordingly, first to the cocycles and then to Mathlib's continuous cohomology, giving the bilinear map

cup P m n : Hᵐ(G, X) →ₗ[R] Hⁿ(G, Y) →ₗ[R] Hᵐ⁺ⁿ(G, Z),

determined by cup P m n [a] [b] = [a ⌣ b] on classes of cocycles (TauCeti.TopPairing.cup_π). Biadditivity, and more generally R-bilinearity, is carried by the type: additivity in either argument is LinearMap.map_add₂ and map_add.

The descent runs through HomologicalComplex.descHomologyₗ, the elementwise universal property of homology in TopModuleCat R: a linear map out of the cycles that vanishes on the kernel of the class map factors through the homology. It is applied twice, once in each variable, which is why that universal property is stated for linear maps into an arbitrary module rather than for morphisms of TopModuleCat R.

Main definitions

• TauCeti.TopPairing.cupCocycles: the cup product of cocycles.
• TauCeti.TopPairing.cup: the cup product on continuous cohomology.

Main results

• TauCeti.TopPairing.iCycles_cupCocycles: the cup product of cocycles is, on underlying cochains, the cup product of cochains.
• TauCeti.TopPairing.homologyπ_cupCocycles_eq_zero_of_left_eq_zero and TauCeti.TopPairing.homologyπ_cupCocycles_eq_zero_of_right_eq_zero: the cup product of a coboundary with a cocycle, in either order, is a coboundary.
• TauCeti.TopPairing.cup_π: the cup product of the classes of two cocycles is the class of their cup product.

References

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

The cup product of cocycles

noncomputable def TauCeti.TopPairing.cupCocycles {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 : ℕ) : ↑(ContinuousCohomology.cocycles X m).toModuleCat →ₗ[R] ↑(ContinuousCohomology.cocycles Y n).toModuleCat →ₗ[R] ↑(ContinuousCohomology.cocycles Z (m + n)).toModuleCat

The cup product of cocycles: the cup product TauCeti.TopPairing.cupCochain of the underlying homogeneous cochains, which is a cocycle by the Leibniz rule.

Equations

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

theorem TauCeti.TopPairing.iCycles_cupCocycles {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.cocycles X m).toModuleCat) (b : ↑(ContinuousCohomology.cocycles Y n).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles Z.homogeneousCochains (m + n))) (((P.cupCocycles m n) a) b) = ((P.cupCochain m n) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains m)) a)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles Y.homogeneousCochains n)) b)

On underlying cochains, the cup product of cocycles is the cup product of cochains.

Coboundaries cup to coboundaries

theorem TauCeti.TopPairing.homologyπ_cupCocycles_eq_zero_of_left_eq_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) (m n : ℕ) (a : ↑(ContinuousCohomology.cocycles X m).toModuleCat) (ha : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X m)) a = 0) (b : ↑(ContinuousCohomology.cocycles Y n).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π Z (m + n))) (((P.cupCocycles m n) a) b) = 0

A coboundary cupped with a cocycle is a coboundary: the class of a ⌣ b vanishes when the class of a does.

theorem TauCeti.TopPairing.homologyπ_cupCocycles_eq_zero_of_right_eq_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) (m n : ℕ) (a : ↑(ContinuousCohomology.cocycles X m).toModuleCat) (b : ↑(ContinuousCohomology.cocycles Y n).toModuleCat) (hb : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π Y n)) b = 0) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π Z (m + n))) (((P.cupCocycles m n) a) b) = 0

A cocycle cupped with a coboundary is a coboundary: the class of a ⌣ b vanishes when the class of b does.

The cup product on continuous cohomology

noncomputable def TauCeti.TopPairing.cup {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 : ℕ) : ↑(continuousCohomology m X).toModuleCat →ₗ[R] ↑(continuousCohomology n Y).toModuleCat →ₗ[R] ↑(continuousCohomology (m + n) Z).toModuleCat

The cup product on continuous cohomology, Hᵐ(G, X) →ₗ[R] Hⁿ(G, Y) →ₗ[R] Hᵐ⁺ⁿ(G, Z), for a coefficient pairing P : TopPairing X Y Z: the class of a ⌣ b on the classes of the cocycles a and b (cup_π).

Equations

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

@[simp]

theorem TauCeti.TopPairing.cup_π {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.cocycles X m).toModuleCat) (b : ↑(ContinuousCohomology.cocycles Y n).toModuleCat) : ((P.cup m n) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X m)) a)) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π Y n)) b) = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π Z (m + n))) (((P.cupCocycles m n) a) b)

The cup product on classes: the cup product of the classes of two cocycles is the class of their cup product.