The D_R degree-2 presentation comparison — single-relator obstruction (ticket R13b)

The D_R = ⟨s, x, y | r₂⟩_{pro-2} analogue of the (non-module) Γ_A degree-2 bridge GQ2/WordCoh2.lean. Because D_R has a single relator, the relator obstruction is a single 𝔽₂ value (not the tame/wild pair of Γ_A), so there is no "balance" (im d¹) condition: the obstruction map lands in 𝔽₂ directly and injectivity is exactly the #H² ≤ 2 statement.

GQ2/WordCoh2.lean is not a module, so its generic central-extension algebra cannot be imported here; the ## Generic central-extension algebra section below re-derives the pieces we need (TwoCocycle, CentExt, FiberProd, zeroCocycle, coboundaryCocycle, Psi, TwoCocycle.comap/projExt, exists_openNormalSubgroup_factor_two) verbatim in the GQ2.DRCoh namespace. On top of that:

• drRelZ m c — the fibre of drWord evaluated at the zero-fibre lift of a triple m : Fin 3 → L; naturality (drRelZ_comap), additivity (drRelZ_add), coboundary law (drRelZ_coboundary);
• the profinite factoring exists_twoCocycle_factor_DR (the generic compactness core applied to the pro-2 group D_R directly — the relation is inherited by every finite quotient D_R ⧸ V);
• DRLevelFactor/obs/obs_congr — the level-independent single-𝔽₂ obstruction;
• the injectivity keystone: when obs = 0 the relator dies exactly, so drLiftHom directly builds a splitting section D_R → CentExt c and the pulled-back cocycle is a continuous coboundary;
• obsH2_DR : H²(D_R, 𝔽₂) →+ 𝔽₂, its injectivity, and the bridge obsFun_DR_eq_of_factor computing the obstruction at any finite quotient — consumed by GQ2/Roe/DRH2.lean and DRDemushkin.lean.

Generic central-extension algebra (re-derived from GQ2/WordCoh2.lean)

Verbatim ports of the generic-in-L declarations of the non-module GQ2/WordCoh2.lean, placed in the fresh GQ2.DRCoh namespace to avoid any clash with GQ2.WordCoh2.* (both are visible in the top-level GQ2.lean aggregate).

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

A ZMod 2-valued 2-cocycle on L, normalized at (1,1) (WordCoh2.TwoCocycle).

• κ : 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.DRCoh.TwoCocycle.κ_one_left {L : Type u_1} [Group L] (c : TwoCocycle L) (l : L) : c.κ 1 l = 0

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

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

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

The central extension L ×_κ ZMod 2 (WordCoh2.CentExt).

Equations

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

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

Base coordinate.

Equations

• p.base = p.1

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

Fibre coordinate.

Equations

• p.fib = p.2

theorem GQ2.DRCoh.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.DRCoh.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.DRCoh.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.DRCoh.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.DRCoh.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.DRCoh.CentExt.proj {L : Type u_1} [Group L] (c : TwoCocycle L) : CentExt c →* L

The base projection CentExt c →* L.

Equations

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

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

The central inclusion ZMod 2 → CentExt c.

Equations

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

theorem GQ2.DRCoh.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

@[simp]

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

@[simp]

theorem GQ2.DRCoh.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

@[implicit_reducible]

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

Equations

• GQ2.DRCoh.CentExt.instTopologicalSpace = ⊥

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

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

Level change: pulling a cocycle back along a group hom

def GQ2.DRCoh.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 φ : L' →* L.

Equations

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

@[simp]

theorem GQ2.DRCoh.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.DRCoh.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 CentExt (c.comap φ) →* CentExt c.

Equations

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

@[simp]

