The graded mod-two continuous cohomology algebra

For a topological group G, the groups H^n(G, 𝔽₂) with trivial coefficients form a graded-commutative algebra under the cup product. In characteristic two the Koszul sign is invisible, so the external direct sum

⊕ n : ℕ, H^n(G, 𝔽₂)

is an ordinary commutative ring. This file packages the all-degree cup product along TauCeti.trivialF2TopPairing in that form: the graded ring structure is the general TauCeti.TopPairing.cohomologyGRing of that pairing, whose unit is TauCeti.cohomF2.one, and its value on the direct-sum generators is fixed by TauCeti.cohomF2.of_mul_of.

The coefficient object TauCeti.trivialF2 is an object of TopRep ℤ G, the coefficients over which the existing mod-two corpus is stated, so its cohomology groups carry a priori only a ℤ-module structure. Each of them is nevertheless killed by 2 (TauCeti.cohomF2.two_nsmul_eq_zero), and therefore has its canonical ZMod 2-module structure. The resulting direct sum is a ZMod 2-algebra whose multiplication preserves degrees.

Main definitions

• TauCeti.gradedCohomF2: the external direct sum of the cohomology groups, a commutative ZMod 2-algebra.

Main results

• TauCeti.cohomF2.of_mul_of: multiplication of homogeneous elements is the cup product.
• TauCeti.cohomF2.one_eq_one: the unit class is the 1 of the degree-zero ring; with DirectSum.of_zero_one, it is therefore also the 1 of gradedCohomF2.
• TauCeti.cohomF2.algebraMap_apply: scalars from ZMod 2 lie in degree zero.
• TauCeti.trivialF2Map_one: pullback along a continuous homomorphism preserves the unit.

The cup-product identities used here are the Alexander–Whitney identities in Brown, Cohomology of Groups, Chapter V, §3, and Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, (1.4.4).

@[reducible, inline]

noncomputable abbrev TauCeti.gradedCohomF2 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Type u

The graded mod-two continuous cohomology algebra, as the external direct sum of the groups cohomF2 G n.

@[instance_reducible]

noncomputable instance TauCeti.cohomF2.instGRing (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : DirectSum.GRing (cohomF2 G)

Mod-two continuous cohomology is a graded ring under the cup product along TauCeti.trivialF2TopPairing, with unit TauCeti.cohomF2.one.

@[simp]

theorem TauCeti.cohomF2.gMul_eq_cup (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m n : ℕ} (x : cohomF2 G m) (y : cohomF2 G n) : GradedMonoid.GMul.mul x y = (((trivialF2TopPairing G).cup m n) x) y

The multiplication supplied by the graded ring structure is the cup product.

@[simp]

theorem TauCeti.cohomF2.gOne_eq_one (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : GradedMonoid.GOne.one = one G

The unit supplied by the graded ring structure is the degree-zero unit class.

@[simp]

theorem TauCeti.cohomF2.one_eq_one (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : one G = 1

The unit class is the 1 of the degree-zero ring cohomF2 G 0.

@[instance_reducible]

noncomputable instance TauCeti.cohomF2.instGCommRing (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : DirectSum.GCommRing (cohomF2 G)

In characteristic two the graded-commutative cup product is an ordinary commutative multiplication on the graded pieces.

@[instance_reducible]

noncomputable instance TauCeti.cohomF2.instGAlgebra (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : DirectSum.GAlgebra (ZMod 2) (cohomF2 G)

Degree-zero scalar multiples of the unit make mod-two continuous cohomology a graded ZMod 2-algebra.

@[simp]

theorem TauCeti.cohomF2.of_mul_of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m n : ℕ} (x : cohomF2 G m) (y : cohomF2 G n) : (DirectSum.of (cohomF2 G) m) x * (DirectSum.of (cohomF2 G) n) y = (DirectSum.of (cohomF2 G) (m + n)) ((((trivialF2TopPairing G).cup m n) x) y)

Multiplication of homogeneous elements in gradedCohomF2 is their cup product.

@[simp]

theorem TauCeti.cohomF2.algebraMap_apply (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (r : ZMod 2) : (algebraMap (ZMod 2) (gradedCohomF2 G)) r = (DirectSum.of (cohomF2 G) 0) (r • 1)

The scalar r : ZMod 2 in the total cohomology algebra is the degree-zero class r • 1.

@[simp]

theorem TauCeti.trivialF2Map_one (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) : (CategoryTheory.ConcreteCategory.hom (trivialF2Map φ 0)) 1 = 1

Pullback with trivial 𝔽₂ coefficients along a continuous homomorphism preserves the unit class.