The Γ_A degree-≤1 presentation comparison

For a finite discrete C-module A and a continuous surjection q : Γ_A ↠ C, the continuous H¹ of Γ_A (with A a Γ_A-module through q) is computed by the Fox–Heisenberg word complex Z1w/H1w of the pushed marking t_q = Marking.push q:

z1Equiv : ContCoh.Z1 Γ_A A ≃+ Z1w t_q (evaluation at the four marked generators),

descending to h1Equiv : ContCoh.H1 Γ_A A ≃+ H1w t_q. This is the Γ_A-side replacement for B6/Tate duality that the Γ_A half-torsor proof (lemma_8_6_gammaA) needs — the word-complex self-duality prop_5_15 then transports to H¹(Γ_A). Reusable beyond §8 (the degree-1 half of the presentation comparison, wanted again for Theorem 4.2).

Level. Γ_A = GammaA = ProfiniteGrp.of (F₄ ⧸ N_A) re-wraps the raw quotient with fresh (defeq-but-not-syntactic) group/topology instances, whereas all the marking machinery (quotientMk/quotientLift/Marking.push/Marking.descend) lives over the raw FreeProfiniteGroup (Fin 4) ⧸ N_A. To keep q.comp (quotientMk NA) unifying, this file is built over the raw quotient GA := FreeProfiniteGroup (Fin 4) ⧸ N_A; the carrier is defeq to GammaA, so the results transport to the GammaA statement (z1EquivGammaA at the end).

The spine: a continuous crossed cocycle z : GA → A (for the q-conjugation action) is exactly the .u-component of a continuous hom φ_z : GA → WordLift A C = A ⋊ C lifting q ((φ_z γ).g = q γ). Evaluating φ_z at the generators lands in Z1w because the relators die in GA; conversely a word cocycle x ∈ Z1w gives an admissible marking of WordLift, which Marking.descends to the hom, whose .u-component is the cocycle (ker_char_NA_le_iff pattern: Generates is automatic for a quotient of F₄).

@[reducible, inline]

abbrev GQ2.WordCohBridge.GA : Type

The raw quotient Γ_A = F₄ ⧸ N_A (defeq to GammaA, but with the QuotientGroup instances the marking machinery is stated against).

Equations

