The Γ_A degree-2 presentation comparison — foundation

Building on the degree-≤1 bridge GQ2/WordCohBridge.lean (z1Equiv/h1Equiv), this file develops the degree-2 half: an injection H²(Γ_A, 𝔽₂) ↪ 𝔽₂² ⧸ im d1_triv = H2w(t_triv) (evaluation of the two relator words on a central extension), whose target has cardinality 2 (card_H2w_trivial), giving #H²(Γ_A, 𝔽₂) ≤ 2 — the source-side cohomological input lemma_8_6_gammaA (the Γ_A half-torsor proof) needs.

This file, so far — the central-extension foundation. A ZMod 2-valued 2-cocycle κ on a group L (normalized at (1,1)) is packaged as TwoCocycle L, and CentExt c is the central extension L ×_κ ZMod 2: carrier L × ZMod 2, product (l,z)·(l',z') = (l·l', z + z' + κ l l'). The kernel {(1, z)} ≅ ZMod 2 is central; the base projection is CentExt c →* L. When L is finite discrete so is CentExt c — the codomain for a Marking whose relator values read off the cocycle's obstruction.

The remaining θ construction (factor a continuous cocycle through a finite admissible level, mark the extension by (ḡᵢ, 0), read the tame/wild relator z-values, quotient by im d1_triv, prove additivity, vanishing on coboundaries, and injectivity via Marking.descend) is the next work; see the tail comment.

structure GQ2.WordCoh2.TwoCocycle (L : Type u_2) [Group L] : Type u_2

A ZMod 2-valued 2-cocycle on L, normalized at (1,1) — the datum of a central extension of L by ZMod 2 (trivial action). The single cocycle identity κ(a,b) + κ(ab,c) = κ(a,bc) + κ(b,c) forces κ(1,·) = κ(·,1) = κ(1,1); the norm field pins that constant to 0.

• κ : L → L → ZMod 2

  The underlying 2-cochain.

• norm : self.κ 1 1 = 0

  Normalization at the identity.

• cocyc (a b c : L) : self.κ a b + self.κ (a * b) c = self.κ a (b * c) + self.κ b c

  The 2-cocycle identity (trivial coefficients).

theorem GQ2.WordCoh2.TwoCocycle.κ_one_left {L : Type u_1} [Group L] (c : TwoCocycle L) (l : L) : c.κ 1 l = 0

κ vanishes on the left axis (κ(1,l) = 0).

theorem GQ2.WordCoh2.TwoCocycle.κ_one_right {L : Type u_1} [Group L] (c : TwoCocycle L) (l : L) : c.κ l 1 = 0

κ vanishes on the right axis (κ(l,1) = 0).

theorem GQ2.WordCoh2.TwoCocycle.κ_inv {L : Type u_1} [Group L] (c : TwoCocycle L) (l : L) : c.κ l l⁻¹ = c.κ l⁻¹ l

Symmetry of κ on inverse pairs (κ(l,l⁻¹) = κ(l⁻¹,l)) — the fact underlying the inverse law of the central extension.

def GQ2.WordCoh2.CentExt {L : Type u_1} [Group L] (_c : TwoCocycle L) : Type u_1

The central extension L ×_κ ZMod 2 of L by ZMod 2 attached to a 2-cocycle κ: carrier L × ZMod 2, product (l,z)·(l',z') = (l·l', z + z' + κ l l').

Equations

• GQ2.WordCoh2.CentExt _c = (L × ZMod 2)

def GQ2.WordCoh2.CentExt.base {L : Type u_1} [Group L] {c : TwoCocycle L} (p : CentExt c) : L

Base coordinate of an element of the extension.

Equations

• p.base = p.1

def GQ2.WordCoh2.CentExt.fib {L : Type u_1} [Group L] {c : TwoCocycle L} (p : CentExt c) : ZMod 2

Fibre (ZMod 2) coordinate of an element of the extension.

Equations

• p.fib = p.2

theorem GQ2.WordCoh2.CentExt.ext {L : Type u_1} [Group L] {c : TwoCocycle L} {p q : CentExt c} (h1 : p.base = q.base) (h2 : p.fib = q.fib) : p = q

theorem GQ2.WordCoh2.CentExt.ext_iff {L : Type u_1} [Group L] {c : TwoCocycle L} {p q : CentExt c} : p = q ↔ p.base = q.base ∧ p.fib = q.fib

@[implicit_reducible]

instance GQ2.WordCoh2.CentExt.instGroup {L : Type u_1} [Group L] {c : TwoCocycle L} : Group (CentExt c)

Equations

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

@[simp]

theorem GQ2.WordCoh2.CentExt.mul_base {L : Type u_1} [Group L] {c : TwoCocycle L} (p q : CentExt c) : (p * q).base = p.base * q.base

@[simp]

theorem GQ2.WordCoh2.CentExt.mul_fib {L : Type u_1} [Group L] {c : TwoCocycle L} (p q : CentExt c) : (p * q).fib = p.fib + q.fib + c.κ p.base q.base

def GQ2.WordCoh2.CentExt.proj {L : Type u_1} [Group L] (c : TwoCocycle L) : CentExt c →* L

The base projection L ×_κ ZMod 2 →* L, a group homomorphism.

Equations

• GQ2.WordCoh2.CentExt.proj c = { toFun := GQ2.WordCoh2.CentExt.base, map_one' := ⋯, map_mul' := ⋯ }

def GQ2.WordCoh2.CentExt.incl {L : Type u_1} [Group L] (c : TwoCocycle L) : ZMod 2 → CentExt c

The central inclusion ZMod 2 → L ×_κ ZMod 2, z ↦ (1, z).

Equations

• GQ2.WordCoh2.CentExt.incl c z = (1, z)

theorem GQ2.WordCoh2.CentExt.base_eq_one_iff {L : Type u_1} [Group L] {c : TwoCocycle L} (p : CentExt c) : p.base = 1 ↔ p = incl c p.fib

An element of the extension lies over the base identity iff it is in the central ZMod 2.

@[simp]

theorem GQ2.WordCoh2.CentExt.incl_zero {L : Type u_1} [Group L] {c : TwoCocycle L} : incl c 0 = 1

incl 0 is the identity of the extension.

@[simp]

theorem GQ2.WordCoh2.CentExt.incl_mul_fib {L : Type u_1} [Group L] {c : TwoCocycle L} (z : ZMod 2) (p : CentExt c) : (incl c z * p).fib = z + p.fib

The fibre of incl z · p is z + p.fib (the base being p.base).

@[implicit_reducible]

instance GQ2.WordCoh2.CentExt.instTopologicalSpace {L : Type u_1} [Group L] {c : TwoCocycle L} : TopologicalSpace (CentExt c)

Equations

• GQ2.WordCoh2.CentExt.instTopologicalSpace = ⊥

instance GQ2.WordCoh2.CentExt.instDiscreteTopology {L : Type u_1} [Group L] {c : TwoCocycle L} : DiscreteTopology (CentExt c)

instance GQ2.WordCoh2.CentExt.instFinite {L : Type u_1} [Group L] {c : TwoCocycle L} [Finite L] : Finite (CentExt c)

Lifting a level marking and reading the relator obstruction

def GQ2.WordCoh2.liftMark {L : Type u_1} [Group L] (t : Marking L) (c : TwoCocycle L) : Marking (CentExt c)

Lift a marking of the base group L to the central extension by placing each generator over it with zero fibre coordinate. Its base projection is the original marking.

Equations

• GQ2.WordCoh2.liftMark t c = { σ := (t.σ, 0), τ := (t.τ, 0), x₀ := (t.x₀, 0), x₁ := (t.x₁, 0) }

@[simp]

theorem GQ2.WordCoh2.liftMark_map_proj {L : Type u_1} [Group L] (t : Marking L) (c : TwoCocycle L) : Marking.map (CentExt.proj c) (liftMark t c) = t

theorem GQ2.WordCoh2.liftMark_tameValue_base {L : Type u_1} [Group L] (t : Marking L) (c : TwoCocycle L) : (liftMark t c).tameValue.base = t.tameValue

The tame relator value of the lifted marking projects to that of the base marking.

theorem GQ2.WordCoh2.liftMark_wildValue_base {L : Type u_1} [Group L] [Finite L] (t : Marking L) (c : TwoCocycle L) : (liftMark t c).wildValue.base = t.wildValue

The wild relator value of the lifted marking projects to that of the base marking (needs L finite: Marking.map_wildValue's ω₂-naturality is finite-only, and CentExt c is finite).

noncomputable def GQ2.WordCoh2.relZPair {L : Type u_1} [Group L] [Finite L] (t : Marking L) (c : TwoCocycle L) : ZMod 2 × ZMod 2

The relator-z pair of c relative to a base marking t: the fibre coordinates of the tame and wild relator values of the lifted marking — the degree-2 obstruction of c, pre-quotient by im d1_triv.

Equations

• GQ2.WordCoh2.relZPair t c = ((GQ2.WordCoh2.liftMark t c).tameValue.fib, (GQ2.WordCoh2.liftMark t c).wildValue.fib)

theorem GQ2.WordCoh2.liftMark_tameValue_eq_incl {L : Type u_1} [Group L] (t : Marking L) (ht : t.TameRel) (c : TwoCocycle L) : (liftMark t c).tameValue = CentExt.incl c (liftMark t c).tameValue.fib

When the base marking satisfies the tame relation, the lifted tame relator value is exactly the central element (1, tameZ) — the relator "dies into the fibre".

theorem GQ2.WordCoh2.liftMark_wildValue_eq_incl {L : Type u_1} [Group L] [Finite L] (t : Marking L) (hw : t.WildRel) (c : TwoCocycle L) : (liftMark t c).wildValue = CentExt.incl c (liftMark t c).wildValue.fib

When the base marking satisfies the wild relation, the lifted wild relator value is exactly the central element (1, wildZ).

The shifted lift and its wild Pro2Core

For the injectivity of θ we adjust the fibre coordinates of the lifted marking by a : Fin 4 → 𝔽₂ (so the relators can be made to die exactly), then run the NA_le_ker machinery of c1. The Pro2Core clause of admissibility is the hard sub-step; it holds by the same argument as c1 (isPGroup_liftMarking_wildCore): the wild core lands in proj⁻¹(base wild core), a 2-group as an extension of the base wild core by the central 𝔽₂.

def GQ2.WordCoh2.shiftLiftMark {L : Type u_1} [Group L] (t : Marking L) (a : Fin 4 → ZMod 2) (c : TwoCocycle L) : Marking (CentExt c)

The lifted marking with the four fibre coordinates shifted by a.

Equations

• GQ2.WordCoh2.shiftLiftMark t a c = { σ := (t.σ, a 0), τ := (t.τ, a 1), x₀ := (t.x₀, a 2), x₁ := (t.x₁, a 3) }

theorem GQ2.WordCoh2.isPGroup_proj_ker {L : Type u_1} [Group L] (c : TwoCocycle L) : IsPGroup 2 ↥(CentExt.proj c).ker

The base projection's kernel {(1, z)} ≅ 𝔽₂ is elementary-2.

theorem GQ2.WordCoh2.isPGroup_shiftLift_wildCore {L : Type u_1} [Group L] (t : Marking L) (a : Fin 4 → ZMod 2) (c : TwoCocycle L) (ht2 : IsPGroup 2 ↥(Subgroup.normalClosure {t.x₀, t.x₁})) : IsPGroup 2 ↥(Subgroup.normalClosure {(shiftLiftMark t a c).x₀, (shiftLiftMark t a c).x₁})

The Pro2Core crux for the extension. If the base marking's wild core is a 2-group, so is the shifted lift's — an extension of it by the central 𝔽₂ (IsPGroup.comap_of_injective route, exactly as c1's isPGroup_liftMarking_wildCore).

theorem GQ2.WordCoh2.shiftLiftMark_tameValue_base {L : Type u_1} [Group L] (t : Marking L) (a : Fin 4 → ZMod 2) (c : TwoCocycle L) : (shiftLiftMark t a c).tameValue.base = t.tameValue

The shifted lift's tame relator value projects to the base's.

theorem GQ2.WordCoh2.shiftLiftMark_wildValue_base {L : Type u_1} [Group L] [Finite L] (t : Marking L) (a : Fin 4 → ZMod 2) (c : TwoCocycle L) : (shiftLiftMark t a c).wildValue.base = t.wildValue

The shifted lift's wild relator value projects to the base's (needs L finite).

theorem GQ2.WordCoh2.shiftLiftMark_tameValue_eq_one {L : Type u_1} [Group L] (t : Marking L) (ht : t.TameRel) (a : Fin 4 → ZMod 2) (c : TwoCocycle L) (hz : (shiftLiftMark t a c).tameValue.fib = 0) : (shiftLiftMark t a c).tameValue = 1

Tame relator dies exactly. When the base marking satisfies the tame relation and the shifted tame z-value is 0, the shifted lift's tame relator value is the identity of the extension.

theorem GQ2.WordCoh2.shiftLiftMark_wildValue_eq_one {L : Type u_1} [Group L] [Finite L] (t : Marking L) (hw : t.WildRel) (a : Fin 4 → ZMod 2) (c : TwoCocycle L) (hz : (shiftLiftMark t a c).wildValue.fib = 0) : (shiftLiftMark t a c).wildValue = 1

Wild relator dies exactly. When the base marking satisfies the wild relation and the shifted wild z-value is 0, the shifted lift's wild relator value is the identity of the extension.

The splitting section: N_A ≤ ker (classify (shifted lift))

The injectivity crux, an exact mirror of c1's WordCohBridge.NA_le_ker_classify: over a finite admissible level L = F₄ ⧸ U (N_A ≤ U), if the shifted lift's relators die exactly, the classified F₄ → CentExt c hom kills N_A — ker is an admissible open (Generates automatic, relators die, Pro2Core from isPGroup_shiftLift_wildCore transferred along kerLift).

theorem GQ2.WordCoh2.NA_le_ker_shiftLift (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NA ≤ ↑U.toOpenSubgroup) (c : TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (a : Fin 4 → ZMod 2) (htame0 : (shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).tameValue.fib = 0) (hwild0 : (shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).wildValue.fib = 0) : NA ≤ (shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).classify.ker

N_A ≤ ker for the shifted lift. ([Finite (F₄ ⧸ U)] is needed at statement level for CentExt c to be finite — it is not a global instance; callers supply it via Subgroup.quotient_finite_of_isOpen _ U.isOpen'.)

noncomputable def GQ2.WordCoh2.sectionHom (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NA ≤ ↑U.toOpenSubgroup) (c : TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (a : Fin 4 → ZMod 2) (htame0 : (shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).tameValue.fib = 0) (hwild0 : (shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).wildValue.fib = 0) : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA →ₜ* CentExt c

The splitting section Γ_A → CentExt c produced by NA_le_ker_shiftLift: the descended classify of the (relator-killing) shifted lift.

Equations

• GQ2.WordCoh2.sectionHom U hU c a htame0 hwild0 = GQ2.quotientLift GQ2.NA (GQ2.WordCoh2.shiftLiftMark (GQ2.Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) GQ2.univMarking) a c).classify ⋯

theorem GQ2.WordCoh2.projC_comp_sectionHom (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NA ≤ ↑U.toOpenSubgroup) (c : TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (a : Fin 4 → ZMod 2) (htame0 : (shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).tameValue.fib = 0) (hwild0 : (shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).wildValue.fib = 0) (g : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) : ((sectionHom U hU c a htame0 hwild0) ((quotientMk NA) g)).base = (QuotientGroup.mk' ↑U.toOpenSubgroup) g

The section splits the base projection: proj ∘ s is the level projection Γ_A ↠ F₄ ⧸ U (pointwise, proj (s (mk_{N_A} g)) = mk_U g). Proof by Marking.toHom_hom_univMarking_map uniqueness: both projC ∘ classify(shifted lift) and quotientMk U push univMarking to t_L.

Coboundary extraction — the θ-injectivity payoff

Once the shifted lift's relators die, the level cocycle pulled back to Γ_A (as the base-coordinate pairing of the section) is dOne of the continuous 1-cochain λ = fib ∘ s, hence a continuous 2-coboundary. This is the concrete "extension splits ⇒ cocycle is a coboundary" step.

theorem GQ2.WordCoh2.cocycle_mem_B2 [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] [TopologicalSpace (ZMod 2)] [DiscreteTopology (ZMod 2)] (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NA ≤ ↑U.toOpenSubgroup) (c : TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (a : Fin 4 → ZMod 2) (htame0 : (shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).tameValue.fib = 0) (hwild0 : (shiftLiftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) a c).wildValue.fib = 0) (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) : (fun (p : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) => c.κ ((sectionHom U hU c a htame0 hwild0) p.1).base ((sectionHom U hU c a htame0 hwild0) p.2).base) ∈ ContCoh.B2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)

Coboundary extraction. With 𝔽₂ a trivial Γ_A-module, the 2-cocycle (x,y) ↦ c.κ ((s x).base) ((s y).base) — the level cocycle pulled back through the splitting section s — is a continuous 2-coboundary dOne (fib ∘ s). (dOne λ (x,y) = λ(y) − λ(xy) + λ(x) at trivial action; the section's fibre law λ(xy) = λ(x) + λ(y) + c.κ((s x).base,(s y).base) makes this equal to the pairing, an 8-case 𝔽₂ identity.)

The shift laws — how a generator shift moves the fibre obstruction

shiftLiftMark t a c is liftMark t c with generator i left-multiplied by the central incl (a i). Evaluating the tame/wild relator words, each fibre obstruction shifts by exactly a 1 (the τ-coordinate): the tame and wild relators both have odd τ-content and even content in σ, x₀, x₁ (mod 2) — the same content computation as the trivial-module differential d¹ = (a₁, a₁) of FoxH.d1Fun_of_trivial. We transport that computation through the comparison hom WordLift (ZMod 2) (CentExt c) →* CentExt c, ⟨z, g⟩ ↦ incl z · g, which realizes shiftLiftMark t a c as (liftMarking (liftMark t c) a).map _. (Note both fibres move by the same a 1, so the shift always stays in the diagonal Δ = im d¹_triv — exactly what makes θ land in 𝔽₂²/Δ and its kernel adjustable by a shift.)

@[implicit_reducible]

def GQ2.WordCoh2.trivAction {L : Type u_2} [Group L] {c : TwoCocycle L} : DistribMulAction (CentExt c) (ZMod 2)

The extension acts trivially on the coefficient ZMod 2.

Equations

• GQ2.WordCoh2.trivAction = { smul := fun (x : GQ2.WordCoh2.CentExt c) (z : ZMod 2) => z, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

def GQ2.WordCoh2.shiftCompare {L : Type u_2} [Group L] {c : TwoCocycle L} : FoxH.WordLift (ZMod 2) (CentExt c) →* CentExt c

The comparison hom ⟨z, g⟩ ↦ incl z · g, WordLift (ZMod 2) (CentExt c) →* CentExt c.

Equations

• GQ2.WordCoh2.shiftCompare = { toFun := fun (p : GQ2.FoxH.WordLift (ZMod 2) (GQ2.WordCoh2.CentExt c)) => GQ2.WordCoh2.CentExt.incl c p.u * p.g, map_one' := ⋯, map_mul' := ⋯ }

def GQ2.WordCoh2.wlBase {L : Type u_2} [Group L] {c : TwoCocycle L} : FoxH.WordLift (ZMod 2) (CentExt c) →* CentExt c

The base projection ⟨z, g⟩ ↦ g, WordLift (ZMod 2) (CentExt c) →* CentExt c.

Equations

• GQ2.WordCoh2.wlBase = { toFun := GQ2.FoxH.WordLift.g, map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.WordCoh2.shiftCompare_liftGen {L : Type u_2} [Group L] {c : TwoCocycle L} (g : L) (z : ZMod 2) : shiftCompare { u := z, g := (g, 0) } = (g, z)

shiftCompare ⟨z, (g, 0)⟩ = (g, z) — the central shift applied to a zero-fibre lift.

@[simp]

theorem GQ2.WordCoh2.map_wlBase_liftMarking {L : Type u_2} [Group L] {c : TwoCocycle L} (t : Marking L) (a : Fin 4 → ZMod 2) : Marking.map wlBase (FoxH.liftMarking (liftMark t c) a) = liftMark t c

liftMarking (liftMark t c) a projects (via wlBase) back to liftMark t c.

theorem GQ2.WordCoh2.map_shiftCompare_liftMarking {L : Type u_2} [Group L] {c : TwoCocycle L} (t : Marking L) (a : Fin 4 → ZMod 2) : Marking.map shiftCompare (FoxH.liftMarking (liftMark t c) a) = shiftLiftMark t a c

liftMarking (liftMark t c) a maps (via shiftCompare) to shiftLiftMark t a c.

theorem GQ2.WordCoh2.liftMarking_tameValue_g {L : Type u_2} [Group L] {c : TwoCocycle L} (t : Marking L) (a : Fin 4 → ZMod 2) : (FoxH.liftMarking (liftMark t c) a).tameValue.g = (liftMark t c).tameValue

The tame relator value's base coordinate of the lift recovers that of liftMark t c.

theorem GQ2.WordCoh2.liftMarking_wildValue_g {L : Type u_2} [Group L] {c : TwoCocycle L} [Finite L] (t : Marking L) (a : Fin 4 → ZMod 2) : (FoxH.liftMarking (liftMark t c) a).wildValue.g = (liftMark t c).wildValue

The wild relator value's base coordinate of the lift recovers that of liftMark t c.

theorem GQ2.WordCoh2.liftMarking_tameValue_u_eq {L : Type u_2} [Group L] {c : TwoCocycle L} (t : Marking L) (a : Fin 4 → ZMod 2) : (FoxH.liftMarking (liftMark t c) a).tameValue.u = a 1

The tame fibre shift of the lift is a 1 (trivial action, char 2 — relation-free).

theorem GQ2.WordCoh2.liftMarking_wildValue_u_eq {L : Type u_2} [Group L] {c : TwoCocycle L} [Finite L] (t : Marking L) (a : Fin 4 → ZMod 2) : (FoxH.liftMarking (liftMark t c) a).wildValue.u = a 1

The wild fibre shift of the lift is a 1 (liftMarking_wildValue_u at trivial action, char 2).

theorem GQ2.WordCoh2.shiftLiftMark_tameValue_fib {L : Type u_2} [Group L] {c : TwoCocycle L} (t : Marking L) (a : Fin 4 → ZMod 2) : (shiftLiftMark t a c).tameValue.fib = (liftMark t c).tameValue.fib + a 1

Tame shift law: shifting the lift by a changes the tame fibre obstruction by a 1.

theorem GQ2.WordCoh2.shiftLiftMark_wildValue_fib {L : Type u_2} [Group L] {c : TwoCocycle L} [Finite L] (t : Marking L) (a : Fin 4 → ZMod 2) : (shiftLiftMark t a c).wildValue.fib = (liftMark t c).wildValue.fib + a 1

Wild shift law: shifting the lift by a changes the wild fibre obstruction by a 1.

theorem GQ2.WordCoh2.exists_shift_of_relZ_eq {L : Type u_2} [Group L] {c : TwoCocycle L} [Finite L] (t : Marking L) (hrel : (liftMark t c).tameValue.fib = (liftMark t c).wildValue.fib) : ∃ (a : Fin 4 → ZMod 2), (shiftLiftMark t a c).tameValue.fib = 0 ∧ (shiftLiftMark t a c).wildValue.fib = 0

The d¹-adjustment. When the tame and wild fibre obstructions of liftMark t c agree (i.e. relZPair ∈ Δ = im d¹_triv), the constant shift a ≡ (liftMark t c).tameValue.fib makes both shifted relator fibres vanish — the hypothesis feeding NA_le_ker_shiftLift.

Level change: pulling a cocycle back along a group hom

For the well-definedness of θ across refinements, we record that the relator obstruction relZPair is natural: pulling a cocycle c back along φ : L' →* L and pushing the base marking forward by φ give the same obstruction. The comparison hom is projExt : CentExt (c.comap φ) →* CentExt c, (l, z) ↦ (φ l, z).

def GQ2.WordCoh2.TwoCocycle.comap {L : Type u_2} {L' : Type u_3} [Group L] [Group L'] (c : TwoCocycle L) (φ : L' →* L) : TwoCocycle L'

Pull back a 2-cocycle along a group hom φ : L' →* L.

Equations

• c.comap φ = { κ := fun (a b : L') => c.κ (φ a) (φ b), norm := ⋯, cocyc := ⋯ }

@[simp]

theorem GQ2.WordCoh2.TwoCocycle.comap_κ {L : Type u_2} {L' : Type u_3} [Group L] [Group L'] (c : TwoCocycle L) (φ : L' →* L) (a b : L') : (c.comap φ).κ a b = c.κ (φ a) (φ b)

def GQ2.WordCoh2.projExt {L : Type u_2} {L' : Type u_3} [Group L] [Group L'] (c : TwoCocycle L) (φ : L' →* L) : CentExt (c.comap φ) →* CentExt c

The base hom φ lifts to a hom of central extensions CentExt (c.comap φ) →* CentExt c.

Equations

• GQ2.WordCoh2.projExt c φ = { toFun := fun (p : GQ2.WordCoh2.CentExt (c.comap φ)) => (φ p.base, p.fib), map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.WordCoh2.map_projExt_liftMark {L : Type u_2} {L' : Type u_3} [Group L] [Group L'] (t' : Marking L') (c : TwoCocycle L) (φ : L' →* L) : Marking.map (projExt c φ) (liftMark t' (c.comap φ)) = liftMark (Marking.map φ t') c

liftMark t' (c.comap φ) maps to liftMark (t'.map φ) c under projExt.

theorem GQ2.WordCoh2.relZPair_comap {L : Type u_2} {L' : Type u_3} [Group L] [Group L'] [Finite L] [Finite L'] (t' : Marking L') (c : TwoCocycle L) (φ : L' →* L) : relZPair (Marking.map φ t') c = relZPair t' (c.comap φ)

Level-independence of the relator obstruction. Pulling c back along φ and pushing the base marking forward by φ give the same relZPair.

Additivity of the relator obstruction (the Baer sum)

relZPair t (c₁ + c₂) = relZPair t c₁ + relZPair t c₂. The comparison object is the fiber product FiberProd c₁ c₂ = L ×_κ 𝔽₂², the central extension of L by 𝔽₂ × 𝔽₂ with the pair cocycle (κ₁, κ₂). Its three coefficient homs pr₁, pr₂, prSum (first fibre, second fibre, fibre sum) carry the fiber-product lift onto liftMark t c₁, liftMark t c₂, liftMark t (c₁ + c₂); the relator values then add by Marking.map_{tame,wild}Value (exactly the d1Fun_add pattern). Note prSum : FiberProd →* CentExt (c₁ + c₂) is a hom precisely because the summed fibre matches κ₁ + κ₂; the naive CentExt (c₁ + c₂) →* CentExt c₁ × CentExt c₂ is not a homomorphism.

@[implicit_reducible]

instance GQ2.WordCoh2.instAddTwoCocycle {L : Type u_2} [Group L] : Add (TwoCocycle L)

Pointwise sum of 2-cocycles.

Equations

• GQ2.WordCoh2.instAddTwoCocycle = { add := fun (c₁ c₂ : GQ2.WordCoh2.TwoCocycle L) => { κ := fun (a b : L) => c₁.κ a b + c₂.κ a b, norm := ⋯, cocyc := ⋯ } }

def GQ2.WordCoh2.FiberProd {L : Type u_2} [Group L] (_c₁ _c₂ : TwoCocycle L) : Type u_2

The fiber product CentExt c₁ ×_L CentExt c₂: a central extension of L by 𝔽₂ × 𝔽₂.

Equations

• GQ2.WordCoh2.FiberProd _c₁ _c₂ = (L × ZMod 2 × ZMod 2)

def GQ2.WordCoh2.FiberProd.base {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} (p : FiberProd c₁ c₂) : L

Base coordinate.

Equations

• p.base = p.1

def GQ2.WordCoh2.FiberProd.fibA {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} (p : FiberProd c₁ c₂) : ZMod 2

First fibre coordinate.

Equations

• p.fibA = p.2.1

def GQ2.WordCoh2.FiberProd.fibB {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} (p : FiberProd c₁ c₂) : ZMod 2

Second fibre coordinate.

Equations

• p.fibB = p.2.2

@[implicit_reducible]

instance GQ2.WordCoh2.FiberProd.instGroup {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} : Group (FiberProd c₁ c₂)

Equations

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

def GQ2.WordCoh2.FiberProd.pr1 {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} : FiberProd c₁ c₂ →* CentExt c₁

Projection to the first central extension.

Equations

• GQ2.WordCoh2.FiberProd.pr1 = { toFun := fun (p : GQ2.WordCoh2.FiberProd c₁ c₂) => (p.base, p.fibA), map_one' := ⋯, map_mul' := ⋯ }

def GQ2.WordCoh2.FiberProd.pr2 {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} : FiberProd c₁ c₂ →* CentExt c₂

Projection to the second central extension.

Equations

• GQ2.WordCoh2.FiberProd.pr2 = { toFun := fun (p : GQ2.WordCoh2.FiberProd c₁ c₂) => (p.base, p.fibB), map_one' := ⋯, map_mul' := ⋯ }

def GQ2.WordCoh2.FiberProd.prSum {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} : FiberProd c₁ c₂ →* CentExt (c₁ + c₂)

The fibre-sum hom to the sum extension — a homomorphism because fibA + fibB tracks κ₁ + κ₂.

Equations

• GQ2.WordCoh2.FiberProd.prSum = { toFun := fun (p : GQ2.WordCoh2.FiberProd c₁ c₂) => (p.base, p.fibA + p.fibB), map_one' := ⋯, map_mul' := ⋯ }

instance GQ2.WordCoh2.FiberProd.instFinite {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} [Finite L] : Finite (FiberProd c₁ c₂)

def GQ2.WordCoh2.liftMarkFP {L : Type u_2} [Group L] (t : Marking L) (c₁ c₂ : TwoCocycle L) : Marking (FiberProd c₁ c₂)

The fiber-product lift of a base marking (both fibres zero).

Equations

• GQ2.WordCoh2.liftMarkFP t c₁ c₂ = { σ := (t.σ, 0, 0), τ := (t.τ, 0, 0), x₀ := (t.x₀, 0, 0), x₁ := (t.x₁, 0, 0) }

theorem GQ2.WordCoh2.relZPair_add {L : Type u_2} [Group L] [Finite L] (t : Marking L) (c₁ c₂ : TwoCocycle L) : relZPair t (c₁ + c₂) = relZPair t c₁ + relZPair t c₂

Additivity of the relator obstruction.

Vanishing on coboundaries: obs kills B² (upgrading #H² ≤ 2 to H² ↪ 𝔽₂)

The obstruction obs (the sum of the tame and wild relator fibre values) vanishes on continuous 2-coboundaries. The mechanism: a finite-level coboundary κ = δ¹λ gives a central extension CentExt (δ¹λ) that is trivialised by Ψ_λ : (l, z) ↦ (l, z + λ l) onto the split extension CentExt 0. Under Ψ_λ, the lifted marking becomes the λ-shifted split marking, whose relator fibres are a 1 (the shift laws) plus λ of the (dying) relator base — so both relator fibres pick up the same value and their sum is 0. Combined with obs_ker_le, this makes obs descend to an injection H²(Γ_A, 𝔽₂) ↪ 𝔽₂ — the degree-2 presentation-comparison, reusable Thm-4.2-ward.

theorem GQ2.WordCoh2.trivialMarking_tameValue {L : Type u_2} [Group L] : { σ := 1, τ := 1, x₀ := 1, x₁ := 1 }.tameValue = 1

The trivial marking (all four generators 1) satisfies the tame relation.

theorem GQ2.WordCoh2.trivialMarking_wildValue {L : Type u_2} [Group L] : { σ := 1, τ := 1, x₀ := 1, x₁ := 1 }.wildValue = 1

The trivial marking (all four generators 1) satisfies the wild relation.

def GQ2.WordCoh2.zeroCocycle {L : Type u_2} [Group L] : TwoCocycle L

The trivial (split) 2-cocycle κ ≡ 0: CentExt zeroCocycle = L × 𝔽₂ is the direct product.

Equations

• GQ2.WordCoh2.zeroCocycle = { κ := fun (x x_1 : L) => 0, norm := GQ2.WordCoh2.zeroCocycle._proof_1, cocyc := ⋯ }

def GQ2.WordCoh2.fibHom0 {L : Type u_2} [Group L] : CentExt zeroCocycle →* Multiplicative (ZMod 2)

The fibre projection CentExt zeroCocycle →* Multiplicative 𝔽₂ — a homomorphism because the split extension is the direct product (κ ≡ 0).

Equations

• GQ2.WordCoh2.fibHom0 = { toFun := fun (p : GQ2.WordCoh2.CentExt GQ2.WordCoh2.zeroCocycle) => Multiplicative.ofAdd p.fib, map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.WordCoh2.relZPair_zero {L : Type u_2} [Group L] [Finite L] (t : Marking L) : relZPair t zeroCocycle = (0, 0)

The split extension has balanced (zero) relator obstruction: both relator fibres vanish, as they are the image of the trivial marking ⟨1, 1, 1, 1⟩ under fibHom0.

def GQ2.WordCoh2.coboundaryCocycle {L : Type u_2} [Group L] (lam : L → ZMod 2) (hlam1 : lam 1 = 0) : TwoCocycle L

The coboundary 2-cocycle δ¹λ: κ (a, b) = λ a + λ b + λ (a b) (trivial action, char 2). Requires the normalization λ 1 = 0.

Equations

• GQ2.WordCoh2.coboundaryCocycle lam hlam1 = { κ := fun (a b : L) => lam a + lam b + lam (a * b), norm := ⋯, cocyc := ⋯ }

def GQ2.WordCoh2.Psi {L : Type u_2} [Group L] (lam : L → ZMod 2) (hlam1 : lam 1 = 0) : CentExt (coboundaryCocycle lam hlam1) →* CentExt zeroCocycle

The trivialization hom Ψ_λ : (l, z) ↦ (l, z + λ l), an iso CentExt (δ¹λ) ≃* CentExt 0 of the coboundary extension with the split extension.

Equations

• GQ2.WordCoh2.Psi lam hlam1 = { toFun := fun (p : GQ2.WordCoh2.CentExt (GQ2.WordCoh2.coboundaryCocycle lam hlam1)) => (p.base, p.fib + lam p.base), map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.WordCoh2.map_Psi_liftMark {L : Type u_2} [Group L] (t : Marking L) (lam : L → ZMod 2) (hlam1 : lam 1 = 0) : Marking.map (Psi lam hlam1) (liftMark t (coboundaryCocycle lam hlam1)) = shiftLiftMark t ![lam t.σ, lam t.τ, lam t.x₀, lam t.x₁] zeroCocycle

Ψ_λ carries the lifted marking of the coboundary extension onto the λ-shifted split marking.

theorem GQ2.WordCoh2.obs_coboundary_eq {L : Type u_2} [Group L] [Finite L] (t : Marking L) (lam : L → ZMod 2) (hlam1 : lam 1 = 0) : (relZPair t (coboundaryCocycle lam hlam1)).1 + (relZPair t (coboundaryCocycle lam hlam1)).2 = lam t.tameValue + lam t.wildValue

The obstruction of a finite-level coboundary is λ (tame relator) + λ (wild relator). At an admissible level both relators die, so this is 0 — the vanishing of obs on B².

The injectivity keystone: a balanced inflated cocycle is a coboundary

Assembling the shift laws (exists_shift_of_relZ_eq) with cocycle_mem_B2: if a finite-level 2-cocycle c has balanced relator obstruction (tame.fib = wild.fib, i.e. relZPair ∈ Δ = im d¹_triv), then the 2-cocycle it inflates to on Γ_A — (x, y) ↦ c.κ (level x) (level y) — is a continuous 2-coboundary. This is the algebraic half of θ-injectivity: a class killed by θ (balanced obstruction) is trivial after factoring the continuous cocycle through a finite level. The finite-level factorization is supplied at the topological consumer.

noncomputable def GQ2.WordCoh2.levelProj (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hU : NA ≤ ↑U.toOpenSubgroup) : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA →ₜ* ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup

The level projection Γ_A = F₄ ⧸ N_A ↠ F₄ ⧸ U for N_A ≤ U.

Equations

• GQ2.WordCoh2.levelProj U hU = GQ2.quotientLift GQ2.NA (GQ2.quotientMk ↑U.toOpenSubgroup) ⋯

@[simp]

theorem GQ2.WordCoh2.levelProj_quotientMk (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hU : NA ≤ ↑U.toOpenSubgroup) (g : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) : (levelProj U hU) ((quotientMk NA) g) = (QuotientGroup.mk' ↑U.toOpenSubgroup) g

theorem GQ2.WordCoh2.inflated_cocycle_mem_B2 [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] [TopologicalSpace (ZMod 2)] [DiscreteTopology (ZMod 2)] (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NA ≤ ↑U.toOpenSubgroup) (c : TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (hrel : (liftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) c).tameValue.fib = (liftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) c).wildValue.fib) (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) : (fun (p : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) => c.κ ((levelProj U hU) p.1) ((levelProj U hU) p.2)) ∈ ContCoh.B2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)

Injectivity keystone. A finite-level cocycle with balanced relator obstruction inflates to a continuous 2-coboundary on Γ_A. ([Finite (F₄ ⧸ U)] at statement level, as for NA_le_ker_shiftLift.)

Factoring a continuous cocycle through a finite level (the topological input)

The remaining input to θ: a continuous 2-cochain on the profinite Γ_A is uniformly locally constant, hence factors through a finite quotient F₄ ⧸ U (N_A ≤ U). The core is a compactness argument (exists_openNormalSubgroup_factor_two): a continuous f : G × G → M to a discrete space is invariant under right-translation of both arguments by a single open normal subgroup. Applied to a normalized continuous 2-cocycle κ on Γ_A and transported to F₄ ⧸ U := comap N_A V, it yields a genuine TwoCocycle (F₄ ⧸ U) inflating to κ — the hypothesis that inflated_cocycle_mem_B2 consumes.

theorem GQ2.WordCoh2.exists_openNormalSubgroup_factor_two {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {M : Type u_3} [TopologicalSpace M] [DiscreteTopology M] (f : G × G → M) (hf : Continuous f) : ∃ (V : OpenNormalSubgroup G), ∀ (x y u : G), u ∈ V → ∀ v ∈ V, f (x * u, y * v) = f (x, y)

Uniform local constancy (2-variable form): a continuous map f : G × G → M from a profinite group to a discrete space is invariant under right-translation of both arguments by a single open normal subgroup V — equivalently, f factors through (G ⧸ V) × (G ⧸ V). Proof: each point has a basic clopen box on which f is constant (isOpen_prod_iff + exist_openNormalSubgroup_sub_open_nhds_of_one); compactness extracts a finite subcover; V is the (finite) intersection of the boxes' subgroups.

theorem GQ2.WordCoh2.exists_twoCocycle_factor (κ : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA → ZMod 2) (hκc : Continuous κ) (hκ1 : κ (1, 1) = 0) (hκcoc : ∀ (a b c : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA), κ (a, b) + κ (a * b, c) = κ (a, b * c) + κ (b, c)) : ∃ (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hU : NA ≤ ↑U.toOpenSubgroup) (c : TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)), ∀ (x y : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA), κ (x, y) = c.κ ((levelProj U hU) x) ((levelProj U hU) y)

Factoring a normalized continuous 2-cocycle. A continuous κ : Γ_A × Γ_A → 𝔽₂ that is normalized (κ (1,1) = 0) and satisfies the 2-cocycle identity descends to a genuine TwoCocycle (F₄ ⧸ U) at some finite level N_A ≤ U, inflating back to κ through levelProj.

theorem GQ2.WordCoh2.exists_oneCochain_factor (ψ : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA → ZMod 2) (hψc : Continuous ψ) : ∃ (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hU : NA ≤ ↑U.toOpenSubgroup) (lam : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup → ZMod 2), ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA), ψ x = lam ((levelProj U hU) x)

Factoring a continuous 1-cochain. A continuous ψ : Γ_A → 𝔽₂ descends to a function on a finite admissible level N_A ≤ U (via the same compactness lemma applied to ψ ∘ fst).

Injectivity, assembled: a balanced continuous cocycle is a coboundary

Combining the factoring (exists_twoCocycle_factor) with the injectivity keystone (inflated_cocycle_mem_B2): a continuous 2-cocycle κ on Γ_A that factors through a finite level c with balanced relator obstruction is a continuous 2-coboundary. This is the kernel-side of θ-injectivity in its consumable form.

theorem GQ2.WordCoh2.mem_B2_of_factor_balanced [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] [TopologicalSpace (ZMod 2)] [DiscreteTopology (ZMod 2)] (κ : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA → ZMod 2) (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) [Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)] (hU : NA ≤ ↑U.toOpenSubgroup) (c : TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)) (hfact : ∀ (x y : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA), κ (x, y) = c.κ ((levelProj U hU) x) ((levelProj U hU) y)) (hbal : (liftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) c).tameValue.fib = (liftMark (Marking.map (QuotientGroup.mk' ↑U.toOpenSubgroup) univMarking) c).wildValue.fib) : κ ∈ ContCoh.B2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)

Injectivity, consumable form. If a continuous cochain κ factors through a finite level c (κ = c.κ ∘ (levelProj × levelProj)) whose relator obstruction is balanced (tame.fib = wild.fib), then κ is a continuous 2-coboundary.

The obstruction map and the cardinality bound #H²(Γ_A, 𝔽₂) ≤ 2

Assembling everything. The obstruction obs : Z²_cont(Γ_A, 𝔽₂) →+ 𝔽₂ sends a continuous 2-cocycle to the sum of its tame and wild relator obstructions, computed after normalizing at (1,1) and factoring through a finite admissible level. The value is level-independent (relZPair_comap) and additive (relZPair_add), and its kernel lands in B² (mem_B2_of_factor_balanced). Hence H² = Z²/B² is a quotient of Z²/ker obs ↪ 𝔽₂, giving #H²(Γ_A, 𝔽₂) ≤ #𝔽₂ = 2.

theorem GQ2.WordCoh2.TwoCocycle.ext {L : Type u_2} [Group L] {c d : TwoCocycle L} (h : c.κ = d.κ) : c = d

Two TwoCocycles with equal cochain are equal (the norm/cocyc fields are propositions).

instance GQ2.WordCoh2.quotient_finite_openNormal (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) : Finite (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup)

An open normal subgroup of the compact free profinite group has finite quotient.

structure GQ2.WordCoh2.LevelFactor (κ : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA → ZMod 2) : Type

A factorization of a Γ_A-cochain κ through a finite admissible level: κ (x, y) = c.κ (levelProj x) (levelProj y).

• U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop

  The finite admissible level F₄ ⧸ U.

• hU : NA ≤ ↑self.U.toOpenSubgroup

  N_A ≤ U, so Γ_A = F₄ ⧸ N_A ↠ F₄ ⧸ U.

• c : TwoCocycle (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑self.U.toOpenSubgroup)

  The finite-level 2-cocycle whose inflation is κ.

• hfact (x y : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) : κ (x, y) = self.c.κ ((levelProj self.U ⋯) x) ((levelProj self.U ⋯) y)

  κ is the inflation of c along levelProj.

noncomputable def GQ2.WordCoh2.LevelFactor.obs {κ : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA → ZMod 2} (F : LevelFactor κ) : ZMod 2

The relator obstruction of a factorization: the sum of the tame and wild relator fibre-z values of the finite-level cocycle.

Equations

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

theorem GQ2.WordCoh2.LevelFactor.obs_eq_comap {κ : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA → ZMod 2} (F : LevelFactor κ) (W : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (proj : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑W.toOpenSubgroup →* ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑F.U.toOpenSubgroup) (hproj : proj.comp (QuotientGroup.mk' ↑W.toOpenSubgroup) = QuotientGroup.mk' ↑F.U.toOpenSubgroup) : F.obs = (relZPair (Marking.map (QuotientGroup.mk' ↑W.toOpenSubgroup) univMarking) (F.c.comap proj)).1 + (relZPair (Marking.map (QuotientGroup.mk' ↑W.toOpenSubgroup) univMarking) (F.c.comap proj)).2

Level-independence. F.obs may be computed at any finer level W (via a projection proj : F₄ ⧸ W → F₄ ⧸ F.U with proj ∘ mk_W = mk_{F.U}) through the pulled-back cocycle F.c.comap proj — this is relZPair_comap.

theorem GQ2.WordCoh2.LevelFactor.obs_congr {κ : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA → ZMod 2} (F₁ F₂ : LevelFactor κ) : F₁.obs = F₂.obs

Well-definedness. F.obs depends only on κ, not on the chosen factorization: two factorizations agree at their common refinement F₁.U ⊓ F₂.U, where both finite-level cocycles pull back to the same cocycle (both inflate to κ).

theorem GQ2.WordCoh2.levelProj_comp (W U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) (hUW : NA ≤ ↑W.toOpenSubgroup) (hU : NA ≤ ↑U.toOpenSubgroup) (proj : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑W.toOpenSubgroup →* ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ ↑U.toOpenSubgroup) (hproj : proj.comp (QuotientGroup.mk' ↑W.toOpenSubgroup) = QuotientGroup.mk' ↑U.toOpenSubgroup) (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) : proj ((levelProj W hUW) x) = (levelProj U hU) x

The two projections F₄ ⧸ W → F₄ ⧸ U (for N_A ≤ W ≤ U, via proj) and the level maps Γ_A → F₄ ⧸ W → F₄ ⧸ U compose to the level map Γ_A → F₄ ⧸ U.

noncomputable def GQ2.WordCoh2.normalizeCochain (κ : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA → ZMod 2) : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA → ZMod 2

Normalize a 2-cochain at (1,1) by subtracting the (coboundary) constant κ (1,1).

Equations

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

theorem GQ2.WordCoh2.const2_mem_B2 [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) (v : ZMod 2) : (fun (x : (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) × ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) => v) ∈ ContCoh.B2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)

Under the trivial action, a constant 2-cochain is a continuous coboundary (= δ¹ of a constant 1-cochain).

theorem GQ2.WordCoh2.nonempty_levelFactor_normalize [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2))) : Nonempty (LevelFactor (normalizeCochain ↑φ))

The normalization of a continuous 2-cocycle factors through a finite admissible level.

noncomputable def GQ2.WordCoh2.obsFun [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2))) : ZMod 2

The per-cocycle obstruction: the relator obstruction of any factorization of the normalization.

Equations

• GQ2.WordCoh2.obsFun htriv φ = ⋯.some.obs

theorem GQ2.WordCoh2.obsFun_eq [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2))) (F : LevelFactor (normalizeCochain ↑φ)) : obsFun htriv φ = F.obs

obsFun may be computed at any factorization of the normalization (well-definedness).

theorem GQ2.WordCoh2.obsFun_add [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) (φ ψ : ↥(ContCoh.Z2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2))) : obsFun htriv (φ + ψ) = obsFun htriv φ + obsFun htriv ψ

Additivity of the obstruction. Both φ and ψ factor through a common refinement W = U_φ ⊓ U_ψ, where their finite-level cocycles pull back and add (relZPair_add).

noncomputable def GQ2.WordCoh2.obs [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) : ↥(ContCoh.Z2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)) →+ ZMod 2

The obstruction homomorphism Z²_cont(Γ_A, 𝔽₂) →+ 𝔽₂.

Equations

• GQ2.WordCoh2.obs htriv = AddMonoidHom.mk' (GQ2.WordCoh2.obsFun htriv) ⋯

theorem GQ2.WordCoh2.obs_ker_le [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) : (obs htriv).ker ≤ (ContCoh.B2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)).addSubgroupOf (ContCoh.Z2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2))

The kernel of the obstruction lands in the 2-coboundaries: an obs-trivial cocycle is balanced, hence a coboundary (mem_B2_of_factor_balanced), after adding back the normalization constant.

theorem GQ2.WordCoh2.obs_B2_eq_zero [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) : (ContCoh.B2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)).addSubgroupOf (ContCoh.Z2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)) ≤ (obs htriv).ker

obs kills B² (the vanishing on coboundaries). A continuous coboundary κ = δ¹ψ normalizes to δ¹ψ' (ψ' 1 = 0), which factors through a finite admissible level as coboundaryCocycle λ; its obstruction is λ(tameValue) + λ(wildValue) = λ 1 + λ 1 = 0 since both relators die at that level. Combined with obs_ker_le, this makes obs descend to an injection H²(Γ_A, 𝔽₂) ↪ 𝔽₂ — the degree-2 presentation-comparison.

theorem GQ2.WordCoh2.obs_ker_eq_B2 [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) : (obs htriv).ker = (ContCoh.B2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)).addSubgroupOf (ContCoh.Z2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2))

ker obs = B² (the Γ_A half-torsor proof, lemma A). The obstruction is trivial on coboundaries and nowhere else, so it descends to an injection H²(Γ_A, 𝔽₂) ↪ 𝔽₂ — the reusable degree-2 presentation-comparison. (obs_ker_le ⊆, obs_B2_eq_zero ⊇.)

noncomputable def GQ2.WordCoh2.obsH2 [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) : ContCoh.H2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2) →+ ZMod 2

The descended obstruction H²(Γ_A, 𝔽₂) →+ 𝔽₂, and its injectivity: a continuous 2-cocycle whose obstruction is nonzero is not a coboundary.

Equations

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

theorem GQ2.WordCoh2.obsH2_injective [DistribMulAction (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (ZMod 2)] (htriv : ∀ (x : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) (m : ZMod 2), x • m = m) : Function.Injective ⇑(obsH2 htriv)