theorem GQ2.DRCoh.projExt_fib {L : Type u_2} {L' : Type u_3} [Group L] [Group L'] (c : TwoCocycle L) (φ : L' →* L) (p : CentExt (c.comap φ)) : ((projExt c φ) p).fib = p.fib

Additivity infrastructure: sum cocycle and fiber product

@[implicit_reducible]

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

Pointwise sum of 2-cocycles.

Equations

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

@[simp]

theorem GQ2.DRCoh.TwoCocycle.add_κ {L : Type u_2} [Group L] (c₁ c₂ : TwoCocycle L) (a b : L) : (c₁ + c₂).κ a b = c₁.κ a b + c₂.κ a b

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

The fiber product CentExt c₁ ×_L CentExt c₂.

Equations

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

def GQ2.DRCoh.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.DRCoh.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.DRCoh.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.DRCoh.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.DRCoh.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.DRCoh.FiberProd.pr1 = { toFun := fun (p : GQ2.DRCoh.FiberProd c₁ c₂) => (p.base, p.fibA), map_one' := ⋯, map_mul' := ⋯ }

def GQ2.DRCoh.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.DRCoh.FiberProd.pr2 = { toFun := fun (p : GQ2.DRCoh.FiberProd c₁ c₂) => (p.base, p.fibB), map_one' := ⋯, map_mul' := ⋯ }

def GQ2.DRCoh.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.

Equations

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

@[simp]

theorem GQ2.DRCoh.FiberProd.pr1_fib {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} (p : FiberProd c₁ c₂) : (pr1 p).fib = p.fibA

@[simp]

theorem GQ2.DRCoh.FiberProd.pr2_fib {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} (p : FiberProd c₁ c₂) : (pr2 p).fib = p.fibB

@[simp]

theorem GQ2.DRCoh.FiberProd.prSum_fib {L : Type u_2} [Group L] {c₁ c₂ : TwoCocycle L} (p : FiberProd c₁ c₂) : (prSum p).fib = p.fibA + p.fibB

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

The split and coboundary cocycles

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

The trivial (split) 2-cocycle κ ≡ 0.

Equations

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

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

The fibre projection CentExt zeroCocycle →* Multiplicative 𝔽₂.

Equations

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

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

The coboundary 2-cocycle δ¹λ.

Equations

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

def GQ2.DRCoh.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).

Equations

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

@[simp]

theorem GQ2.DRCoh.Psi_fib {L : Type u_2} [Group L] (lam : L → ZMod 2) (hlam1 : lam 1 = 0) (p : CentExt (coboundaryCocycle lam hlam1)) : ((Psi lam hlam1) p).fib = p.fib + lam p.base

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

Two TwoCocycles with equal cochain are equal.

Factoring a continuous 2-variable map through a finite quotient

theorem GQ2.DRCoh.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) — WordCoh2.exists_openNormalSubgroup_factor_two, generic in the profinite group G.

@[reducible, inline]

abbrev GQ2.DRT : Type

The carrier of D_R as a plain Type. Coercing the ProfiniteGrp object DR once (rather than inside an explicit product DRT × DRT, where the second ascription fails to fire) avoids a universe-inference quirk.

Equations

• GQ2.DRT = ↑GQ2.DR.toProfinite.toTop

The single-relator obstruction drRelZ

def GQ2.drLift {L : Type u_1} [Group L] (m : Fin 3 → L) (c : DRCoh.TwoCocycle L) (k : Fin 3) : DRCoh.CentExt c

The three D_R generators m 0, m 1, m 2 placed in CentExt c with zero fibre.

Equations

• GQ2.drLift m c k = (m k, 0)

@[simp]

theorem GQ2.drLift_base {L : Type u_1} [Group L] (m : Fin 3 → L) (c : DRCoh.TwoCocycle L) (k : Fin 3) : (drLift m c k).base = m k

@[simp]

theorem GQ2.drLift_fib {L : Type u_1} [Group L] (m : Fin 3 → L) (c : DRCoh.TwoCocycle L) (k : Fin 3) : (drLift m c k).fib = 0

def GQ2.drRelZ {L : Type u_1} [Group L] (m : Fin 3 → L) (c : DRCoh.TwoCocycle L) : ZMod 2

The single-relator obstruction of a 2-cocycle c relative to the marking m : Fin 3 → L: the fibre coordinate of drWord evaluated at the zero-fibre lift. The D_R analogue of WordCoh2.relZPair, but a single 𝔽₂ value (one relator).

Equations

• GQ2.drRelZ m c = (GQ2.drWord (GQ2.drLift m c 0) (GQ2.drLift m c 1) (GQ2.drLift m c 2)).fib

theorem GQ2.drRelZ_base {L : Type u_1} [Group L] (m : Fin 3 → L) (c : DRCoh.TwoCocycle L) : (drWord (drLift m c 0) (drLift m c 1) (drLift m c 2)).base = drWord (m 0) (m 1) (m 2)

The base of the lifted relator value is the base relator value.

