The index-two graph cochain as a pullback of the D₁₆ extension cocycle

Let U be a subgroup of index two of a group G, let s be an element outside U and let α : U →* Multiplicative (ZMod 2) be a homomorphism. The two-point graph cochain ν_α of TauCeti.RepresentationTheory.Homological.ContCohomology.Evens.Cochain represents the index-two Evens norm of α. This file identifies ν_α, on the nose, with the pullback of the factor set of the central extension 1 → C₂ → D₁₆ → C₂ ≀ C₂ → 1 plus an explicit coboundary.

The universal case is the base group U₀ = C₂ × C₂ of C₂ ≀ C₂ with its tautological character (a, b, 0) ↦ a. At every element t = (a, 0, 1) outside U₀ the two Shapiro components of the tautological character are the first two coordinates, and the graph cochain is

ν_taut = c_{D₁₆} + δ w,        w (a, b, c) = a + c,

where c_{D₁₆} is the factor set TauCeti.wreathD16Cocycle and w is the indicator of {u, u v, s, v s}, with u = (1, 0, 0), v = (0, 1, 0) and s = (0, 0, 1) (TauCeti.ContCohomology.evensGraphCochain_wreath). This is a finite computation.

For general U, s and α, the induced homomorphism Ind α : G → C₂ ≀ C₂, γ ↦ (b₁ γ, b_s γ, χ_U γ), built from the two Shapiro components and the character χ_U of U, is a homomorphism by the cocycle law of the pair (b₁, b_s). It pulls U₀ back to U and the tautological character back to α, and it sends s to an element of the form (a, 0, 1). Hence ν_α is the pullback of ν_taut along Ind α, and so

ν_α = c_{D₁₆} ∘ (Ind α × Ind α) + δ (w ∘ Ind α)

(TauCeti.ContCohomology.evensGraphCochain_eq_indexTwoInd_pullback). When U is open and α is continuous, Ind α is locally constant, so both pulled-back functions are continuous. On classes, the coboundary disappears: the index-two Evens norm of the class of α is the class of the pulled-back D₁₆ factor set,

N^{Ev}(α) = (Ind α)^* c_{D₁₆}

(TauCeti.ContCohomology.evensNormIndexTwo_eq_ind_pullback).

Read through the signed-permutation representation C₂ ≀ C₂ ⊂ O₂, Ind α is the representation induced from α. By Kahn and Serre, the class of c_{D₁₆} is the second Stiefel–Whitney class of that representation of C₂ ≀ C₂, so the identity above is the cochain-level form of the statement that the index-two Evens norm of α is w₂ of the induced representation; the Stiefel–Whitney reading is not formalised here.

Main definitions

• TauCeti.ContCohomology.wreathWitness: the coboundary witness w = 1_{{u, uv, s, vs}}.
• TauCeti.ContCohomology.indexTwoInd: the induced homomorphism Ind α : G →* C₂ ≀ C₂.

Main results

• TauCeti.ContCohomology.evensGraphCochain_wreath: the universal identity ν_taut = c_{D₁₆} + δ w on C₂ ≀ C₂.
• TauCeti.ContCohomology.comap_indexTwoInd_wreathBase and TauCeti.ContCohomology.wreathTautological_indexTwoInd: Ind α pulls the base group back to U and the tautological character back to α.
• TauCeti.ContCohomology.evensGraphCochain_indexTwoInd: ν_α is the pullback of ν_taut along Ind α.
• TauCeti.ContCohomology.evensGraphCochain_eq_indexTwoInd_pullback: ν_α = c_{D₁₆} ∘ (Ind α × Ind α) + δ (w ∘ Ind α).
• TauCeti.ContCohomology.isLocallyConstant_indexTwoInd, TauCeti.ContCohomology.continuous_wreathD16Cocycle_indexTwoInd and TauCeti.ContCohomology.continuous_wreathWitness_indexTwoInd: continuity of the pulled-back cocycle and witness.
• TauCeti.ContCohomology.evensNormIndexTwo_eq_ind_pullback: the index-two Evens norm of the class of α is the class of c_{D₁₆} ∘ (Ind α × Ind α).

