The two-point graph cochain of the Evens norm at index two

Let U be a subgroup of index two of a topological group G, let s be an element outside U, and let α : U →* Multiplicative (ZMod 2) be a continuous homomorphism, that is a continuous 1-cocycle of U with trivial 𝔽₂ coefficients. The multiplicative transfer (Evens norm) N^{Ev}(α) ∈ H²(G, 𝔽₂) is, in this degree and at this index, the class of an explicit 2-cochain built from the two components of the Shapiro description of α:

b₁ γ = α γ            (γ ∈ U),        b₁ γ = α (γ s)        (γ ∉ U),
b_s γ = b₁ (s⁻¹ γ),
ν (γ, η) = b₁ γ * b_s η                         (γ ∈ U),
ν (γ, η) = b₁ γ * b₁ η + b₁ η * b_s η           (γ ∉ U).

This file builds b₁, b_s, their sum and ν, and proves the cochain-level facts the class N^{Ev}(α) and its characterizing identities rest on: b₁ and b_s are the two coordinates of a 1-cocycle of G valued in the permutation module 𝔽₂[G/U], so their sum is a continuous homomorphism G → 𝔽₂, and ν is a continuous 2-cocycle whose class does not depend on the element s chosen outside U.

Main definitions

• TauCeti.ContCohomology.evensExtend: a homomorphism on U, extended by zero to G.
• TauCeti.ContCohomology.evensB1 and TauCeti.ContCohomology.evensBs: the two Shapiro components.
• TauCeti.ContCohomology.evensCorCochain: their sum, the shape the degree-one corestriction of α over the transversal {1, s} takes.
• TauCeti.ContCohomology.evensGraphCochain: the two-point graph 2-cochain ν.

Main statements