theorem GQ2.drRelZ_comap {L : Type u_1} {L' : Type u_2} [Group L] [Group L'] (m : Fin 3 → L') (c : DRCoh.TwoCocycle L) (φ : L' →* L) : drRelZ (fun (k : Fin 3) => φ (m k)) c = drRelZ m (c.comap φ)

Level-independence. Pulling c back along φ and pushing the marking forward by φ give the same obstruction (WordCoh2.relZPair_comap, single relator).

def GQ2.drLiftFP {L : Type u_1} [Group L] (m : Fin 3 → L) (c₁ c₂ : DRCoh.TwoCocycle L) (k : Fin 3) : DRCoh.FiberProd c₁ c₂

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

Equations

• GQ2.drLiftFP m c₁ c₂ k = (m k, 0, 0)

theorem GQ2.drRelZ_add {L : Type u_1} [Group L] (m : Fin 3 → L) (c₁ c₂ : DRCoh.TwoCocycle L) : drRelZ m (c₁ + c₂) = drRelZ m c₁ + drRelZ m c₂

Additivity of the relator obstruction (WordCoh2.relZPair_add, single relator).

theorem GQ2.drRelZ_zero {L : Type u_1} [Group L] (m : Fin 3 → L) : drRelZ m DRCoh.zeroCocycle = 0

The obstruction of the split cocycle vanishes (WordCoh2.relZPair_zero).

theorem GQ2.drRelZ_coboundary {L : Type u_1} [Group L] (m : Fin 3 → L) (lam : L → ZMod 2) (hlam1 : lam 1 = 0) : drRelZ m (DRCoh.coboundaryCocycle lam hlam1) = lam (drWord (m 0) (m 1) (m 2))

The obstruction of a coboundary is lam of the base relator value (WordCoh2.obs_coboundary_eq, single relator). It vanishes when the marking satisfies the relation.

The named generator triple and its image obstruction

noncomputable def GQ2.drGens : Fin 3 → DRT

The marked generators s, x, y of D_R, packaged as a triple.

Equations

• GQ2.drGens = ![GQ2.drS, GQ2.drX, GQ2.drY]

@[simp]

theorem GQ2.drGens_zero : drGens 0 = drS

@[simp]

theorem GQ2.drGens_one : drGens 1 = drX

@[simp]

theorem GQ2.drGens_two : drGens 2 = drY

theorem GQ2.drRelZ_drGens_comap {L : Type u_1} [Group L] (φ : DRT →* L) (c : DRCoh.TwoCocycle L) : drRelZ (fun (k : Fin 3) => φ (drGens k)) c = drRelZ drGens (c.comap φ)

The obstruction of c read through the marking φ ∘ (s, x, y) for a hom φ : D_R →* L.

Factoring a continuous cocycle through a finite quotient of D_R

D_R is profinite and already the presented pro-2 group, so the generic compactness core applies directly: a continuous 2-cocycle on D_R factors through a finite quotient D_R ⧸ V, and the relation drWord (s,x,y) = 1 is inherited by that quotient (no N_A/admissibility machinery).

theorem GQ2.exists_twoCocycle_factor_DR (κ : DRT × DRT → ZMod 2) (hκc : Continuous κ) (hκ1 : κ (1, 1) = 0) (hκcoc : ∀ (a b c : DRT), κ (a, b) + κ (a * b, c) = κ (a, b * c) + κ (b, c)) : ∃ (V : OpenNormalSubgroup DRT) (c : DRCoh.TwoCocycle (DRT ⧸ ↑V.toOpenSubgroup)), ∀ (x y : DRT), κ (x, y) = c.κ ((QuotientGroup.mk' ↑V.toOpenSubgroup) x) ((QuotientGroup.mk' ↑V.toOpenSubgroup) y)

Factoring a normalized continuous 2-cocycle on D_R (WordCoh2.exists_twoCocycle_factor, directly on D_R).

