Corestriction commutes with the coboundary differential

The degree-2 corestriction cochain cor2Fun U (GQ2/Corestriction.lean, eq. (108)) commutes with the group-cohomology differential: for a 𝔽₂-valued 0-cochain-shifted 1-cochain c : ↥U → 𝔽₂ (trivial action), the corestriction of the coboundary δ¹c is the coboundary δ¹(cor¹ c). Written with the explicit trivial-action coboundary (δ¹c)(a,b) = c b − c (a·b) + c a to stay clear of DistribMulAction ↥U (ZMod 2) instance plumbing.

This is the cochain heart of "corestriction descends to H²": it makes the per-orbit contributions of the Lemma-6.17 vanishing clause (ShapiroLedger.lemma_6_15_*, whose outputs are H2ofFun (cor2Fun U (cup of scalar Kummer cocycles))) vanish once the underlying scalar cup does — the deep-class orthogonality LocalKummer.cup_deepClasses. std-3, no axiom.

theorem GQ2.Corestriction.lTrans_mul {G : Type u_1} [Group G] (U : Subgroup G) (u : G ⧸ U) (γ η : G) : lTrans U u γ * lTrans U (γ⁻¹ • u) η = lTrans U u (γ * η)

The transversal 1-cocycle identity (general — no normality): the corestriction word ℓ_u is a 1-cocycle for the left G-action on G ⧸ U.

theorem GQ2.Corestriction.cor2Fun_dOne {G : Type u_1} [Group G] (U : Subgroup G) [Finite (G ⧸ U)] (c : ↥U → ZMod 2) : (cor2Fun U fun (ab : ↥U × ↥U) => c ab.2 - c (ab.1 * ab.2) + c ab.1) = fun (p : G × G) => cor1Fun U c p.2 - cor1Fun U c (p.1 * p.2) + cor1Fun U c p.1

Corestriction commutes with δ¹ (𝔽₂, trivial action): the degree-2 corestriction of the coboundary (a,b) ↦ c b − c (a·b) + c a is the coboundary of the degree-1 corestriction cor1Fun U c.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (108) = ⟦eq-normalized-corestriction-two⟧