References

• B. Kahn, Classes de Stiefel-Whitney de formes quadratiques et de représentations galoisiennes réelles, Invent. Math. 78 (1984), 223–256, th. I.4.2 and Remarque II.2.3.
• J.-P. Serre, L'invariant de Witt de la forme Tr(x²), Comment. Math. Helv. 59 (1984), 651–676, Théorème 1′.
• A. Kozlowski, The Evens–Kahn formula for the total Stiefel–Whitney class, Proc. Amer. Math. Soc. 91 (1984), 309–313.

The universal case: the tautological character of C₂ ≀ C₂

theorem TauCeti.ContCohomology.evensB1_wreath {t : WreathC2} (hB : t.coordB = 0) (hC : t.coordC = 1) (g : WreathC2) : evensB1 wreathBase t wreathTautological g = g.coordA

The first Shapiro component of the tautological character is the first coordinate, at every element t = (a, 0, 1) outside the base group.

theorem TauCeti.ContCohomology.evensBs_wreath {t : WreathC2} (hB : t.coordB = 0) (hC : t.coordC = 1) (g : WreathC2) : evensBs wreathBase t wreathTautological g = g.coordB

The second Shapiro component of the tautological character is the second coordinate, at every element t = (a, 0, 1) outside the base group.

def TauCeti.ContCohomology.wreathWitness (g : WreathC2) : ZMod 2

The coboundary witness w = 1_{{u, uv, s, vs}} on C₂ ≀ C₂, which on coordinates is a + c (TauCeti.ContCohomology.wreathWitness_eq_one_iff). Its coboundary is the difference between the graph cochain of the tautological character and the D₁₆ extension cocycle.

theorem TauCeti.ContCohomology.wreathWitness_eq_one_iff (g : WreathC2) : wreathWitness g = 1 ↔ g = WreathC2.mk 1 0 0 ∨ g = WreathC2.mk 1 0 0 * WreathC2.mk 0 1 0 ∨ g = WreathC2.mk 0 0 1 ∨ g = WreathC2.mk 0 1 0 * WreathC2.mk 0 0 1

The witness is the indicator of {u, uv, s, vs}, with u = (1, 0, 0), v = (0, 1, 0) and s = (0, 0, 1).

theorem TauCeti.ContCohomology.evensGraphCochain_wreath {t : WreathC2} (hB : t.coordB = 0) (hC : t.coordC = 1) (g h : WreathC2) : evensGraphCochain wreathBase t wreathTautological (g, h) = wreathD16Cocycle (g, h) + (wreathWitness h - wreathWitness (g * h) + wreathWitness g)

The universal identity: the graph cochain of the tautological character of C₂ ≀ C₂, at every element t = (a, 0, 1) outside the base group, is the D₁₆ extension cocycle plus the coboundary of the witness, ν_taut = c_{D₁₆} + δ w. This is an identity of cochains; the consequence that the index-two Evens norm of the tautological character is the class of the extension D₁₆ → C₂ ≀ C₂ needs passing from cochains to classes and is not formalised here.

The induced homomorphism Ind α : G → C₂ ≀ C₂

noncomputable def TauCeti.ContCohomology.indexTwoInd {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) : G →* WreathC2

The induced homomorphism Ind α : G →* C₂ ≀ C₂ of a homomorphism α on a subgroup U of index two, at an element s ∉ U: γ ↦ (b₁ γ, b_s γ, χ_U γ), with b₁, b_s the two Shapiro components of α and χ_U the character of U. It is a homomorphism by the cocycle law of the pair (b₁, b_s) in the permutation module 𝔽₂[G ⧸ U], which is the multiplication of C₂ ≀ C₂ read on coordinates. Read through C₂ ≀ C₂ ⊂ O₂, it is the representation induced from α.