theorem GQ2.exists_oneCochain_factor_DR (ψ : DRT → ZMod 2) (hψc : Continuous ψ) : ∃ (V : OpenNormalSubgroup DRT) (lam : DRT ⧸ ↑V.toOpenSubgroup → ZMod 2), ∀ (x : DRT), ψ x = lam ((QuotientGroup.mk' ↑V.toOpenSubgroup) x)

Factoring a continuous 1-cochain on D_R.

The level-independent obstruction DRLevelFactor.obs

instance GQ2.quotient_finite_openNormal_DR (V : OpenNormalSubgroup DRT) : Finite (DRT ⧸ ↑V.toOpenSubgroup)

Every open normal subgroup of D_R has finite quotient.

structure GQ2.DRLevelFactor (κ : DRT × DRT → ZMod 2) : Type

A factorization of a D_R-cochain κ through a finite quotient D_R ⧸ V.

• V : OpenNormalSubgroup DRT

  The finite level D_R ⧸ V.

• c : DRCoh.TwoCocycle (DRT ⧸ ↑self.V.toOpenSubgroup)

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

• hfact (x y : DRT) : κ (x, y) = self.c.κ ((QuotientGroup.mk' ↑self.V.toOpenSubgroup) x) ((QuotientGroup.mk' ↑self.V.toOpenSubgroup) y)

  κ is the inflation of c.

noncomputable def GQ2.DRLevelFactor.obs {κ : DRT × DRT → ZMod 2} (F : DRLevelFactor κ) : ZMod 2

The relator obstruction of a factorization: the single-relator obstruction of the finite-level cocycle at the projected generators.

Equations

• F.obs = GQ2.drRelZ (fun (k : Fin 3) => (QuotientGroup.mk' ↑F.V.toOpenSubgroup) (GQ2.drGens k)) F.c

theorem GQ2.DRLevelFactor.obs_eq_comap {κ : DRT × DRT → ZMod 2} (F : DRLevelFactor κ) (W : OpenNormalSubgroup DRT) (proj : DRT ⧸ ↑W.toOpenSubgroup →* DRT ⧸ ↑F.V.toOpenSubgroup) (hproj : proj.comp (QuotientGroup.mk' ↑W.toOpenSubgroup) = QuotientGroup.mk' ↑F.V.toOpenSubgroup) : F.obs = drRelZ (fun (k : Fin 3) => (QuotientGroup.mk' ↑W.toOpenSubgroup) (drGens k)) (F.c.comap proj)

Level-independence. F.obs may be computed at any finer level W through the pulled-back cocycle F.c.comap proj.

theorem GQ2.DRLevelFactor.obs_congr {κ : DRT × DRT → ZMod 2} (F₁ F₂ : DRLevelFactor κ) : F₁.obs = F₂.obs

Well-definedness. F.obs depends only on κ, not on the chosen factorization.

CentExt over a finite quotient of D_R is pro-2

theorem GQ2.isProP_CentExt {V : OpenNormalSubgroup DRT} (c : DRCoh.TwoCocycle (DRT ⧸ ↑V.toOpenSubgroup)) : IsProP 2 (DRCoh.CentExt c)

CentExt c over a finite quotient of the pro-2 group D_R is a finite 2-group, hence pro-2 — the target hypothesis of drLiftHom.

The relation holds at every finite level

theorem GQ2.drWord_mk_eq_one (V : OpenNormalSubgroup DRT) : drWord ((QuotientGroup.mk' ↑V.toOpenSubgroup) (drGens 0)) ((QuotientGroup.mk' ↑V.toOpenSubgroup) (drGens 1)) ((QuotientGroup.mk' ↑V.toOpenSubgroup) (drGens 2)) = 1

The Roe relation drWord (s, x, y) = 1 is inherited by every finite quotient D_R ⧸ V.

The obstruction homomorphism and its injectivity

noncomputable def GQ2.normalizeCochain (κ : DRT × DRT → ZMod 2) : DRT × DRT → ZMod 2

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

Equations

• GQ2.normalizeCochain κ = κ - fun (x : GQ2.DRT × GQ2.DRT) => κ (1, 1)

theorem GQ2.const2_mem_B2 [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) (v : ZMod 2) : (fun (x : DRT × DRT) => v) ∈ ContCoh.B2 DRT (ZMod 2)

A constant 2-cochain is a continuous coboundary.

theorem GQ2.nonempty_levelFactor_normalize [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 DRT (ZMod 2))) : Nonempty (DRLevelFactor (normalizeCochain ↑φ))

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

noncomputable def GQ2.obsFun_DR [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 DRT (ZMod 2))) : ZMod 2

The per-cocycle obstruction.

Equations

• GQ2.obsFun_DR htriv φ = ⋯.some.obs

theorem GQ2.obsFun_DR_eq [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) (φ : ↥(ContCoh.Z2 DRT (ZMod 2))) (F : DRLevelFactor (normalizeCochain ↑φ)) : obsFun_DR htriv φ = F.obs

obsFun_DR may be computed at any factorization of the normalization.

theorem GQ2.obsFun_DR_add [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) (φ ψ : ↥(ContCoh.Z2 DRT (ZMod 2))) : obsFun_DR htriv (φ + ψ) = obsFun_DR htriv φ + obsFun_DR htriv ψ

Additivity of the obstruction.

noncomputable def GQ2.obs_DR [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) : ↥(ContCoh.Z2 DRT (ZMod 2)) →+ ZMod 2

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

Equations

• GQ2.obs_DR htriv = AddMonoidHom.mk' (GQ2.obsFun_DR htriv) ⋯

The obstruction kills coboundaries

theorem GQ2.obs_DR_B2_eq_zero [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) : (ContCoh.B2 DRT (ZMod 2)).addSubgroupOf (ContCoh.Z2 DRT (ZMod 2)) ≤ (obs_DR htriv).ker

obs kills B². A continuous coboundary normalizes to δ¹ψ' (ψ' 1 = 0), which factors as coboundaryCocycle λ; its obstruction is λ (drWord (s,x,y)) = λ 1 = 0 (the relation dies at the level).

The injectivity keystone: obs = 0 ⟹ coboundary (via a drLiftHom section)

theorem GQ2.cocycle_mem_B2_DR [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) {V : OpenNormalSubgroup DRT} {c : DRCoh.TwoCocycle (DRT ⧸ ↑V.toOpenSubgroup)} (sect : ↑DR.toProfinite.toTop →ₜ* DRCoh.CentExt c) : (fun (p : DRT × DRT) => c.κ (sect p.1).base (sect p.2).base) ∈ ContCoh.B2 DRT (ZMod 2)

Coboundary extraction. A continuous hom sect : D_R → CentExt c splitting the level projection ((sect g).base = mk_V g) makes the level cocycle a continuous coboundary δ¹ (fib ∘ sect).

theorem GQ2.obs_DR_ker_le [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) : (obs_DR htriv).ker ≤ (ContCoh.B2 DRT (ZMod 2)).addSubgroupOf (ContCoh.Z2 DRT (ZMod 2))

Injectivity keystone. A continuous 2-cocycle with obs = 0 is a continuous coboundary: the relator dies exactly at the factoring level, so drLiftHom builds a splitting section and the level cocycle is δ¹ (fib ∘ section).

Assembly: the descended obstruction and its injectivity

noncomputable def GQ2.obsH2_DR [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) : ContCoh.H2 DRT (ZMod 2) →+ ZMod 2

The descended obstruction H²(D_R, 𝔽₂) →+ 𝔽₂.

Equations

• GQ2.obsH2_DR htriv = QuotientAddGroup.lift ((GQ2.ContCoh.B2 GQ2.DRT (ZMod 2)).addSubgroupOf (GQ2.ContCoh.Z2 GQ2.DRT (ZMod 2))) (GQ2.obs_DR htriv) ⋯

theorem GQ2.obsH2_DR_injective [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) : Function.Injective ⇑(obsH2_DR htriv)

obsH2_DR is injective — the #H² ≤ 2 half.

The factoring bridge: computing obsH2_DR at any finite quotient

theorem GQ2.obsH2_DR_eq_of_factor [DistribMulAction DRT (ZMod 2)] (htriv : ∀ (x : DRT) (m : ZMod 2), x • m = m) {L : Type} [Group L] [Finite L] (φ : ↥(ContCoh.Z2 DRT (ZMod 2))) (ρ : DRT →* L) (c : DRCoh.TwoCocycle L) (hfact : ∀ (g h : DRT), ↑φ (g, h) = c.κ (ρ g) (ρ h)) : (obsH2_DR htriv) ((ContCoh.H2mk DRT (ZMod 2)) φ) = drRelZ (fun (k : Fin 3) => ρ (drGens k)) c

The obstruction at an explicit factoring. For a continuous 2-cocycle φ factoring through a finite quotient L as φ (g, h) = c.κ (ρ g) (ρ h), the obstruction is the single-relator obstruction drRelZ (ρ ∘ (s, x, y)) c — the hook the Gram matrix of GQ2/Roe/DRH2.lean consumes.