The free-orbit Shapiro ledger and transversal changes

The cocycle, coboundary, free-orbit, and arbitrary-transversal comparison layers.

See GQ2.Shapiro.Ledger for the paper-facing overview, source citations, and deviations.

ZMod 2 actions are trivial (Aut(𝔽₂) = 1)

theorem GQ2.ShapiroLedger.zmodTwo_cases (x : ZMod 2) : x = 0 ∨ x = 1

Case split on 𝔽₂.

theorem GQ2.ShapiroLedger.smul_zmodTwo {H : Type u_1} [Group H] [DistribMulAction H (ZMod 2)] (h : H) (m : ZMod 2) : h • m = m

Every DistribMulAction on 𝔽₂ is trivial: ℤ/2 has no nontrivial additive automorphism.

Z¹(N, 𝔽₂) cocycles are homomorphisms

theorem GQ2.ShapiroLedger.z1_mul {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (x y : ↥N) : ↑α (x * y) = ↑α x + ↑α y

A Z¹(N, 𝔽₂)-cocycle is additive (the action is trivial).

theorem GQ2.ShapiroLedger.z1_one {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) : ↑α 1 = 0

α(1) = 0.

theorem GQ2.ShapiroLedger.z1_inv {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) (α : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (x : ↥N) : ↑α x⁻¹ = ↑α x

α(x⁻¹) = α(x) in 𝔽₂.

H2ofFun collapses coboundary differences

theorem GQ2.ShapiroLedger.H2ofFun_eq_of_sub_mem_B2 {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] [ContinuousSMul G (ZMod 2)] {φ ψ : G × G → ZMod 2} (h : φ - ψ ∈ ContCoh.B2 G (ZMod 2)) : H2ofFun G φ = H2ofFun G ψ

If two raw 2-cochains differ by a continuous coboundary, their H2ofFun classes agree. Because H2ofFun is junk-total (0 off Z²), a coboundary difference forces φ ∈ Z² ↔ ψ ∈ Z² and, when both hold, equal classes.

The transversal 1-cochain is a cocycle; the ĝ-shift correction

theorem GQ2.ShapiroLedger.quot_smul_eq_mk_mul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (g : G) (z : G ⧸ N) : g • z = ↑g * z

The G-action on G ⧸ N is left multiplication by the image: g • z = ḡ · z.

theorem GQ2.ShapiroLedger.lWord_mul {G : Type u_1} [Group G] (N : Subgroup G) (h : G ⧸ N) (γ η : G) : Corestriction.lWord N h (γ * η) = Corestriction.lWord N h γ * Corestriction.lWord N (γ⁻¹ • h) η

Transversal 1-cocycle identity: ℓ_h(γη) = ℓ_h(γ) · ℓ_{γ⁻¹•h}(η) (in G).

noncomputable def GQ2.ShapiroLedger.shiftCorr {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (k : G ⧸ N) : G

The .out-representative discrepancy of the ĝ-shift: c(k) = (k̃·ĝ)⁻¹·(k·ḡ)~ ∈ N.

Equations

• GQ2.ShapiroLedger.shiftCorr N ghat k = (Quotient.out k * ghat)⁻¹ * Quotient.out (k * ↑ghat)

theorem GQ2.ShapiroLedger.shiftCorr_mem {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (k : G ⧸ N) : shiftCorr N ghat k ∈ N

shiftCorr lands in N (both factors are lifts of k·ḡ).

theorem GQ2.ShapiroLedger.lWord_shift {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (k : G ⧸ N) (η : G) : Corestriction.lWord N (k * ↑ghat) η = (shiftCorr N ghat k)⁻¹ * (ghat⁻¹ * Corestriction.lWord N k η * ghat) * shiftCorr N ghat (η⁻¹ • k)

The shift factorization of the transversal word: ℓ_{kḡ}(η) = c(k)⁻¹ · (ĝ⁻¹·ℓ_k(η)·ĝ) · c(η⁻¹•k).

Lemma 6.15, free orbits (104)

noncomputable def GQ2.ShapiroLedger.freeCorr {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (β : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (k : G ⧸ N) : ZMod 2

The shift-correction scalar Δ(k) = β(c(k)).

Equations

• GQ2.ShapiroLedger.freeCorr N β ghat k = ↑β ⟨GQ2.ShapiroLedger.shiftCorr N ghat k, ⋯⟩

noncomputable def GQ2.ShapiroLedger.freeLambda {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α β : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) : G → ZMod 2

The coboundary 1-cochain Λ(γ) = Σ_h α(ℓ_h(γ))·Δ(γ⁻¹•h).

Equations

• GQ2.ShapiroLedger.freeLambda N α β ghat γ = ∑ᶠ (h : G ⧸ N), ↑α (GQ2.Corestriction.lTrans N h γ) * GQ2.ShapiroLedger.freeCorr N β ghat (γ⁻¹ • h)

theorem GQ2.ShapiroLedger.continuous_inv_smul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (_hNo : IsOpen ↑N) (h : G ⧸ N) : Continuous fun (γ : G) => γ⁻¹ • h

γ ↦ γ⁻¹ • h : G → G ⧸ N is continuous (into the discrete quotient).

theorem GQ2.ShapiroLedger.continuous_lTrans {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (hNo : IsOpen ↑N) (h : G ⧸ N) : Continuous fun (γ : G) => Corestriction.lTrans N h γ

γ ↦ lTrans N h γ : G → ↥N is continuous.

theorem GQ2.ShapiroLedger.freeLambda_continuous {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] [Finite (G ⧸ N)] (hNo : IsOpen ↑N) (α β : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) : Continuous (freeLambda N α β ghat)

freeLambda is continuous.

theorem GQ2.ShapiroLedger.conjN_mem {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (ghat : G) (k : G ⧸ N) (η : G) : ghat⁻¹ * Corestriction.lWord N k η * ghat ∈ N

The conjugate ĝ⁻¹·ℓ_k(η)·ĝ lands in N (N normal).

theorem GQ2.ShapiroLedger.beta_lTrans_shift {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (β : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) (k : G ⧸ N) (η : G) : ↑β (Corestriction.lTrans N (k * ↑ghat) η) = freeCorr N β ghat k + ↑β ⟨ghat⁻¹ * Corestriction.lWord N k η * ghat, ⋯⟩ + freeCorr N β ghat (η⁻¹ • k)

Per-term shift: β(ℓ_{kḡ}(η)) = Δ(k) + β(ĝ⁻¹ℓ_k(η)ĝ) + Δ(η⁻¹•k), absorbing the .out discrepancy into the two corrections (β a hom).

theorem GQ2.ShapiroLedger.phi_free_eq {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α β : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat γ η : G) : graphPullback (freeOrbitDatum N ((QuotientGroup.mk' N) ghat)) (⇑(QuotientGroup.mk' N)) (fun (δ : G) => (Corestriction.shapiroFun N (↑α) δ, Corestriction.shapiroFun N (↑β) δ)) (γ, η) = ∑ᶠ (h : G ⧸ N), ↑α (Corestriction.lTrans N h γ) * ↑β (Corestriction.lTrans N (((QuotientGroup.mk' N) γ)⁻¹ * (h * (QuotientGroup.mk' N) ghat)) η)

The free graph pullback, unfolded to an explicit sum over G ⧸ N.

theorem GQ2.ShapiroLedger.psi_free_eq {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod 2)] (N : Subgroup G) [N.Normal] (α β : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat γ η : G) : Corestriction.cor2Fun N (fun (p : ↥N × ↥N) => ↑α p.1 * ↑β ⟨ghat⁻¹ * ↑p.2 * ghat, ⋯⟩) (γ, η) = ∑ᶠ (u : G ⧸ N), ↑α (Corestriction.lTrans N u γ) * ↑β ⟨ghat⁻¹ * Corestriction.lWord N (γ⁻¹ • u) η * ghat, ⋯⟩

The corestriction side, unfolded to an explicit sum over G ⧸ N (definitional).

theorem GQ2.ShapiroLedger.sum_reindex_smul {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] [Fintype (G ⧸ N)] (γ : G) (F : G ⧸ N → ZMod 2) : ∑ h : G ⧸ N, F (γ • h) = ∑ h : G ⧸ N, F h

Reindexing over G ⧸ N by left translation.

theorem GQ2.ShapiroLedger.lemma_6_15_free_aux {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] [ContinuousSMul G (ZMod 2)] (N : Subgroup G) [N.Normal] [Finite (G ⧸ N)] (hNo : IsOpen ↑N) (α β : ↥(ContCoh.Z1 (↥N) (ZMod 2))) (ghat : G) : H2ofFun G (graphPullback (freeOrbitDatum N ((QuotientGroup.mk' N) ghat)) ⇑(QuotientGroup.mk' N) fun (γ : G) => (Corestriction.shapiroFun N (↑α) γ, Corestriction.shapiroFun N (↑β) γ)) = H2ofFun G (Corestriction.cor2Fun N fun (p : ↥N × ↥N) => ↑α p.1 * ↑β ⟨ghat⁻¹ * ↑p.2 * ghat, ⋯⟩)

Lemma 6.15, free orbits (104): proved via the coboundary δ¹Λ with the explicit Λ = freeLambda. (the §§6–7 statement; the Shapiro-ledger proof, Ax = ∅.)

Abstract cocycle twist (any group, char 2)

noncomputable def GQ2.ShapiroLedger.twistCorr {A : Type u_1} [Group A] (ν : A × A → ZMod 2) (a c d : A) : ZMod 2

Per-slot transversal correction: M(a; c, d) = ν(c⁻¹, a·d) + ν(a, d) + ν(d, d⁻¹).

Equations

• GQ2.ShapiroLedger.twistCorr ν a c d = ν (c⁻¹, a * d) + ν (a, d) + ν (d, d⁻¹)

theorem GQ2.ShapiroLedger.cocycle_twist {A : Type u_1} [Group A] (ν : A × A → ZMod 2) (hcoc : ∀ (a b c : A), ν (b, c) + ν (a * b, c) + ν (a, b * c) + ν (a, b) = 0) (hr1 : ∀ (z : A), ν (z, 1) = 0) (x y c₀ c₁ c₂ : A) : ν (c₀⁻¹ * x * c₁, c₁⁻¹ * y * c₂) = ν (x, y) + twistCorr ν x c₀ c₁ + twistCorr ν y c₁ c₂ + twistCorr ν (x * y) c₀ c₂

Cocycle twist: conjugating a composable pair (x, y) by corrections c₀, c₁, c₂ changes a right-normalized char-2 2-cocycle by three twistCorr reads.

Corestriction along an arbitrary transversal

noncomputable def GQ2.ShapiroLedger.lWordT {G : Type u_1} [Group G] (U : Subgroup G) (T : G ⧸ U → G) (v : G ⧸ U) (γ : G) : G

ℓ-word along an arbitrary transversal lift T : G ⧸ U → G.

Equations

• GQ2.ShapiroLedger.lWordT U T v γ = (T v)⁻¹ * γ * T (γ⁻¹ • v)

noncomputable def GQ2.ShapiroLedger.lTransT {G : Type u_1} [Group G] (U : Subgroup G) (T : G ⧸ U → G) (hT : ∀ (v : G ⧸ U), ↑(T v) = v) (v : G ⧸ U) (γ : G) : ↥U

The transversal 1-cochain along T, valued in ↥U.

Equations

• GQ2.ShapiroLedger.lTransT U T hT v γ = ⟨GQ2.ShapiroLedger.lWordT U T v γ, ⋯⟩

theorem GQ2.ShapiroLedger.lWordT_mul {G : Type u_1} [Group G] (U : Subgroup G) (T : G ⧸ U → G) (v : G ⧸ U) (γ η : G) : lWordT U T v (γ * η) = lWordT U T v γ * lWordT U T (γ⁻¹ • v) η

The ℓ^T-cocycle identity (transversal-independent telescoping).

theorem GQ2.ShapiroLedger.lWordT_out {G : Type u_1} [Group G] (U : Subgroup G) (v : G ⧸ U) (γ : G) : lWordT U (fun (w : G ⧸ U) => Quotient.out w) v γ = Corestriction.lWord U v γ

The canonical transversal is the T = Quotient.out special case.

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

ℓ-cocycle identity for the canonical transversal (normality-free).

noncomputable def GQ2.ShapiroLedger.tCorr {G : Type u_1} [Group G] (U : Subgroup G) (T : G ⧸ U → G) (v : G ⧸ U) : G

The .out-vs-T transversal correction at v: T v = v.out · tCorr v.

Equations

• GQ2.ShapiroLedger.tCorr U T v = (Quotient.out v)⁻¹ * T v

noncomputable def GQ2.ShapiroLedger.tCorrEl {G : Type u_1} [Group G] (U : Subgroup G) (T : G ⧸ U → G) (hT : ∀ (v : G ⧸ U), ↑(T v) = v) (v : G ⧸ U) : ↥U

tCorr as an element of ↥U.

Equations

• GQ2.ShapiroLedger.tCorrEl U T hT v = ⟨GQ2.ShapiroLedger.tCorr U T v, ⋯⟩

theorem GQ2.ShapiroLedger.lTransT_factor {G : Type u_1} [Group G] (U : Subgroup G) (T : G ⧸ U → G) (hT : ∀ (v : G ⧸ U), ↑(T v) = v) (v : G ⧸ U) (γ : G) : lTransT U T hT v γ = (tCorrEl U T hT v)⁻¹ * Corestriction.lTrans U v γ * tCorrEl U T hT (γ⁻¹ • v)

Factorization: the T-word sandwiches the canonical word between corrections.

noncomputable def GQ2.ShapiroLedger.cor2FunT {G : Type u_1} [Group G] (U : Subgroup G) (T : G ⧸ U → G) (hT : ∀ (v : G ⧸ U), ↑(T v) = v) (ν : ↥U × ↥U → ZMod 2) : G × G → ZMod 2

Corestriction of ν : U × U → 𝔽₂ along the transversal T.

Equations

• GQ2.ShapiroLedger.cor2FunT U T hT ν p = ∑ᶠ (v : G ⧸ U), ν (GQ2.ShapiroLedger.lTransT U T hT v p.1, GQ2.ShapiroLedger.lTransT U T hT (p.1⁻¹ • v) p.2)

noncomputable def GQ2.ShapiroLedger.twistLambda {G : Type u_1} [Group G] (U : Subgroup G) (T : G ⧸ U → G) (hT : ∀ (v : G ⧸ U), ↑(T v) = v) (ν : ↥U × ↥U → ZMod 2) : G → ZMod 2

The transversal-change 1-cochain Λ.

Equations

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

theorem GQ2.ShapiroLedger.sum_reindex_smul' {G : Type u_1} [Group G] (U : Subgroup G) [Fintype (G ⧸ U)] (γ : G) (F : G ⧸ U → ZMod 2) : ∑ v : G ⧸ U, F (γ⁻¹ • v) = ∑ v : G ⧸ U, F v

Reindex a G ⧸ U-sum along v ↦ γ⁻¹ • v (normality-free).

theorem GQ2.ShapiroLedger.locallyConstant_inv_smul {G : Type u_1} [Group G] (U : Subgroup G) [TopologicalSpace G] [IsTopologicalGroup G] (hUo : IsOpen ↑U) (v : G ⧸ U) : IsLocallyConstant fun (γ : G) => γ⁻¹ • v

γ ↦ γ⁻¹ • v : G → G ⧸ U is locally constant when U is open (fibers are open).

theorem GQ2.ShapiroLedger.continuous_comp_inv_smul {G : Type u_1} [Group G] (U : Subgroup G) [TopologicalSpace G] [IsTopologicalGroup G] {X : Type u_2} [TopologicalSpace X] (hUo : IsOpen ↑U) (v : G ⧸ U) (f : G ⧸ U → X) : Continuous fun (γ : G) => f (γ⁻¹ • v)

Any function of γ⁻¹ • v is continuous (U open).

theorem GQ2.ShapiroLedger.continuous_lTrans' {G : Type u_1} [Group G] (U : Subgroup G) [TopologicalSpace G] [IsTopologicalGroup G] (hUo : IsOpen ↑U) (v : G ⧸ U) : Continuous fun (γ : G) => Corestriction.lTrans U v γ

γ ↦ ℓ_v(γ) : G → ↥U is continuous (normality-free).

theorem GQ2.ShapiroLedger.twistLambda_continuous {G : Type u_1} [Group G] (U : Subgroup G) [TopologicalSpace G] [IsTopologicalGroup G] [Finite (G ⧸ U)] (hUo : IsOpen ↑U) (T : G ⧸ U → G) (hT : ∀ (v : G ⧸ U), ↑(T v) = v) (ν : ↥U × ↥U → ZMod 2) (hνc : Continuous ν) : Continuous (twistLambda U T hT ν)

twistLambda is continuous.

theorem GQ2.ShapiroLedger.cor2FunT_sub_cor2Fun_mem_B2 {G : Type u_1} [Group G] (U : Subgroup G) [TopologicalSpace G] [IsTopologicalGroup G] [DistribMulAction G (ZMod 2)] [Finite (G ⧸ U)] (hUo : IsOpen ↑U) (T : G ⧸ U → G) (hT : ∀ (v : G ⧸ U), ↑(T v) = v) (ν : ↥U × ↥U → ZMod 2) (hνc : Continuous ν) (hcoc : ∀ (a b c : ↥U), ν (b, c) + ν (a * b, c) + ν (a, b * c) + ν (a, b) = 0) (hr1 : ∀ (z : ↥U), ν (z, 1) = 0) : cor2FunT U T hT ν - Corestriction.cor2Fun U ν ∈ ContCoh.B2 G (ZMod 2)

Transversal change for corestriction: the T-corestriction of a right-normalized 2-cocycle ν on the open finite-index U differs from the canonical one by a coboundary.