• GQ2.WordCohBridge.GA = (↑(GQ2.FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ GQ2.NA)

@[implicit_reducible]

instance GQ2.WordCohBridge.instTopologicalSpaceWordLift {C A : Type} : TopologicalSpace (FoxH.WordLift A C)

The (discrete) topology on WordLift A C making it a valid codomain for continuous homs.

Equations

• GQ2.WordCohBridge.instTopologicalSpaceWordLift = ⊥

instance GQ2.WordCohBridge.instDiscreteTopologyWordLift {C A : Type} : DiscreteTopology (FoxH.WordLift A C)

noncomputable def GQ2.WordCohBridge.wordHom {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (z : ↥(ContCoh.Z1 GA A)) : GA →ₜ* FoxH.WordLift A C

The WordLift A C = A ⋊ C hom γ ↦ ⟨z γ, q γ⟩ attached to a continuous crossed cocycle z. The cocycle identity z(γδ) = z γ + q γ • z δ is exactly the WordLift product law on the .u-slot.

Equations

• GQ2.WordCohBridge.wordHom q hcompat z = { toFun := fun (γ : GQ2.WordCohBridge.GA) => { u := ↑z γ, g := q γ }, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

noncomputable def GQ2.WordCohBridge.gammaGen : Marking GA

The canonical marking of Γ_A by the images of the four free generators.

Equations

• GQ2.WordCohBridge.gammaGen = GQ2.Marking.map (GQ2.quotientMk GQ2.NA).toMonoidHom GQ2.univMarking

noncomputable def GQ2.WordCohBridge.markC {C : Type} [Group C] [TopologicalSpace C] (q : GA →ₜ* C) : Marking C

The pushed marking t_q : Marking C of the surjection q — the marking against which the word complex Z1w/H1w is formed.

Equations

• GQ2.WordCohBridge.markC q = GQ2.Marking.push q

theorem GQ2.WordCohBridge.markC_admissible {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] (q : GA →ₜ* C) (hq : Function.Surjective ⇑q) : (markC q).Admissible

theorem GQ2.WordCohBridge.markC_map {C : Type} [Group C] [TopologicalSpace C] (q : GA →ₜ* C) : markC q = Marking.map q.toMonoidHom gammaGen

t_q = q ∘ (canonical Γ_A-marking) on each generator (the Marking.map_map collapse).

noncomputable def GQ2.WordCohBridge.eval {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction GA A] (z : ↥(ContCoh.Z1 GA A)) : Fin 4 → A

Evaluation of a continuous crossed cocycle at the four marked generators of Γ_A.

Equations

• GQ2.WordCohBridge.eval z = ![↑z GQ2.WordCohBridge.gammaGen.σ, ↑z GQ2.WordCohBridge.gammaGen.τ, ↑z GQ2.WordCohBridge.gammaGen.x₀, ↑z GQ2.WordCohBridge.gammaGen.x₁]

theorem GQ2.WordCohBridge.liftMarking_eval {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (z : ↥(ContCoh.Z1 GA A)) : FoxH.liftMarking (markC q) (eval z) = Marking.map (wordHom q hcompat z).toMonoidHom gammaGen

The lifted marking at eval z is the pushforward of wordHom along the canonical marking — the identity underlying "eval lands in Z1w".

theorem GQ2.WordCohBridge.liftMarking_eval_univ {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (z : ↥(ContCoh.Z1 GA A)) : FoxH.liftMarking (markC q) (eval z) = Marking.map ((wordHom q hcompat z).comp (quotientMk NA)).toMonoidHom univMarking

The lifted marking at eval z, rewritten as the pushforward of the universal marking along φ_z ∘ quotientMk : F₄ → WordLift — the form the relator-death lemmas consume.

theorem GQ2.WordCohBridge.liftMarking_eval_tameRel {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (z : ↥(ContCoh.Z1 GA A)) : (FoxH.liftMarking (markC q) (eval z)).TameRel

The tame relation holds for the lifted marking at eval z (the tame relator dies in Γ_A).

theorem GQ2.WordCohBridge.liftMarking_eval_wildRel {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (z : ↥(ContCoh.Z1 GA A)) : (FoxH.liftMarking (markC q) (eval z)).WildRel

The wild relation holds for the lifted marking at eval z (the wild relator dies in Γ_A).

theorem GQ2.WordCohBridge.eval_mem_Z1w {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (z : ↥(ContCoh.Z1 GA A)) : eval z ∈ FoxH.Z1w (markC q)

Forward: eval lands in Z1w. The evaluation of a continuous crossed cocycle at the four generators is a word cocycle, because both relators die in Γ_A.

theorem GQ2.WordCohBridge.eval_add {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction GA A] (z z' : ↥(ContCoh.Z1 GA A)) : eval (z + z') = eval z + eval z'

eval is additive (it is pointwise evaluation of the additive z.1).

noncomputable def GQ2.WordCohBridge.toZ1wHom {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) : ↥(ContCoh.Z1 GA A) →+ ↥(FoxH.Z1w (markC q))

The forward map Z1(Γ_A, A) →+ Z1w t_q (evaluation at the four marked generators), bundled additively.

Equations

• GQ2.WordCohBridge.toZ1wHom q hcompat = AddMonoidHom.mk' (fun (z : ↥(GQ2.ContCoh.Z1 GQ2.WordCohBridge.GA A)) => ⟨GQ2.WordCohBridge.eval z, ⋯⟩) ⋯

@[simp]

theorem GQ2.WordCohBridge.toZ1wHom_coe {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (z : ↥(ContCoh.Z1 GA A)) : ↑((toZ1wHom q hcompat) z) = eval z

The Pro2Core crux: the wild core of a lifted marking is pro-2.

def GQ2.WordCohBridge.gHom {C : Type} [Group C] {A : Type} [AddCommGroup A] [DistribMulAction C A] : FoxH.WordLift A C →* C

The base projection WordLift A C →* C (the .g component).

Equations

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

def GQ2.WordCohBridge.gHomC {C : Type} [Group C] [TopologicalSpace C] {A : Type} [AddCommGroup A] [DistribMulAction C A] : FoxH.WordLift A C →ₜ* C

The base projection as a continuous hom (WordLift is discrete).

Equations

• GQ2.WordCohBridge.gHomC = { toMonoidHom := GQ2.WordCohBridge.gHom, continuous_toFun := ⋯ }

theorem GQ2.WordCohBridge.isPGroup_gHom_ker {C : Type} [Group C] {A : Type} [AddCommGroup A] [DistribMulAction C A] (hA₂ : ∀ (a : A), a + a = 0) : IsPGroup 2 ↥gHom.ker

The kernel of the base projection is elementary-2 (it is A with g = 1).

theorem GQ2.WordCohBridge.isPGroup_liftMarking_wildCore {C : Type} [Group C] {A : Type} [AddCommGroup A] [DistribMulAction C A] (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht2 : IsPGroup 2 ↥(Subgroup.normalClosure {t.x₀, t.x₁})) (x : Fin 4 → A) : IsPGroup 2 ↥(Subgroup.normalClosure {(FoxH.liftMarking t x).x₀, (FoxH.liftMarking t x).x₁})

The Pro2Core crux: the wild core ⟪(x₂,t.x₀), (x₃,t.x₁)⟫ of a lifted marking is a 2-group — an extension of the (pro-2, t.Pro2Core) base wild core by the elementary-2 A. Proved with IsPGroup.comap_of_ker_isPGroup: the core is ≤ gHom⁻¹(base core).

theorem GQ2.WordCohBridge.liftMarking_map_gHom {C : Type} [Group C] {A : Type} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) (x : Fin 4 → A) : Marking.map gHom (FoxH.liftMarking t x) = t

Projecting a lifted marking back through gHom recovers the base marking.

theorem GQ2.WordCohBridge.liftMarking_Z1w_tameRel {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [Finite A] [DistribMulAction C A] (q : GA →ₜ* C) (hq : Function.Surjective ⇑q) (x : ↥(FoxH.Z1w (markC q))) : (FoxH.liftMarking (markC q) ↑x).TameRel

For a word cocycle x ∈ Z1w, the lifted marking satisfies the tame relation: the .u-slot dies because x is a cocycle, the .g-slot because t_q is admissible.

theorem GQ2.WordCohBridge.liftMarking_Z1w_wildRel {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [Finite A] [DistribMulAction C A] (q : GA →ₜ* C) (hq : Function.Surjective ⇑q) (x : ↥(FoxH.Z1w (markC q))) : (FoxH.liftMarking (markC q) ↑x).WildRel

For a word cocycle x ∈ Z1w, the lifted marking satisfies the wild relation.

theorem GQ2.WordCohBridge.NA_le_ker_classify {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [Finite A] [DistribMulAction C A] (q : GA →ₜ* C) (hq : Function.Surjective ⇑q) (hA₂ : ∀ (a : A), a + a = 0) (x : ↥(FoxH.Z1w (markC q))) : NA ≤ (FoxH.liftMarking (markC q) ↑x).classify.ker

Backward, gateway step. For a word cocycle x ∈ Z1w t_q, the classified lift c := classify (liftMarking t_q x) : F₄ →ₜ* WordLift A C kills N_A. Its kernel is an admissible open: Generates is automatic (generates_univMarking_map), both relators die (x is a cocycle ⇒ .u-slot dies, t_q admissible ⇒ .g-slot dies), and the wild core is pro-2 by isPGroup_liftMarking_wildCore (transferred into F₄ ⧸ ker c along the injective kerLift c), using that A is elementary-2.

noncomputable def GQ2.WordCohBridge.liftHom {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [Finite A] [DistribMulAction C A] (q : GA →ₜ* C) (hq : Function.Surjective ⇑q) (hA₂ : ∀ (a : A), a + a = 0) (x : ↥(FoxH.Z1w (markC q))) : GA →ₜ* FoxH.WordLift A C

The descended WordLift-valued hom of a word cocycle: Marking.classify (liftMarking t_q x) pushed through Γ_A = F₄ ⧸ N_A (legitimate by NA_le_ker_classify).

Equations

• GQ2.WordCohBridge.liftHom q hq hA₂ x = GQ2.quotientLift GQ2.NA (GQ2.FoxH.liftMarking (GQ2.WordCohBridge.markC q) ↑x).classify ⋯

theorem GQ2.WordCohBridge.liftHom_g {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [Finite A] [DistribMulAction C A] (q : GA →ₜ* C) (hq : Function.Surjective ⇑q) (hA₂ : ∀ (a : A), a + a = 0) (x : ↥(FoxH.Z1w (markC q))) (γ : GA) : ((liftHom q hq hA₂ x) γ).g = q γ

The descended hom lifts q on the base coordinate: (liftHom x γ).g = q γ. (Both gHomC ∘ liftHom and q are the descent of the same F₄ → C hom, since projecting the lifted marking recovers t_q — liftMarking_map_gHom.)

noncomputable def GQ2.WordCohBridge.ofZ1w {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (hq : Function.Surjective ⇑q) (hA₂ : ∀ (a : A), a + a = 0) (x : ↥(FoxH.Z1w (markC q))) : ↥(ContCoh.Z1 GA A)

Backward map Z1w t_q → Z1(Γ_A, A): take the .u-component of the descended hom. Continuity is WordLift.u ∘ liftHom; the cocycle identity is the WordLift product law on .u, using (liftHom x γ).g = q γ (liftHom_g) and the compatibility of the two actions.

Equations

• GQ2.WordCohBridge.ofZ1w q hcompat hq hA₂ x = ⟨fun (γ : GQ2.WordCohBridge.GA) => ((GQ2.WordCohBridge.liftHom q hq hA₂ x) γ).u, ⋯⟩

The equivalence

The forward map toZ1wHom and backward map ofZ1w are complete and verified below, together with both round trips and the additive equivalence z1Equiv. Neither round trip needs the topological generation of Γ_A: both factor through quotientMk surjectivity and the univMarking.map uniqueness Marking.toHom_hom_univMarking_map. The H¹ corollary h1Equiv descends z1Equiv through B1 ↔ B1w (degree-0 half of the comparison) — the next sub-step.

theorem GQ2.WordCohBridge.toZ1wHom_ofZ1w {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (hq : Function.Surjective ⇑q) (hA₂ : ∀ (a : A), a + a = 0) (x : ↥(FoxH.Z1w (markC q))) : (toZ1wHom q hcompat) (ofZ1w q hcompat hq hA₂ x) = x

Right inverse (toZ1wHom ∘ ofZ1w = id on Z1w). Evaluating the descended hom at the four generators returns x: (liftHom x (quotientMk N_A (univMarking.slot))).u = (Marking.classify (liftMarking t_q x) (univMarking.slot)).u = ((liftMarking t_q x).slot).u = x.slot.

theorem GQ2.WordCohBridge.ofZ1w_toZ1wHom {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (hq : Function.Surjective ⇑q) (hA₂ : ∀ (a : A), a + a = 0) (z : ↥(ContCoh.Z1 GA A)) : ofZ1w q hcompat hq hA₂ ((toZ1wHom q hcompat) z) = z

Left inverse (ofZ1w ∘ toZ1wHom = id on Z1). The descended hom of eval z is wordHom z: both equal (wordHom z).comp (quotientMk N_A) after quotientMk (by liftMarking_eval_univ + Marking.toHom_hom_univMarking_map), so their .u-slots agree.

noncomputable def GQ2.WordCohBridge.z1Equiv {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (hq : Function.Surjective ⇑q) (hA₂ : ∀ (a : A), a + a = 0) : ↥(ContCoh.Z1 GA A) ≃+ ↥(FoxH.Z1w (markC q))

The degree-1 comparison (the Γ_A half-torsor proof): continuous crossed cocycles of Γ_A valued in the elementary-2 module A are exactly the Fox–Heisenberg word cocycles of the pushed marking t_q = Marking.push q, via evaluation at the four marked generators.

Equations

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

theorem GQ2.WordCohBridge.eval_dZero {C : Type} [Group C] [TopologicalSpace C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction C A] [DistribMulAction GA A] [ContinuousSMul GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (m : A) : eval ⟨(ContCoh.dZero GA A) m, ⋯⟩ = (FoxH.d0 (markC q)) m

Degree-0 compatibility. Evaluation carries a Γ_A-coboundary dZero m to the word-coboundary d0 t_q m: on each generator gammaGen.slot • m = t_q.slot • m, since q intertwines the two actions (hcompat) and q gammaGen.slot = t_q.slot by construction.

noncomputable def GQ2.WordCohBridge.h1Equiv {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] {A : Type} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [Finite A] [DistribMulAction C A] [DistribMulAction GA A] [ContinuousSMul GA A] (q : GA →ₜ* C) (hcompat : ∀ (γ : GA) (a : A), γ • a = q γ • a) (hq : Function.Surjective ⇑q) (hA₂ : ∀ (a : A), a + a = 0) : ContCoh.H1 GA A ≃+ FoxH.H1w (markC q)

The degree-1 comparison in cohomology (the Γ_A half-torsor proof): H¹(Γ_A, A) ≃+ H¹_word(t_q), obtained by descending z1Equiv through the coboundary correspondence B¹ ↔ B¹_word (eval_dZero).

Equations

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

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

• Theorem 4.2 = ⟦thm-fixedframe⟧