B9: corestriction, the index-two Evens norm, and eq. (111)'s ingredients

Statement infrastructure for the paper's Evens/Kahn/Kozlowski leaf (B9): the paper's eq. (111)

w(Tr_{L/k}⟨a⟩) = w(Tr_{L/k}⟨1⟩) · (1 + cor_{L/k}[a] + N^{Ev}_{L/k}([a]))

(Kahn, Théorème 2 at the rank-1 form ⟨a⟩, expanded through Evens' Theorem 1 for index 2; the index-2 case is Kozlowski Thm 1.1) — truncated to degrees ≤ 2 and scoped to the concrete diagonalizations the paper uses in Lemma 6.16. The axiom itself (GQ2.evensKahn_dyadic, the degree-1 and degree-2 components of (111)) lives in GQ2/Foundations/Axioms.lean; this file provides all definitions and their well-formedness.

What is defined (all unconditional constructions)

For a topological group G, an open subgroup U of index 2 and a fixed s ∉ U, and a continuous homomorphism α : U → 𝔽₂ (a trivial-action 1-cocycle):

• evensAux U s α : G → 𝔽₂ — the paper's normalized Shapiro cocycle component b(γ)₁ = α(γ·s̃^{c(γ)}) of eq. (97) (c(γ) = [γ ∉ U]); the other component is bS U s α = evensAux U s α ∘ (s⁻¹·) (a simplification of (97) recorded here: b(γ)_s = b(s⁻¹γ)₁).
• corFun U s α = b₁ + b_s — the degree-1 corestriction cocycle (sum over the coset transversal {1, s}); corFun_mem_Z1 packages it for Z¹(G, 𝔽₂).
• evensNormFun U s α : G × G → 𝔽₂ — the paper's two-point graph cocycle (98): ν_α(γ,η) = b(γ)₁·b(η)_{γ̄⁻¹s} + ε(γ̄)·b(η)₁·b(η)_s; evensNormH2 packages its class in H²(G,𝔽₂). By the paper's Lemma 6.13 (eq. (99)) this class is the index-two Evens norm N^{Ev}([α]) — we define the Evens norm by this cocycle, exactly as the plan prescribes ("transcribe (95)–(98) as the definition").
• Over k with algebraic closure k̄ (the Kummer-class API's setting): kummerZ1On — the Kummer cocycle of a ∈ Lˣ over the subgroup N = G_L (β² = a, N fixing a), generalizing the Kummer-class API's full-group kummerCocycle to elements algebraic over k.
• Stiefel–Whitney classes of diagonal rank-2 forms are notational: for ⟨x, y⟩ over ℚ₂, w₁ = [x] + [y] (Kummer classes, the Kummer-class API) and w₂ = [x] ∪ [y] (trivialCupPairing, the Demushkin interface/the cup-product API). Following the plan, no QuadraticForm machinery is used: (111) is asserted at the paper's fixed diagonal representatives Tr_{L/k}⟨a⟩ ≃ ⟨2u, 2dn/u⟩, Tr_{L/k}⟨1⟩ ≃ ⟨2, 2d⟩ (Lemma 6.16), absorbing the Delzant well-definedness question into the axiom's scoping. Deviation flagged.

The cocycle identity

ν_α ∈ Z² is proved from the uniform expansion rules (index 2)

b₁(xy) = b₁(x) + D₀(x;y), b_s(xy) = b_s(x) + D₁(x;y),

where D₀(x;y) = if x ∈ U then b₁(y) else b_s(y) and D₁ is the other branch; the cocycle sum then cancels pairwise in characteristic 2 using D₀(h;k)·D₁(h;k) = b₁(k)·b_s(k). Convention anchor (checked by hand, model G = C₄ ⊇ U = C₂, α ≠ 0): the class restricts on U to the nontrivial H²(C₂)-class, and the fibre extension of the universal two-point cocycle is D₈ (paper, Lemma 6.13).

Citations

Evens, Trans. AMS 108 (1963), Thm 1 (§§4–5); Kahn, Invent. Math. 78 (1984), Théorèmes 1–3; Kozlowski, Proc. AMS 91 (1984), Thm 1.1; paper §6, eqs. (95)–(100), (111), Lemmas 6.13/6.16. docs/literature-axioms.md B9.

Index-2 helpers

theorem GQ2.mul_mem_iff_of_index_two {G : Type u_1} [Group G] {U : Subgroup G} (h : U.index = 2) (x y : G) : x * y ∈ U ↔ (x ∈ U ↔ y ∈ U)

Product membership for an index-2 subgroup: xy ∈ U ↔ (x ∈ U ↔ y ∈ U).

theorem GQ2.notMem_mul_mem {G : Type u_1} [Group G] {U : Subgroup G} (h : U.index = 2) {x y : G} (hx : x ∉ U) (hy : y ∉ U) : x * y ∈ U

theorem GQ2.notMem_mul_notMem {G : Type u_1} [Group G] {U : Subgroup G} (h : U.index = 2) {x y : G} (hx : x ∉ U) (hy : y ∈ U) : x * y ∉ U

theorem GQ2.inv_notMem {G : Type u_1} [Group G] {U : Subgroup G} {s : G} (hs : s ∉ U) : s⁻¹ ∉ U

The Shapiro components b₁, b_s and their expansion rules

noncomputable def GQ2.evensAux {G : Type u_1} [Group G] (U : Subgroup G) (s : G) (α : ↥U → ZMod 2) : G → ZMod 2

The first Shapiro component (paper eq. (97), u = 1): b(γ)₁ = α(γ) for γ ∈ U and α(γs) otherwise. (Total function: junk 0 if the membership bookkeeping fails, which cannot happen at index 2.)

Equations

• GQ2.evensAux U s α x = if hx : x ∈ U then α ⟨x, hx⟩ else if hxs : x * s ∈ U then α ⟨x * s, hxs⟩ else 0

noncomputable def GQ2.bS {G : Type u_1} [Group G] (U : Subgroup G) (s : G) (α : ↥U → ZMod 2) : G → ZMod 2

The second Shapiro component b(γ)_s, via the identity b(γ)_s = b(s⁻¹γ)₁.

Equations

• GQ2.bS U s α x = GQ2.evensAux U s α (s⁻¹ * x)

theorem GQ2.evensAux_of_mem {G : Type u_1} [Group G] {U : Subgroup G} {s : G} (α : ↥U → ZMod 2) {x : G} (hx : x ∈ U) : evensAux U s α x = α ⟨x, hx⟩

theorem GQ2.evensAux_of_notMem {G : Type u_1} [Group G] {U : Subgroup G} {s : G} (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) {x : G} (hx : x ∉ U) : evensAux U s α x = α ⟨x * s, ⋯⟩

theorem GQ2.bS_of_mem {G : Type u_1} [Group G] {U : Subgroup G} {s : G} (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) {x : G} (hx : x ∈ U) : bS U s α x = α ⟨s⁻¹ * x * s, ⋯⟩

theorem GQ2.bS_of_notMem {G : Type u_1} [Group G] {U : Subgroup G} {s : G} (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) {x : G} (hx : x ∉ U) : bS U s α x = α ⟨s⁻¹ * x, ⋯⟩

theorem GQ2.evensAux_mul {G : Type u_1} [Group G] {U : Subgroup G} {s : G} (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) (hα : ∀ (u v : ↥U), α (u * v) = α u + α v) (x y : G) : evensAux U s α (x * y) = evensAux U s α x + if x ∈ U then evensAux U s α y else bS U s α y

Expansion rule for b₁ on a product.

theorem GQ2.bS_mul {G : Type u_1} [Group G] {U : Subgroup G} {s : G} (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) (hα : ∀ (u v : ↥U), α (u * v) = α u + α v) (x y : G) : bS U s α (x * y) = bS U s α x + if x ∈ U then bS U s α y else evensAux U s α y

Expansion rule for b_s on a product (the two branches swap).

Continuity

theorem GQ2.evensAux_continuous {G : Type u_1} [Group G] {U : Subgroup G} {s : G} [TopologicalSpace G] [IsTopologicalGroup G] (hUo : IsOpen ↑U) (hUi : U.index = 2) (hs : s ∉ U) {α : ↥U → ZMod 2} (hαc : Continuous α) : Continuous (evensAux U s α)

b₁ is locally constant, hence continuous: on U it is α ∘ ι, off U it is α ∘ (·s) ∘ ι, both witnessed on open sets.

Degree-1 corestriction

noncomputable def GQ2.corFun {G : Type u_1} [Group G] (U : Subgroup G) (s : G) (α : ↥U → ZMod 2) : G → ZMod 2

The degree-1 corestriction cocycle: cor(α) = b₁ + b_s (sum over the transversal {1, s}).

Equations

• GQ2.corFun U s α x = GQ2.evensAux U s α x + GQ2.bS U s α x

theorem GQ2.corFun_hom {G : Type u_1} [Group G] {U : Subgroup G} {s : G} (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) (hα : ∀ (u v : ↥U), α (u * v) = α u + α v) (x y : G) : corFun U s α (x * y) = corFun U s α x + corFun U s α y

cor(α) is a homomorphism (the two expansion cross-terms recombine).

theorem GQ2.corFun_mem_Z1 {G : Type u_1} [Group G] {U : Subgroup G} {s : G} [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] (htriv : ∀ (g : G) (m : ZMod 2), g • m = m) (hUo : IsOpen ↑U) (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) (hα : ∀ (u v : ↥U), α (u * v) = α u + α v) (hαc : Continuous α) : corFun U s α ∈ ContCoh.Z1 G (ZMod 2)

cor(α) as a continuous 1-cocycle (trivial action): membership in Z¹(G, 𝔽₂).

noncomputable def GQ2.corH1 {G : Type u_1} [Group G] {U : Subgroup G} {s : G} [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] (htriv : ∀ (g : G) (m : ZMod 2), g • m = m) (hUo : IsOpen ↑U) (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) (hα : ∀ (u v : ↥U), α (u * v) = α u + α v) (hαc : Continuous α) : ContCoh.H1 G (ZMod 2)

The degree-1 corestriction class cor([α]) ∈ H¹(G, 𝔽₂).

Equations

• GQ2.corH1 htriv hUo hUi hs α hα hαc = (GQ2.ContCoh.H1mk G (ZMod 2)) ⟨GQ2.corFun U s α, ⋯⟩

The index-two Evens norm (the paper's two-point graph cocycle (98))

noncomputable def GQ2.evensNormFun {G : Type u_1} [Group G] (U : Subgroup G) (s : G) (α : ↥U → ZMod 2) : G × G → ZMod 2

The paper's eq. (98): ν_α(γ,η) = b(γ)₁·b(η)_{γ̄⁻¹s} + ε(γ̄)·b(η)₁·b(η)_s. Its class is the index-two Evens norm N^{Ev}_{U→G}([α]) (paper Lemma 6.13, eq. (99)).

Equations

• GQ2.evensNormFun U s α q = if q.1 ∈ U then GQ2.evensAux U s α q.1 * GQ2.bS U s α q.2 else GQ2.evensAux U s α q.1 * GQ2.evensAux U s α q.2 + GQ2.evensAux U s α q.2 * GQ2.bS U s α q.2

theorem GQ2.evensNormFun_continuous {G : Type u_1} [Group G] {U : Subgroup G} {s : G} [TopologicalSpace G] [IsTopologicalGroup G] (hUo : IsOpen ↑U) (hUi : U.index = 2) (hs : s ∉ U) {α : ↥U → ZMod 2} (hαc : Continuous α) : Continuous (evensNormFun U s α)

theorem GQ2.evensNormFun_mem_Z2 {G : Type u_1} [Group G] {U : Subgroup G} {s : G} [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] (htriv : ∀ (g : G) (m : ZMod 2), g • m = m) (hUo : IsOpen ↑U) (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) (hα : ∀ (u v : ↥U), α (u * v) = α u + α v) (hαc : Continuous α) : evensNormFun U s α ∈ ContCoh.Z2 G (ZMod 2)

ν_α is a 2-cocycle — the pairwise-cancellation calculation of the module docstring (uniform expansion rules + D₀·D₁ = b₁(k)·b_s(k), characteristic 2).

noncomputable def GQ2.evensNormH2 {G : Type u_1} [Group G] {U : Subgroup G} {s : G} [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] (htriv : ∀ (g : G) (m : ZMod 2), g • m = m) (hUo : IsOpen ↑U) (hUi : U.index = 2) (hs : s ∉ U) (α : ↥U → ZMod 2) (hα : ∀ (u v : ↥U), α (u * v) = α u + α v) (hαc : Continuous α) : ContCoh.H2 G (ZMod 2)

The index-two Evens norm N^{Ev}([α]) ∈ H²(G, 𝔽₂), defined as the class of the two-point graph cocycle (98) (= the paper's Lemma 6.13/eq. (99) normalization).

Equations

• GQ2.evensNormH2 htriv hUo hUi hs α hα hαc = (GQ2.ContCoh.H2mk G (ZMod 2)) ⟨GQ2.evensNormFun U s α, ⋯⟩

Kummer cocycles over a subgroup

For a ∈ Lˣ (rather than kˣ), the Kummer cocycle g ↦ [g√a ≠ √a] is a homomorphism on any subgroup N ≤ G_k that fixes a — the input [a] ∈ H¹(G_L, 𝔽₂) of the Evens norm and corestriction in (111).

theorem GQ2.ne_neg_of_ne_zero {K : Type u_1} [Field K] [CharZero K] {β : AlgebraicClosure K} (hβ0 : β ≠ 0) : β ≠ -β

A nonzero element of a characteristic-zero field is not its own negative.

theorem GQ2.two_values_of_fixed {K : Type u_1} [Field K] {A β : AlgebraicClosure K} (hβ : β ^ 2 = A) {g : Kummer.GaloisGroup K} (hg : g • A = A) : g • β = β ∨ g • β = -β

If g fixes β², then g√ = ±√: the two-values lemma with an abstract fixed square (the Kummer-class API's two_values, relativized off the base field).

theorem GQ2.kummerCocycleFun_hom_on {K : Type u_1} [Field K] [CharZero K] {A β : AlgebraicClosure K} {N : Subgroup (Kummer.GaloisGroup K)} (hβ : β ^ 2 = A) (hβ0 : β ≠ 0) (hN : ∀ g ∈ N, g • A = A) (g h : ↥N) : Kummer.kummerCocycleFun β (↑g * ↑h) = Kummer.kummerCocycleFun β ↑g + Kummer.kummerCocycleFun β ↑h

The Kummer cocycle function is a homomorphism on a subgroup fixing β².

noncomputable def GQ2.kummerZ1On {K : Type u_1} [Field K] [CharZero K] {A β : AlgebraicClosure K} (N : Subgroup (Kummer.GaloisGroup K)) (hβ : β ^ 2 = A) (hβ0 : β ≠ 0) (hN : ∀ g ∈ N, g • A = A) : ↥(ContCoh.Z1 (↥N) (ZMod 2))

The Kummer cocycle of a over a subgroup N fixing it, as an element of Z¹(N, 𝔽₂): the input class [a] ∈ H¹(G_L, 𝔽₂) of (111) (with N = G_L, a = β²).

Equations

• GQ2.kummerZ1On N hβ hβ0 hN = ⟨fun (g : ↥N) => GQ2.Kummer.kummerCocycleFun β ↑g, ⋯⟩

Base-general Kummer classes over G_k

The base-general forms of B9 and B11 (finite dyadic base k — the §§6–7 proof layer census amendment, docs/section67-extraction.md §the §§6–7 proof layer amendments) phrase Kummer classes of units of k over the subtype group G_k = ↥(k.fixingSubgroup) inside the one fixed G_ℚ₂ — no second algebraic closure is introduced, so the classes compose directly with the subgroup-relative corestriction and Evens norm above (exactly the shape GQ2.SectionSix.lemma_6_16 consumes).

noncomputable def GQ2.sqrtCl (x : AlgebraicClosure ℚ_[2]) : AlgebraicClosure ℚ_[2]

A canonical square root in the algebraically closed ℚ̄₂.

Equations

• GQ2.sqrtCl x = ⋯.choose

@[simp]

theorem GQ2.sqrtCl_sq (x : AlgebraicClosure ℚ_[2]) : sqrtCl x ^ 2 = x

theorem GQ2.sqrtCl_ne_zero {x : AlgebraicClosure ℚ_[2]} (hx : x ≠ 0) : sqrtCl x ≠ 0

theorem GQ2.fixingSubgroup_smul (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) {g : Kummer.GaloisGroup ℚ_[2]} (hg : g ∈ k.fixingSubgroup) (x : ↥k) : g • ↑x = ↑x

G_k = fixingSubgroup k fixes the elements of k, in •-form.

theorem GQ2.unitCoe_ne_zero (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (a : (↥k)ˣ) : ↑↑a ≠ 0

The ℚ̄₂-coercion of a unit of k is nonzero.

noncomputable def GQ2.kummerClassK (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) (a : (↥k)ˣ) : ContCoh.H1 (↥k.fixingSubgroup) (ZMod 2)

The base-general Kummer class [a] ∈ H¹(G_k, 𝔽₂) of a unit a ∈ kˣ, over the subtype group of k.fixingSubgroup and via the canonical root sqrtCl (class independent of the root, the Kummer-class API's kummerCocycleFun_root_indep). Specializes the Kummer-class API's base-ℚ₂ kummerClass to arbitrary finite dyadic bases; the input shape of the amended B9/B11 axioms.

Equations

• GQ2.kummerClassK k a = (GQ2.ContCoh.H1mk (↥k.fixingSubgroup) (ZMod 2)) ⟨fun (g : ↥k.fixingSubgroup) => GQ2.Kummer.kummerCocycleFun (GQ2.sqrtCl ↑↑a) ↑g, ⋯⟩

noncomputable def GQ2.twoUnit (k : IntermediateField ℚ_[2] (AlgebraicClosure ℚ_[2])) : (↥k)ˣ

2 as a unit of the intermediate field k (char 0).

Equations

• GQ2.twoUnit k = Units.mk0 2 ⋯

Z¹-level packaging (for the axiom statement)

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

• eq. (100) = ⟦eq-halforbit-transfer-description⟧
• eq. (111) = ⟦eq-SWconvention⟧
• eq. (95) = ⟦eq-universal-two-point-cocycle⟧
• eq. (97) = ⟦eq-two-point-shapiro⟧
• eq. (98) = ⟦eq-explicit-evens⟧
• eq. (99) = ⟦eq-evens-normalization⟧
• Lemma 6.13 = ⟦lem-twopointevans⟧
• Lemma 6.16 = ⟦lem-evensvanish⟧
• Thm 1.1 = ⟦prop-markedDem⟧ [cited as theorem; paper says proposition]