The Γ_R degree-≤1 presentation comparison #
The Roe-candidate twin of GQ2/WordCohBridge.lean: for a finite discrete C-module A and a
continuous surjection q : Γ_R ↠ C, the continuous H¹ of Γ_R (with A a Γ_R-module through
q) is computed by the Roe word complex Z1wR/H1wR (GQ2/Roe/FoxBasic.lean) of the pushed
marking t_q = markC_R q:
z1EquivR : ContCoh.Z1 Γ_R A ≃+ Z1wR (markC_R q) (evaluation at the four marked generators),
descending to h1EquivR : ContCoh.H1 Γ_R A ≃+ H1wR (markC_R q). This is the substrate the whole
Γ_R supply lane (tickets R31c–R31g) is stated against — the Γ_R replacement for B6/Tate duality,
through which the word-complex self-duality prop_5_15_R transports to H¹(Γ_R).
What is new and what is inherited. The entire argument is relator-agnostic except one step:
the wild relator of Γ_R is r_R = (x₀^σ)⁻¹ · a · x₁² · c (note eq. (1.2) ⟦eq:relators⟧,
Marking.wildValueR), not Γ_A's r_A, so the two "wild relator dies" lemmas
(liftMarking_evalR_wildRelR, liftMarking_Z1wR_wildRelR) are re-derived from
wildRelatorR_mem_NR (GQ2/Roe/AdmissibleLimit.lean) and Marking.map_wildRelatorR_eq_one_iff
(GQ2/Roe/GammaR.lean). Everything genuinely word-independent is imported from the Γ_A file
and reused verbatim, never re-defined: the base projection WordCohBridge.gHom/gHomC, the
elementary-2 kernel WordCohBridge.isPGroup_gHom_ker, the Pro2Core crux
WordCohBridge.isPGroup_liftMarking_wildCore, and WordCohBridge.liftMarking_map_gHom — together
with the discrete WordLift topology instances registered there. Likewise markC_R /
markC_admissible_R are consumed from GQ2/Roe/Prop23.lean, not re-proved.
Level. As on the Γ_A side, this file is built over the raw quotient
GR := FreeProfiniteGroup (Fin 4) ⧸ N_R (defeq to the bundled GammaR,
RStageGammaR.gammaR_eq_quotient), because all the marking machinery
(quotientMk/quotientLift/Marking.pushR/Marking.descendR) lives over the raw quotient and
q.comp (quotientMk NR) must unify.
The spine: a continuous crossed cocycle z : GR → A (for the q-conjugation action) is exactly the
.u-component of a continuous hom φ_z : GR → WordLift A C = A ⋊ C lifting q
((φ_z γ).g = q γ).
Evaluating φ_z at the generators lands in Z1wR because both Γ_R relators die in GR;
conversely a Roe word cocycle x ∈ Z1wR gives an R-admissible marking of WordLift, which
descends to the hom, whose .u-component is the cocycle.
The raw quotient Γ_R = F₄ ⧸ N_R (defeq to GammaR by RStageGammaR.gammaR_eq_quotient, but
with the QuotientGroup instances the marking machinery is stated against).
Equations
- GQ2.WordCohBridgeR.GR = (↑(GQ2.FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ GQ2.NR)
Instances For
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. Word-independent — the verbatim Γ_R retyping of WordCohBridge.wordHom.
Equations
- GQ2.WordCohBridgeR.wordHomR q hcompat z = { toFun := fun (γ : GQ2.WordCohBridgeR.GR) => { u := ↑z γ, g := q γ }, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }
Instances For
The canonical marking of Γ_R #
Only the four scalars gammaSigmaR/gammaTauR/gammaX0R/gammaX1R exist (GQ2/Roe/Tame.lean);
gammaGenR bundles them into a Marking GR, which is the form evalR and the L4/L5 cover-lift
kernel (ticket R31e) consume.
The canonical marking of Γ_R by the images of the four free generators — the Γ_R twin of
WordCohBridge.gammaGen, and the bundled form of gammaSigmaR/gammaTauR/gammaX0R/gammaX1R
(GQ2/Roe/Tame.lean).
Equations
- GQ2.WordCohBridgeR.gammaGenR = GQ2.Marking.map (GQ2.quotientMk GQ2.NR).toMonoidHom GQ2.univMarking
Instances For
Sanity 1/4. gammaGenR.σ is the banked scalar gammaSigmaR.
Sanity 2/4. gammaGenR.τ is the banked scalar gammaTauR.
Sanity 3/4. gammaGenR.x₀ is the banked scalar gammaX0R.
Sanity 4/4. gammaGenR.x₁ is the banked scalar gammaX1R.
t_q = q ∘ (canonical Γ_R-marking) on each generator (the Marking.map_map collapse) — the
Γ_R twin of WordCohBridge.markC_map.
Evaluation of a continuous crossed cocycle at the four marked generators of Γ_R.
Equations
Instances For
The lifted marking at evalR z is the pushforward of wordHomR along the canonical marking —
the identity underlying "evalR lands in Z1wR".
The lifted marking at evalR z, rewritten as the pushforward of the universal marking along
φ_z ∘ quotientMk : F₄ → WordLift — the form the relator-death lemmas consume.
The tame relation holds for the lifted marking at evalR z (the tame relator — shared with
Γ_A — dies in Γ_R, tameRelator_mem_NR).
The one genuinely new ingredient. The Roe wild relation holds for the lifted marking at
evalR z: the Roe wild relator word r_R dies in Γ_R (wildRelatorR_mem_NR,
GQ2/Roe/AdmissibleLimit.lean), and dying profinitely is the same as WildRelR of the pushed
marking (Marking.map_wildRelatorR_eq_one_iff, GQ2/Roe/GammaR.lean). This is the sole place
where the Γ_A proof of WordCohBridge.liftMarking_eval_wildRel does not transfer.
Forward: evalR lands in Z1wR. The evaluation of a continuous crossed cocycle at the four
generators is a Roe word cocycle, because both Γ_R relators die in Γ_R.
evalR is additive (it is pointwise evaluation of the additive z.1).
The forward map Z1(Γ_R, A) →+ Z1wR t_q (evaluation at the four marked generators), bundled
additively.
Equations
- GQ2.WordCohBridgeR.toZ1wRHom q hcompat = AddMonoidHom.mk' (fun (z : ↥(GQ2.ContCoh.Z1 GQ2.WordCohBridgeR.GR A)) => ⟨GQ2.WordCohBridgeR.evalR z, ⋯⟩) ⋯
Instances For
The backward direction #
WordCohBridge.gHom (the base projection WordLift A C →* C), isPGroup_gHom_ker,
isPGroup_liftMarking_wildCore (the Pro2Core crux) and liftMarking_map_gHom are all
relator-independent, so they are imported and reused, not cloned.
For a Roe word cocycle x ∈ Z1wR, the lifted marking satisfies the tame relation: the .u-slot
dies because x is a cocycle, the .g-slot because t_q is R-admissible.
For a Roe word cocycle x ∈ Z1wR, the lifted marking satisfies the Roe wild relation — the
Z1wR-side twin of WordCohBridge.liftMarking_Z1w_wildRel, re-derived at Marking.wildValueR
(naturality Marking.map_wildValueR, GQ2/Roe/Words.lean) and markC_admissible_R's .2.2.1
clause (which is WildRelR, pinned by markC_admissible_R_clauses).
Backward, gateway step. For a Roe word cocycle x ∈ Z1wR t_q, the classified lift
c := classify (liftMarking t_q x) : F₄ →ₜ* WordLift A C kills N_R. Its kernel is an
R-admissible open: Generates is automatic (generates_univMarking_map), both Γ_R relators die
(x is a cocycle ⇒ .u-slot dies, t_q R-admissible ⇒ .g-slot dies), and the wild core is
pro-2 by the reused WordCohBridge.isPGroup_liftMarking_wildCore (transferred into F₄ ⧸ ker c
along the injective kerLift c), using that A is elementary-2. Γ_R twin of
WordCohBridge.NA_le_ker_classify, with IsAdmissibleU/isAdmissibleU_iff_NA_le swapped for
IsAdmissibleUR/isAdmissibleUR_iff_NR_le.
The descended WordLift-valued hom of a Roe word cocycle:
Marking.classify (liftMarking t_q x) pushed through Γ_R = F₄ ⧸ N_R (legitimate by
NR_le_ker_classify_R).
Equations
- GQ2.WordCohBridgeR.liftHomR q hq hA₂ x = GQ2.quotientLift GQ2.NR (GQ2.FoxH.liftMarking (GQ2.markC_R q) ↑x).classify ⋯
Instances For
The descended hom lifts q on the base coordinate: (liftHomR x γ).g = q γ. (Both
gHomC ∘ liftHomR and q are the descent of the same F₄ → C hom, since projecting the lifted
marking recovers t_q — the reused WordCohBridge.liftMarking_map_gHom.)
Backward map Z1wR t_q → Z1(Γ_R, A): take the .u-component of the descended hom.
Continuity is WordLift.u ∘ liftHomR; the cocycle identity is the WordLift product law on .u,
using (liftHomR x γ).g = q γ (liftHomR_g) and the compatibility of the two actions.
Equations
- GQ2.WordCohBridgeR.ofZ1wR q hcompat hq hA₂ x = ⟨fun (γ : GQ2.WordCohBridgeR.GR) => ((GQ2.WordCohBridgeR.liftHomR q hq hA₂ x) γ).u, ⋯⟩
Instances For
The equivalence #
Right inverse (toZ1wRHom ∘ ofZ1wR = id on Z1wR). Evaluating the descended hom at the
four generators returns x.
Left inverse (ofZ1wR ∘ toZ1wRHom = id on Z1). The descended hom of evalR z is
wordHomR z: both equal (wordHomR z).comp (quotientMk N_R) after quotientMk (by
liftMarking_evalR_univ + Marking.toHom_hom_univMarking_map), so their .u-slots agree.
The degree-1 comparison for Γ_R: continuous crossed cocycles of Γ_R valued in the
elementary-2 module A are exactly the Roe word cocycles of the pushed marking
t_q = markC_R q, via evaluation at the four marked generators. Binder shape mirrors
WordCohBridge.z1Equiv exactly, so downstream Nat.card_congr (z1EquivR θ hcomp hθs hA₂).toEquiv
calls read verbatim as on the Γ_A side.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Smoke test (z1EquivR round trip). The bundled equivalence really is evalR in the
forward direction and inverts it.
Degree-0 compatibility. Evaluation carries a Γ_R-coboundary dZero m to the
word-coboundary d0 t_q m: on each generator gammaGenR.slot • m = t_q.slot • m, since q
intertwines the two actions (hcompat) and q gammaGenR.slot = t_q.slot by construction. (d⁰
does not see the relator, so this is word-independent — but it is stated at markC_R.)
The degree-1 comparison in cohomology for Γ_R: H¹(Γ_R, A) ≃+ H¹_{R,word}(t_q), obtained
by descending z1EquivR through the coboundary correspondence B¹ ↔ B¹_word (eval_dZeroR;
B1wR = B1w, the relator does not enter d⁰). Binder shape mirrors WordCohBridge.h1Equiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Smoke test (h1EquivR round trip). The H¹-level equivalence is the descent of
z1EquivR: it sends the class of z to the class of evalR z, and inverts.
Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained) #
- eq. (1.2) = ⟦eq:relators⟧ — the Roe wild relator whose death in
Γ_Ris the sole new ingredient (liftMarking_evalR_wildRelR,liftMarking_Z1wR_wildRelR). - Definition 1.1 = ⟦def:GammaR⟧ —
IsAdmissibleUR/N_R, viaNR_le_ker_classify_R.