Restriction of the explicit Evens graph-cocycle class

Let U be an open subgroup of index two in a topological group G and let α : U →* Multiplicative (ZMod 2) be a continuous homomorphism. For a chosen s ∉ U, this file computes the restriction of the class of evensGraphCocycle U s α in the explicit inhomogeneous cohomology model. It is the (1,1) cup product of the class of α with its conjugate, for the multiplication pairing of 𝔽₂:

res_U [graph_s(α)] = [α] ⌣ evensConj1([α]).

Here TauCeti.ContCohomology.evensConj1 is defined on explicit H¹ as res ∘ cor - id, and equals conjugation by every element outside U. The class of α is represented by the cocycle TauCeti.ContCohomology.evensHomCocycleAmbient with the lifted trivial 𝔽₂ coefficients of the ambient group.

The same formula holds for the choice-free class TauCeti.ContCohomology.explicitGraphClass, of which the graph cocycle for a chosen s ∉ U is a representative.

Main results

• TauCeti.ContCohomology.explicitRes2_evensGraphCocycle: in explicit cohomology, the restriction of the graph-cocycle class for a chosen s ∉ U is the cup product with the conjugate class.
• TauCeti.ContCohomology.explicitRes2_explicitGraphClass: the same identity for the choice-free graph class, with no representative on either side.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Trans. Amer. Math. Soc. 108 (1963), 54–65.
• A. Kozlowski, The Evens–Kahn formula for the total Stiefel–Whitney class, Proc. Amer. Math. Soc. 91 (1984), 309–313, Lemma 2.4.

theorem TauCeti.ContCohomology.instContinuousSMulVIntTrivialF2_2 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ContinuousSMul G ↑(trivialF2 G)

G acts continuously on the trivial coefficients 𝔽₂, which are smooth discrete.

theorem TauCeti.ContCohomology.explicitRes2_evensGraphCocycle {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (hU : (↑U).index = 2) {s : G} (hs : s ∉ U) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : (explicitRes2 G ↑(trivialF2 G) ↑U) ↑(evensGraphCocycle U s α hU hs hα) = ((explicitCup11 (↥↑U) (↑(trivialF2 G)) (↑(trivialF2 G)) (↑(trivialF2 G)) (trivialF2Pairing G) ⋯ ⋯) ↑(evensHomCocycleAmbient (↑U) α hα)) ((evensConj1 G (↑(trivialF2 G)) (↑U) hU ⋯) ↑(evensHomCocycleAmbient (↑U) α hα))

Restriction of the explicit graph-cocycle class for a chosen s ∉ U is the (1,1) cup product of the class of α with its choice-free conjugate TauCeti.ContCohomology.evensConj1, for the multiplication pairing of 𝔽₂. Both sides lie in explicit H²(U, 𝔽₂).

theorem TauCeti.ContCohomology.explicitRes2_explicitGraphClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : (explicitRes2 G ↑(trivialF2 G) ↑U) (explicitGraphClass U hU α hα) = ((explicitCup11 (↥↑U) (↑(trivialF2 G)) (↑(trivialF2 G)) (↑(trivialF2 G)) (trivialF2Pairing G) ⋯ ⋯) ↑(evensHomCocycleAmbient (↑U) α hα)) ((evensConj1 G (↑(trivialF2 G)) (↑U) hU ⋯) ↑(evensHomCocycleAmbient (↑U) α hα))

Restriction of the index-two Evens graph class. Restriction of the choice-free graph class TauCeti.ContCohomology.explicitGraphClass is the (1,1) cup product of the class of α with its choice-free conjugate. Both sides lie in explicit H²(U, 𝔽₂); unlike explicitRes2_evensGraphCocycle, neither mentions a representative.