theorem TauCeti.ContCohomology.indexTwoInd_apply {G : Type u} [Group G] {U : Subgroup G} {hU : U.index = 2} {s : G} {hs : s ∉ U} {α : ↥U →* Multiplicative (ZMod 2)} (γ : G) : (indexTwoInd U hU s hs α) γ = WreathC2.mk (evensB1 U s α γ) (evensBs U s α γ) (Multiplicative.toAdd ((U.indexTwoCharacter hU) γ))

Ind α (γ) has coordinates (b₁ γ, b_s γ, χ_U γ).

@[simp]

theorem TauCeti.ContCohomology.coordA_indexTwoInd {G : Type u} [Group G] {U : Subgroup G} {hU : U.index = 2} {s : G} {hs : s ∉ U} {α : ↥U →* Multiplicative (ZMod 2)} (γ : G) : ((indexTwoInd U hU s hs α) γ).coordA = evensB1 U s α γ

The first coordinate of Ind α is the first Shapiro component b₁.

@[simp]

theorem TauCeti.ContCohomology.coordB_indexTwoInd {G : Type u} [Group G] {U : Subgroup G} {hU : U.index = 2} {s : G} {hs : s ∉ U} {α : ↥U →* Multiplicative (ZMod 2)} (γ : G) : ((indexTwoInd U hU s hs α) γ).coordB = evensBs U s α γ

The second coordinate of Ind α is the second Shapiro component b_s.

@[simp]

theorem TauCeti.ContCohomology.coordC_indexTwoInd {G : Type u} [Group G] {U : Subgroup G} {hU : U.index = 2} {s : G} {hs : s ∉ U} {α : ↥U →* Multiplicative (ZMod 2)} (γ : G) : ((indexTwoInd U hU s hs α) γ).coordC = Multiplicative.toAdd ((U.indexTwoCharacter hU) γ)

The third coordinate of Ind α is the character χ_U of U.

theorem TauCeti.ContCohomology.indexTwoInd_mem_wreathBase_iff {G : Type u} [Group G] {U : Subgroup G} {hU : U.index = 2} {s : G} {hs : s ∉ U} {α : ↥U →* Multiplicative (ZMod 2)} {γ : G} : (indexTwoInd U hU s hs α) γ ∈ wreathBase ↔ γ ∈ U

Ind α (γ) lies in the base group exactly when γ lies in U.

theorem TauCeti.ContCohomology.comap_indexTwoInd_wreathBase {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) : Subgroup.comap (indexTwoInd U hU s hs α) wreathBase = U

Ind α pulls the base group of C₂ ≀ C₂ back to U.

theorem TauCeti.ContCohomology.coordA_indexTwoInd_coe {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) (γ : ↥U) : ((indexTwoInd U hU s hs α) ↑γ).coordA = Multiplicative.toAdd (α γ)

Ind α pulls the tautological character back to α: on U, which Ind α maps into the base group, the first coordinate of Ind α is α.

theorem TauCeti.ContCohomology.wreathTautological_indexTwoInd {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) : wreathTautological.comp ((indexTwoInd U hU s hs α).subgroupComap wreathBase) = α.comp (MulEquiv.subgroupCongr ⋯).toMonoidHom

Ind α pulls the tautological character back to α, as homomorphisms on wreathBase.comap (Ind α), which is identified with U by TauCeti.ContCohomology.comap_indexTwoInd_wreathBase.

theorem TauCeti.ContCohomology.coordB_indexTwoInd_self {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) : ((indexTwoInd U hU s hs α) s).coordB = 0

The second coordinate of Ind α (s) vanishes: b_s (s) = b₁ (1) = 0.

theorem TauCeti.ContCohomology.coordC_indexTwoInd_self {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) : ((indexTwoInd U hU s hs α) s).coordC = 1