• TauCeti.ContCohomology.evensExtend_mul_hom, evensB1_mul_hom and evensBs_mul_hom: the extension by zero and the two Shapiro components are additive in the homomorphism.
• TauCeti.ContCohomology.evensB1_mul_of_mem, evensB1_mul_of_notMem, evensBs_mul_of_mem and evensBs_mul_of_notMem: the cocycle law of the pair (b₁, b_s) in the permutation module, from which everything else follows.
• TauCeti.ContCohomology.evensCorCochain_mul: the sum b₁ + b_s is a homomorphism, which neither summand is.
• TauCeti.ContCohomology.evensGraphCochain_cocycle_identity: the 2-cocycle identity for ν, in its trivial-action form.
• TauCeti.ContCohomology.continuous_evensGraphCochain: continuity of ν, for U open.
• TauCeti.ContCohomology.evensGraphCochain_sub_evensGraphCochain: two elements outside U give graph cochains differing by the explicit coboundary of γ ↦ α (s⁻¹ s') * evensExtend U α γ, so the class of ν depends on U and α alone.
• TauCeti.ContCohomology.evensGraphCochain_apply_of_mem_of_mem: on U × U the graph cochain is the cup-product cochain of α with its conjugate η ↦ α (s⁻¹ η s).
• TauCeti.ContCohomology.evensB1_comp_subtype, evensBs_comp_subtype and evensGraphCochain_comp_subtype: for the restriction y|_U of a homomorphism y on G, both Shapiro components are the homomorphism b = y + y(s) · χ_U, with χ_U the character of U, and ν (γ, η) = b γ · b η + χ_U γ · b η.
• TauCeti.ContCohomology.evensExtend_comap, evensB1_comap, evensBs_comap and evensGraphCochain_comap: naturality under pullback along a homomorphism φ : G' →* G.

Implementation notes

b₁ and b_s are cochains and not cocycles, so neither has a class of its own: for G = C₄ = ⟨σ⟩, U = ⟨σ²⟩, s = σ and α ≠ 0, the values of b₁ at 1, σ, σ², σ³ are 0, 1, 1, 0, so b₁ (σ * σ) ≠ b₁ σ + b₁ σ. Only the sum is a homomorphism; the section AcceptanceCheck at the end of this file records that computation, which is why the corestriction statement is about the sum and not about the two components separately.

The element s is data of the cochain formulas and of nothing else. Two elements outside U give graph cochains differing by an explicit coboundary, so the class they define depends on U and α alone; that is TauCeti.ContCohomology.evensGraphCochain_sub_evensGraphCochain, which is stated at every s' outside U rather than at a chosen one.

Everything below is stated for a plain subgroup U together with the hypotheses U.index = 2 for the cocycle identities and the comparison of two elements outside U, and IsOpen (U : Set G) for continuity. The evaluation of the graph cochain on U × U needs neither. The continuity statements need only separately continuous multiplication, since the arguments use fixed translations and the fact that an open subgroup is closed. No topology at all is needed for the algebraic half: the cocycle laws and the comparison of two elements outside U are identities of plain functions G → 𝔽₂.

The 2-cocycle identity is stated in the form it takes for a trivial action, an equation between sums of four values, rather than through groupCohomology.IsCocycle₂, whose statement carries a scalar action of G on 𝔽₂ that nothing here has to fix.

Characteristic two is used only through CharTwo.two_eq_zero and CharTwo.neg_eq, and only in three places: the 2-cocycle identity when γ lies outside U, the comparison of two elements outside U, and the fact that the extension by zero is invariant under inversion. The corresponding identities over a general coefficient ring are false, which is why Evens' expansion is restricted to even degrees away from characteristic two.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Trans. Amer. Math. Soc. 108 (1963), 54–65: the multiplicative transfer, of which the cochain built here is the index-two, degree-one case.
• A. Kozlowski, The Evens–Kahn formula for the total Stiefel–Whitney class, Proc. Amer. Math. Soc. 91 (1984), 309–313: the transfer for double coverings, that is the index-two case, and the formula it gives for a representation induced from a subgroup of index two.
• A. Kozlowski, Transfers in the group of multiplicative units of the classical cohomology ring and Stiefel–Whitney classes, Publ. Res. Inst. Math. Sci. 25 (1989), 59–74: the same transfer on the multiplicative units of the cohomology ring, expressed for double coverings in terms of the Evens transfer; that expression in low degrees is the identity the cochain here is built to satisfy.

A homomorphism on U, extended by zero

noncomputable def TauCeti.ContCohomology.evensExtend {G : Type u} [Group G] (U : Subgroup G) (α : ↥U →* Multiplicative (ZMod 2)) : G → ZMod 2

A homomorphism α : U →* Multiplicative 𝔽₂ — that is, a 1-cocycle of U with trivial coefficients — extended by zero to the whole group: it is Multiplicative.toAdd ∘ α on U and 0 outside. No hypothesis on U or on α is needed to define it; when U is open and α is continuous the extension is continuous, by TauCeti.ContCohomology.continuous_evensExtend. The Shapiro components of the Evens norm are built from it.

Equations

• TauCeti.ContCohomology.evensExtend U α γ = if h : γ ∈ U then Multiplicative.toAdd (α ⟨γ, h⟩) else 0

@[simp]

theorem TauCeti.ContCohomology.evensExtend_of_mem {G : Type u} [Group G] {U : Subgroup G} {α : ↥U →* Multiplicative (ZMod 2)} {γ : G} (h : γ ∈ U) : evensExtend U α γ = Multiplicative.toAdd (α ⟨γ, h⟩)

On U, the extension by zero of α is α, read additively.

@[simp]

theorem TauCeti.ContCohomology.evensExtend_of_notMem {G : Type u} [Group G] {U : Subgroup G} {α : ↥U →* Multiplicative (ZMod 2)} {γ : G} (h : γ ∉ U) : evensExtend U α γ = 0

Off U, the extension by zero of α vanishes.

@[simp]

theorem TauCeti.ContCohomology.evensExtend_mul_hom {G : Type u} [Group G] {U : Subgroup G} {α β : ↥U →* Multiplicative (ZMod 2)} (γ : G) : evensExtend U (α * β) γ = evensExtend U α γ + evensExtend U β γ

The extension by zero is additive in the homomorphism.

@[simp]

theorem TauCeti.ContCohomology.evensExtend_mul {G : Type u} [Group G] {U : Subgroup G} {α : ↥U →* Multiplicative (ZMod 2)} {x y : G} (hx : x ∈ U) (hy : y ∈ U) : evensExtend U α (x * y) = evensExtend U α x + evensExtend U α y

The extension by zero is additive on U, where it is α. It is not additive on G: that failure is what the Evens norm measures.

@[simp]

theorem TauCeti.ContCohomology.evensExtend_inv {G : Type u} [Group G] {U : Subgroup G} {α : ↥U →* Multiplicative (ZMod 2)} (x : G) : evensExtend U α x⁻¹ = evensExtend U α x

The extension by zero is 𝔽₂-valued, so it takes inverses to themselves. No membership hypothesis is needed: on U this is CharTwo.neg_eq, and outside U both sides vanish.

theorem TauCeti.ContCohomology.continuous_evensExtend {G : Type u} [Group G] (U : Subgroup G) (α : ↥U →* Multiplicative (ZMod 2)) [TopologicalSpace G] [SeparatelyContinuousMul G] (hopen : IsOpen ↑U) (hα : Continuous ⇑α) : Continuous (evensExtend U α)

The extension by zero of a continuous homomorphism on an open subgroup is continuous: U is clopen and 𝔽₂ is discrete, so the two branches do not have to agree anywhere.

The two Shapiro components and their sum

noncomputable def TauCeti.ContCohomology.evensB1 {G : Type u} [Group G] (U : Subgroup G) (s : G) (α : ↥U →* Multiplicative (ZMod 2)) : G → ZMod 2

The first Shapiro component b₁ γ = α γ for γ ∈ U and b₁ γ = α (γ s) otherwise.

It is a cochain and not a cocycle, so it has no class of its own; only the sum TauCeti.ContCohomology.evensCorCochain of the two components is a homomorphism.

Equations

• TauCeti.ContCohomology.evensB1 U s α γ = if γ ∈ U then TauCeti.ContCohomology.evensExtend U α γ else TauCeti.ContCohomology.evensExtend U α (γ * s)

noncomputable def TauCeti.ContCohomology.evensBs {G : Type u} [Group G] (U : Subgroup G) (s : G) (α : ↥U →* Multiplicative (ZMod 2)) : G → ZMod 2

The second Shapiro component b_s γ = b₁ (s⁻¹ γ). A cochain, for the same reason as TauCeti.ContCohomology.evensB1.

Equations

• TauCeti.ContCohomology.evensBs U s α γ = TauCeti.ContCohomology.evensB1 U s α (s⁻¹ * γ)

noncomputable def TauCeti.ContCohomology.evensCorCochain {G : Type u} [Group G] (U : Subgroup G) (s : G) (α : ↥U →* Multiplicative (ZMod 2)) : G → ZMod 2

The sum b₁ + b_s of the two Shapiro components, a cochain defined for any U and any s. For U of index two and s ∉ U it is, unlike either summand, a homomorphism, by TauCeti.ContCohomology.evensCorCochain_mul, and it is continuous whenever U is open and α is continuous, by TauCeti.ContCohomology.continuous_evensCorCochain; it is then the shape the degree-one corestriction of α over the transversal {1, s} takes.

Equations

• TauCeti.ContCohomology.evensCorCochain U s α γ = TauCeti.ContCohomology.evensB1 U s α γ + TauCeti.ContCohomology.evensBs U s α γ

@[simp]

theorem TauCeti.ContCohomology.evensB1_of_mem {G : Type u} [Group G] {U : Subgroup G} {s : G} {α : ↥U →* Multiplicative (ZMod 2)} {γ : G} (h : γ ∈ U) : evensB1 U s α γ = evensExtend U α γ

On U, the first Shapiro component b₁ is the extension by zero of α.

@[simp]

theorem TauCeti.ContCohomology.evensB1_of_notMem {G : Type u} [Group G] {U : Subgroup G} {s : G} {α : ↥U →* Multiplicative (ZMod 2)} {γ : G} (h : γ ∉ U) : evensB1 U s α γ = evensExtend U α (γ * s)

Off U, the first Shapiro component is b₁ γ = α (γ s), with α extended by zero.

@[simp]

theorem TauCeti.ContCohomology.evensBs_apply {G : Type u} [Group G] {U : Subgroup G} {s : G} {α : ↥U →* Multiplicative (ZMod 2)} (γ : G) : evensBs U s α γ = evensB1 U s α (s⁻¹ * γ)

The second Shapiro component is b_s γ = b₁ (s⁻¹ γ).

@[simp]

theorem TauCeti.ContCohomology.evensB1_mul_hom {G : Type u} [Group G] {U : Subgroup G} {s : G} {α β : ↥U →* Multiplicative (ZMod 2)} (γ : G) : evensB1 U s (α * β) γ = evensB1 U s α γ + evensB1 U s β γ

The first Shapiro component is additive in the homomorphism.

theorem TauCeti.ContCohomology.evensBs_mul_hom {G : Type u} [Group G] {U : Subgroup G} {s : G} {α β : ↥U →* Multiplicative (ZMod 2)} (γ : G) : evensBs U s (α * β) γ = evensBs U s α γ + evensBs U s β γ

The second Shapiro component is additive in the homomorphism.

@[simp]

theorem TauCeti.ContCohomology.evensCorCochain_apply {G : Type u} [Group G] {U : Subgroup G} {s : G} {α : ↥U →* Multiplicative (ZMod 2)} (γ : G) : evensCorCochain U s α γ = evensB1 U s α γ + evensBs U s α γ

The corestriction cochain is the sum b₁ + b_s of the two Shapiro components.

The four identities below are the cocycle law of the pair (b₁, b_s) read in the permutation module 𝔽₂[G/U]: left translation by an element of U fixes the two coordinates and left translation by an element outside U exchanges them.

They and TauCeti.ContCohomology.evensCorCochain_mul carry @[grind =] rather than @[simp]: their side conditions U.index = 2 and s ∉ U are hypotheses of the ambient context, which grind uses and simp's discharger does not see, and three of them loop as simp lemmas against the unfolding lemma TauCeti.ContCohomology.evensBs_apply, which turns a b_s produced on the right back into a b₁ the left-hand side matches again.

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

Left translation of b₁ by an element of U.

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

Left translation of b₁ by an element outside U produces the other component.

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

Left translation of b_s by an element of U.

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

Left translation of b_s by an element outside U produces the other component.

theorem TauCeti.ContCohomology.evensCorCochain_mul {G : Type u} [Group G] {U : Subgroup G} {s : G} {α : ↥U →* Multiplicative (ZMod 2)} (hU : U.index = 2) (hs : s ∉ U) (γ η : G) : evensCorCochain U s α (γ * η) = evensCorCochain U s α γ + evensCorCochain U s α η

The corestriction cochain is a 1-cocycle. With trivial coefficients a 1-cocycle is a homomorphism; the index-two hypothesis is what makes the two cross terms recombine. Neither TauCeti.ContCohomology.evensB1 nor TauCeti.ContCohomology.evensBs satisfies this on its own, which is why the corestriction is the class of the sum and not of either summand.

theorem TauCeti.ContCohomology.continuous_evensB1 {G : Type u} [Group G] (U : Subgroup G) (s : G) (α : ↥U →* Multiplicative (ZMod 2)) [TopologicalSpace G] [SeparatelyContinuousMul G] (hopen : IsOpen ↑U) (hα : Continuous ⇑α) : Continuous (evensB1 U s α)

The first Shapiro component of a continuous homomorphism on an open subgroup is continuous: U is clopen, so the case split is.

theorem TauCeti.ContCohomology.continuous_evensBs {G : Type u} [Group G] (U : Subgroup G) (s : G) (α : ↥U →* Multiplicative (ZMod 2)) [TopologicalSpace G] [SeparatelyContinuousMul G] (hopen : IsOpen ↑U) (hα : Continuous ⇑α) : Continuous (evensBs U s α)

The second Shapiro component is the first one translated, hence continuous.

theorem TauCeti.ContCohomology.continuous_evensCorCochain {G : Type u} [Group G] (U : Subgroup G) (s : G) (α : ↥U →* Multiplicative (ZMod 2)) [TopologicalSpace G] [SeparatelyContinuousMul G] (hopen : IsOpen ↑U) (hα : Continuous ⇑α) : Continuous (evensCorCochain U s α)

The corestriction cochain of a continuous homomorphism on an open subgroup is continuous.

The two-point graph cochain

noncomputable def TauCeti.ContCohomology.evensGraphCochain {G : Type u} [Group G] (U : Subgroup G) (s : G) (α : ↥U →* Multiplicative (ZMod 2)) : G × G → ZMod 2

The two-point graph 2-cochain of a homomorphism α on an index-two subgroup U at an element s outside it:

ν (γ, η) = b₁ γ * b_s η                        if γ ∈ U,
ν (γ, η) = b₁ γ * b₁ η + b₁ η * b_s η          otherwise.

The formula defines a cochain for any U and any s. For U of index two and s ∉ U it satisfies the 2-cocycle identity, by TauCeti.ContCohomology.evensGraphCochain_cocycle_identity, and it is continuous whenever U is open and α is continuous, by TauCeti.ContCohomology.continuous_evensGraphCochain; under those hypotheses its class in H²(G, 𝔽₂) is the Evens norm N^{Ev}(α).

Equations

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

@[simp]

theorem TauCeti.ContCohomology.evensGraphCochain_of_mem {G : Type u} [Group G] {U : Subgroup G} {s : G} {α : ↥U →* Multiplicative (ZMod 2)} {γ : G} (h : γ ∈ U) (η : G) : evensGraphCochain U s α (γ, η) = evensB1 U s α γ * evensBs U s α η

For γ ∈ U, the graph cochain takes (γ, η) to b₁ γ · b_s η.

@[simp]

theorem TauCeti.ContCohomology.evensGraphCochain_of_notMem {G : Type u} [Group G] {U : Subgroup G} {s : G} {α : ↥U →* Multiplicative (ZMod 2)} {γ : G} (h : γ ∉ U) (η : G) : evensGraphCochain U s α (γ, η) = evensB1 U s α γ * evensB1 U s α η + evensB1 U s α η * evensBs U s α η

For γ ∉ U, the graph cochain takes (γ, η) to b₁ γ · b₁ η + b₁ η · b_s η.

theorem TauCeti.ContCohomology.evensGraphCochain_cocycle_identity {G : Type u} [Group G] {U : Subgroup G} {s : G} {α : ↥U →* Multiplicative (ZMod 2)} (hU : U.index = 2) (hs : s ∉ U) (γ η j : G) : evensGraphCochain U s α (γ * η, j) + evensGraphCochain U s α (γ, η) = evensGraphCochain U s α (η, j) + evensGraphCochain U s α (γ, η * j)

The graph cochain is a 2-cocycle. This is the trivial-action form of the inhomogeneous 2-cocycle identity, the same equation as groupCohomology.IsCocycle₂ with the scalar action dropped. The two cases in which γ lies outside U need characteristic two; the other two hold over any commutative ring.

theorem TauCeti.ContCohomology.continuous_evensGraphCochain {G : Type u} [Group G] (U : Subgroup G) (s : G) (α : ↥U →* Multiplicative (ZMod 2)) [TopologicalSpace G] [SeparatelyContinuousMul G] (hopen : IsOpen ↑U) (hα : Continuous ⇑α) : Continuous (evensGraphCochain U s α)

The graph cochain of a continuous homomorphism on an open subgroup is continuous: the case split is on the clopen set U × G and both branches are products of continuous functions.

The graph cochain on the subgroup

On U × U the graph cochain is the cup-product cochain of α with its conjugate by s, which is again a homomorphism on U since U is normal at index two. This is the cochain form of the identity res_U N^{Ev}(α) = α ⌣ (s · α).

theorem TauCeti.ContCohomology.evensGraphCochain_apply_of_mem_of_mem {G : Type u} [Group G] {U : Subgroup G} {s : G} {α : ↥U →* Multiplicative (ZMod 2)} (hs : s ∉ U) {γ η : G} (hγ : γ ∈ U) (hη : η ∈ U) : evensGraphCochain U s α (γ, η) = evensExtend U α γ * evensExtend U α (s⁻¹ * η * s)

The graph cochain restricted to U is the product of the extension of α with its s-conjugate. This evaluation formula holds for any subgroup and any s ∉ U.

Independence of the element outside U

Two elements outside U give graph cochains differing by an explicit coboundary, so the class of the graph cochain in H²(G, 𝔽₂) depends on U and α alone. This is an identity of plain functions and needs no topology; the 1-cochain whose coboundary it is becomes continuous once G is a topological group, U is open and α is continuous, by TauCeti.ContCohomology.continuous_evensExtend.

theorem TauCeti.ContCohomology.evensB1_eq_add_of_notMem {G : Type u} [Group G] {U : Subgroup G} {s s' : G} {α : ↥U →* Multiplicative (ZMod 2)} (hU : U.index = 2) (hs : s ∉ U) (hs' : s' ∉ U) {γ : G} (hγ : γ ∉ U) : evensB1 U s' α γ = evensB1 U s α γ + evensExtend U α (s⁻¹ * s')

Outside U the first Shapiro component changes by the value of α at s⁻¹ s'.

theorem TauCeti.ContCohomology.evensBs_eq_add_of_notMem {G : Type u} [Group G] {U : Subgroup G} {s s' : G} {α : ↥U →* Multiplicative (ZMod 2)} (hU : U.index = 2) (hs : s ∉ U) (hs' : s' ∉ U) {γ : G} (hγ : γ ∉ U) : evensBs U s' α γ = evensBs U s α γ + evensExtend U α (s⁻¹ * s')

Outside U the second Shapiro component changes by the same value, so the two components move together and their sum, the corestriction cochain, does not change at all.

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

On U the second Shapiro component does not depend on the element chosen outside either: it is evaluated at s⁻¹ γ, which lies outside U, and the change in the first component there is cancelled by the change in the evaluation point.

theorem TauCeti.ContCohomology.evensGraphCochain_sub_evensGraphCochain {G : Type u} [Group G] {U : Subgroup G} {s s' : G} {α : ↥U →* Multiplicative (ZMod 2)} (hU : U.index = 2) (hs : s ∉ U) (hs' : s' ∉ U) (γ η : G) : evensGraphCochain U s' α (γ, η) - evensGraphCochain U s α (γ, η) = evensExtend U α (s⁻¹ * s') * evensExtend U α η - evensExtend U α (s⁻¹ * s') * evensExtend U α (γ * η) + evensExtend U α (s⁻¹ * s') * evensExtend U α γ

The graph cochain does not depend on the element chosen outside U, up to a coboundary. Two elements s and s' outside an index-two subgroup give graph cochains differing by the coboundary of γ ↦ α (s⁻¹ s') * evensExtend U α γ, where TauCeti.ContCohomology.evensExtend is the extension of α by zero. That 1-cochain is continuous whenever α is and U is open, by TauCeti.ContCohomology.continuous_evensExtend, so the class of the graph cochain in H²(G, 𝔽₂) depends on U and α alone.

The graph cochain of a restricted homomorphism

For the restriction y|_U of a homomorphism y : G → 𝔽₂, both Shapiro components are one and the same homomorphism b = y + y(s) · χ_U of G, where χ_U = Subgroup.indexTwoCharacter is the character with kernel U. The graph cochain is then b ⌣ b + χ_U ⌣ b on cochains, which is the cochain form of the identity N^{Ev}(res_U y) = y ⌣ y + χ_U ⌣ y.

theorem TauCeti.ContCohomology.evensB1_comp_subtype {G : Type u} [Group G] {U : Subgroup G} {s : G} (hU : U.index = 2) (hs : s ∉ U) (y : G →* Multiplicative (ZMod 2)) (γ : G) : evensB1 U s (y.comp U.subtype) γ = Multiplicative.toAdd (y γ) + Multiplicative.toAdd (y s) * Multiplicative.toAdd ((U.indexTwoCharacter hU) γ)

The first Shapiro component of a restricted homomorphism is the homomorphism y + y(s) · χ_U of G, with χ_U the character of U.

theorem TauCeti.ContCohomology.evensBs_comp_subtype {G : Type u} [Group G] {U : Subgroup G} {s : G} (hU : U.index = 2) (hs : s ∉ U) (y : G →* Multiplicative (ZMod 2)) : evensBs U s (y.comp U.subtype) = evensB1 U s (y.comp U.subtype)

The two Shapiro components of a restricted homomorphism agree.

theorem TauCeti.ContCohomology.evensGraphCochain_comp_subtype {G : Type u} [Group G] {U : Subgroup G} {s : G} (hU : U.index = 2) (hs : s ∉ U) (y : G →* Multiplicative (ZMod 2)) (γ η : G) : evensGraphCochain U s (y.comp U.subtype) (γ, η) = evensB1 U s (y.comp U.subtype) γ * evensB1 U s (y.comp U.subtype) η + Multiplicative.toAdd ((U.indexTwoCharacter hU) γ) * evensB1 U s (y.comp U.subtype) η

The graph cochain of a restricted homomorphism. With b the common Shapiro component of y|_U (TauCeti.ContCohomology.evensB1_comp_subtype) and χ_U the character of U, the graph cochain is ν (γ, η) = b γ · b η + χ_U γ · b η.

Naturality under pullback along a homomorphism

Pulling U and α back along a homomorphism φ : G' →* G and taking the cochains at s ∈ G' gives the cochains of U and α at φ s, composed with φ. No hypothesis on U, α or φ is needed: membership in U.comap φ is membership of the image in U.

theorem TauCeti.ContCohomology.evensExtend_comap {G : Type u} [Group G] {G' : Type u_1} [Group G'] (φ : G' →* G) (U : Subgroup G) (α : ↥U →* Multiplicative (ZMod 2)) (γ : G') : evensExtend (Subgroup.comap φ U) (α.comp (φ.subgroupComap U)) γ = evensExtend U α (φ γ)

The extension by zero commutes with pullback along a homomorphism.

theorem TauCeti.ContCohomology.evensB1_comap {G : Type u} [Group G] {G' : Type u_1} [Group G'] (φ : G' →* G) (U : Subgroup G) (s : G') (α : ↥U →* Multiplicative (ZMod 2)) (γ : G') : evensB1 (Subgroup.comap φ U) s (α.comp (φ.subgroupComap U)) γ = evensB1 U (φ s) α (φ γ)

The first Shapiro component commutes with pullback along a homomorphism.

theorem TauCeti.ContCohomology.evensBs_comap {G : Type u} [Group G] {G' : Type u_1} [Group G'] (φ : G' →* G) (U : Subgroup G) (s : G') (α : ↥U →* Multiplicative (ZMod 2)) (γ : G') : evensBs (Subgroup.comap φ U) s (α.comp (φ.subgroupComap U)) γ = evensBs U (φ s) α (φ γ)

The second Shapiro component commutes with pullback along a homomorphism.

theorem TauCeti.ContCohomology.evensGraphCochain_comap {G : Type u} [Group G] {G' : Type u_1} [Group G'] (φ : G' →* G) (U : Subgroup G) (s : G') (α : ↥U →* Multiplicative (ZMod 2)) (γ η : G') : evensGraphCochain (Subgroup.comap φ U) s (α.comp (φ.subgroupComap U)) (γ, η) = evensGraphCochain U (φ s) α (φ γ, φ η)

Naturality of the graph cochain: the graph cochain of the pullback of U and α along φ : G' →* G, at s, is the graph cochain of U and α at φ s, composed with φ × φ.

The two components are not cocycles

Evaluated at (s, s) neither Shapiro component is additive as soon as α (s²) ≠ 0, while their sum is. The smallest instance is G = C₄ = ⟨σ⟩ with U = ⟨σ²⟩, s = σ and α ≠ 0, where the values of b₁ at 1, σ, σ², σ³ are 0, 1, 1, 0. Giving b₁ and b_s classes of their own would be a type error dressed as a statement, and this is the computation that catches it.