The graded cohomology ring of an associative unital coefficient pairing

Let P : TopPairing X X X be a coefficient pairing of a topological representation X with itself which is associative and has an invariant two-sided unit u. Then the cup product along P makes the family n ↦ Hⁿ(G, X) a graded ring, with unit the degree-zero class of u. This file packages that structure as Mathlib's DirectSum.GRing, so that ⨁ n, Hⁿ(G, X) is a ring.

The unit and associativity laws are the all-degree cup-product identities TauCeti.TopPairing.cup_one_left, TauCeti.TopPairing.cup_one_right and TauCeti.TopPairing.cup_assoc; distributivity is the bilinearity of the cup product. No commutativity is asserted: the cup product is only graded-commutative (TauCeti.TopPairing.cup_gradedComm), so DirectSum.GCommRing is a statement about particular coefficients.

Main definitions

• TauCeti.TopPairing.cohomologyGRing: the graded ring structure on n ↦ Hⁿ(G, X) given by the cup product along P.

Main results

• TauCeti.TopPairing.cohomologyGRing_mul, TauCeti.TopPairing.cohomologyGRing_one: the multiplication of homogeneous classes is the cup product along P, and the unit is the degree-zero class of u.

@[reducible, inline]

noncomputable abbrev TauCeti.TopPairing.cohomologyGRing {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (P : TopPairing X X X) (u : ↑X) (hinv : ∀ (g : G), (X.ρ g) u = u) (hleft : ∀ (x : ↑X), (P.bil u) x = x) (hright : ∀ (x : ↑X), (P.bil x) u = x) (hassoc : ∀ (x y z : ↑X), (P.bil ((P.bil x) y)) z = (P.bil x) ((P.bil y) z)) : DirectSum.GRing fun (n : ℕ) => ↑(continuousCohomology n X).toModuleCat

The graded cohomology ring of a coefficient pairing. For an associative pairing P : TopPairing X X X with a G-invariant two-sided unit u, the cup product along P and the degree-zero class of u make n ↦ Hⁿ(G, X) a graded ring. The multiplication of homogeneous classes is P.cup m n (TauCeti.TopPairing.cohomologyGRing_mul) and the unit is degreeZeroClass X u hinv (TauCeti.TopPairing.cohomologyGRing_one).

This is not an instance, since P and u do not occur in its type; it is reducible so that instances defined from it unfold, see note [reducible non-instances].

@[simp]

theorem TauCeti.TopPairing.cohomologyGRing_mul {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (P : TopPairing X X X) (u : ↑X) (hinv : ∀ (g : G), (X.ρ g) u = u) (hleft : ∀ (x : ↑X), (P.bil u) x = x) (hright : ∀ (x : ↑X), (P.bil x) u = x) (hassoc : ∀ (x y z : ↑X), (P.bil ((P.bil x) y)) z = (P.bil x) ((P.bil y) z)) {m n : ℕ} (x : ↑(continuousCohomology m X).toModuleCat) (y : ↑(continuousCohomology n X).toModuleCat) : GradedMonoid.GMul.mul x y = ((P.cup m n) x) y

The multiplication of homogeneous classes in TauCeti.TopPairing.cohomologyGRing is the cup product along P.

@[simp]

theorem TauCeti.TopPairing.cohomologyGRing_one {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (P : TopPairing X X X) (u : ↑X) (hinv : ∀ (g : G), (X.ρ g) u = u) (hleft : ∀ (x : ↑X), (P.bil u) x = x) (hright : ∀ (x : ↑X), (P.bil x) u = x) (hassoc : ∀ (x y z : ↑X), (P.bil ((P.bil x) y)) z = (P.bil x) ((P.bil y) z)) : GradedMonoid.GOne.one = ContinuousCohomology.degreeZeroClass X u hinv

The unit of TauCeti.TopPairing.cohomologyGRing is the degree-zero class of u.