The third coordinate of Ind α (s) is 1: Ind α (s) lies outside the base group.

theorem TauCeti.ContCohomology.evensGraphCochain_indexTwoInd {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) (g h : G) : evensGraphCochain U s α (g, h) = evensGraphCochain wreathBase ((indexTwoInd U hU s hs α) s) wreathTautological ((indexTwoInd U hU s hs α) g, (indexTwoInd U hU s hs α) h)

The graph cochain of α is the pullback along Ind α of the graph cochain of the tautological character, taken at Ind α (s).

theorem TauCeti.ContCohomology.evensGraphCochain_eq_indexTwoInd_pullback {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) (g h : G) : evensGraphCochain U s α (g, h) = wreathD16Cocycle ((indexTwoInd U hU s hs α) g, (indexTwoInd U hU s hs α) h) + (wreathWitness ((indexTwoInd U hU s hs α) h) - wreathWitness ((indexTwoInd U hU s hs α) (g * h)) + wreathWitness ((indexTwoInd U hU s hs α) g))

The index-two graph cochain is the pulled-back D₁₆ extension cocycle plus a pulled-back coboundary, on the nose: ν_α = c_{D₁₆} ∘ (Ind α × Ind α) + δ (w ∘ Ind α), with w the witness TauCeti.ContCohomology.wreathWitness.

theorem TauCeti.ContCohomology.isLocallyConstant_indexTwoInd {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) [TopologicalSpace G] [SeparatelyContinuousMul G] (hopen : IsOpen ↑U) (hα : Continuous ⇑α) : IsLocallyConstant ⇑(indexTwoInd U hU s hs α)

Ind α is locally constant when U is open and α is continuous: its three coordinates are continuous maps to the discrete ZMod 2.

theorem TauCeti.ContCohomology.continuous_wreathD16Cocycle_indexTwoInd {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) [TopologicalSpace G] [SeparatelyContinuousMul G] (hopen : IsOpen ↑U) (hα : Continuous ⇑α) : Continuous fun (q : G × G) => wreathD16Cocycle ((indexTwoInd U hU s hs α) q.1, (indexTwoInd U hU s hs α) q.2)

The pulled-back D₁₆ extension cocycle is continuous when U is open and α is continuous.

theorem TauCeti.ContCohomology.continuous_wreathWitness_indexTwoInd {G : Type u} [Group G] (U : Subgroup G) (hU : U.index = 2) (s : G) (hs : s ∉ U) (α : ↥U →* Multiplicative (ZMod 2)) [TopologicalSpace G] [SeparatelyContinuousMul G] (hopen : IsOpen ↑U) (hα : Continuous ⇑α) : Continuous fun (γ : G) => wreathWitness ((indexTwoInd U hU s hs α) γ)

The pulled-back coboundary witness is continuous when U is open and α is continuous.

The index-two norm as the pullback of the D₁₆ class

theorem TauCeti.ContCohomology.evensNormIndexTwo_eq_ind_pullback {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (s : G) (hs : s ∉ U) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) : evensNormIndexTwo U hU (homClass (↥↑U) α hα) = (trivialF2 G).cochainClass 2 (inhomogeneousCochain2 (fun (q : G × G) => wreathD16Cocycle ((indexTwoInd (↑U) hU s hs α) q.1, (indexTwoInd (↑U) hU s hs α) q.2)) ⋯) ⋯

The index-two Evens norm is the pullback of the D₁₆ extension class: N^{Ev}(α) = (Ind α)^* c_{D₁₆}, the class of c_{D₁₆} ∘ (Ind α × Ind α), at every s ∉ U. The norm of the class of α is the class of the graph cochain at s, which differs from the pulled-back factor set by the coboundary of w ∘ Ind α (TauCeti.ContCohomology.evensGraphCochain_eq_indexTwoInd_pullback).