The crossed V-cocycle layer #
The V-side mirror of CentralObstruction.TCocycle, and the semidirect bijection it powers.
In the zero-edge regime descended_splitting (AffineTLift.lean:503) presents Q = Bg/T as a
split extension 1 → V → Q → C₀ → 1 (B/T ≅ V ⋊ C₀), so the continuous homomorphisms
Γ → Q over a fixed lower map ρ' : Γ → C₀ are exactly the continuous crossed V-cocycles
Z¹_{Γ,ρ}(V). This file builds:
rho0— theC₀-valued lower mapΓ → C₀induced byρ : Γ → Bg/M(throughpiC₀);VCocycle— a continuous crossed1-cocycleΓ → Voverρ, mirroringTCocycle, with itsAddCommGroupstructure;vCob— the principal-coboundary mapV → Z¹,v ↦ (γ ↦ ρ'(γ)·v − v), anAddMonoidHom, andvCob_eq_zero_iff(its kernel is theρ'-fixed vectors — freeness whenV^C = 0);vcocycleEquivLifts— the bijectionVCocycle ≃ {g : Γ →ₜ Q // piQbar ∘ g = ρ'}via a splittingσofpiQbar;- the
B¹-translation facts — conjugating anM-liftfbym ∈ Mkeeps it over the sameρ(mConj), preservesCentral(mConj_central), and translates itsT-reductionredT fby the coboundaryvCob (descend m)(cocycleOf_mConj). This is the group-theoretic core of the Bug-1 recalibration (docs/orchestration/p16d6c-handoff.md§⚠): the centralred_T-image is a freeB¹ = V-torsor bundle, so its cardinality carries the missing|B¹| = #Vfactor (c1s), whose arithmetic close is c1c.
Since DescData's V/C₀ are opaque finite types (no topology), continuity of a V-cochain
c : Γ → V is stored through its embedding iV ∘ ofAdd into the discrete Q = Bg/T, and the
σ ∘ ρ' continuity factors through the discrete Bg/M. Everything is source-generic
(RadicalCoverData + DescData), finite-group / generic-Γ; no B6/B7, all std-3.
The quotient Bg ⧸ D.T of the discrete group Bg is discrete (mirror of
CentralObstruction.discreteTopology_quotient).
piC₀ descends through M = ker piC₀ to a map Bg/M → C₀.
Equations
- GQ2.SectionEight.AffineTLift.liftC0 DD = QuotientGroup.lift D.M DD.piC0 ⋯
Instances For
The C₀-valued lower map ρ' : Γ → C₀, the descent of ρ : Γ → Bg/M through piC₀.
Equations
- GQ2.SectionEight.AffineTLift.rho0 DD ρ = (GQ2.SectionEight.AffineTLift.liftC0 DD).comp ρ.toMonoidHom
Instances For
ρ'(γ) = piC₀(b) for any representative b of ρ(γ).
A continuous crossed V-valued 1-cocycle over ρ (the paper's c ∈ Z¹_{Γ,ρ}(V)):
c(γδ) = c(γ) + ρ'(γ)·c(δ), with ρ' = rho0 the C₀-valued descent of ρ. The V-side
mirror of TCocycle (additive, valued directly in V = M/T). Continuity is stored through the
embedding iV ∘ ofAdd into the discrete Q = Bg/T, since V carries no topology.
- c : Γ → DD.Vmod
The underlying function, valued in
V.
Instances For
A crossed cocycle vanishes at 1.
The additive structure on Z¹ and the coboundary map #
Equations
- GQ2.SectionEight.AffineTLift.instZeroVCocycle = { zero := { c := fun (x : Γ) => 0, cont := ⋯, crossed := ⋯ } }
Equations
- GQ2.SectionEight.AffineTLift.instAddVCocycle = { add := fun (u w : GQ2.SectionEight.AffineTLift.VCocycle DD ρ) => { c := fun (γ : Γ) => u.c γ + w.c γ, cont := ⋯, crossed := ⋯ } }
The principal coboundary δv ∈ B¹_{Γ,ρ}(V) of a vector v : V: γ ↦ ρ'(γ)·v − v.
This is the mathematical core of the Bug-1 recalibration: conjugating an M-lift by a lift of
v translates its T-reduction cocycle by vCob v.
Equations
- GQ2.SectionEight.AffineTLift.vCob DD ρ v = { c := fun (γ : Γ) => (GQ2.SectionEight.AffineTLift.rho0 DD ρ) γ • v - v, cont := ⋯, crossed := ⋯ }
Instances For
vCob is additive: δ(v + w) = δv + δw.
Freeness criterion (V^C = 0 clause of Bug 1): the coboundary vCob v is the trivial
cocycle iff v is fixed by every ρ'(γ). When V has no nonzero im ρ'-fixed vector (e.g.
V^C = 0 with ρ' surjective), v ↦ vCob v is injective, so B¹ ≅ V.
Freeness of the B¹-translation (the V^C = 0 clause of Bug 1): if V carries no
nonzero ρ'-fixed vector (e.g. V^C = 0 with ρ' surjective), the coboundary map v ↦ vCob v
is injective — the V-action by B¹-translation is free, so B¹ ≅ V. This is what supplies the
missing |B¹| = #V factor of the c1s recalibration.
The semidirect bijection VCocycle ≃ {Γ →ₜ Q over ρ'} #
Via a splitting σ : C₀ → Q of piQbar (from descended_splitting), Q = Bg/T ≅ V ⋊ C₀, and a
continuous hom Γ → Q over ρ' decomposes as γ ↦ iV(c γ) · σ(ρ'γ) with c ∈ Z¹_{Γ,ρ}(V).
iV lands in ker piQbar.
Every q ∈ ker piQbar is iV(ofAdd v) for some v : V.
iV ∘ ofAdd is injective on V.
iV ∘ ofAdd sends + to *.
iV ∘ ofAdd sends negation to inversion.
Continuous homomorphisms Γ → Q = Bg/T lying over the lower map ρ' = rho0.
Equations
- GQ2.SectionEight.AffineTLift.QLiftsOver DD ρ = { g : Γ →ₜ* Bg ⧸ D.T // ∀ (γ : Γ), (GQ2.SectionEight.AffineTLift.piQbar DD) (g γ) = (GQ2.SectionEight.AffineTLift.rho0 DD ρ) γ }
Instances For
M-lift conjugation and T-reduction as a hom over ρ' #
The T-reduction of an M-lift, packaged as a hom Γ → Q = Bg/T over ρ'.
Equations
- GQ2.SectionEight.AffineTLift.redTLift DD f = ⟨{ toMonoidHom := MonoidHom.mk' (fun (γ : Γ) => ↑(↑f γ)) ⋯, continuous_toFun := ⋯ }, ⋯⟩
Instances For
Conjugation of an M-lift by m ∈ M: still an M-lift over the same ρ (since
mk_M m = 1).
Equations
- GQ2.SectionEight.AffineTLift.mConj m hm f = ⟨{ toMonoidHom := MonoidHom.mk' (fun (γ : Γ) => m * ↑f γ * m⁻¹) ⋯, continuous_toFun := ⋯ }, ⋯⟩
Instances For
Conjugation by m ∈ M preserves the central relation.
σ conjugates iV(ofAdd v) to iV(ofAdd (cc·v)) (the semidirect action via iV_conj).
The commutation form: σ(cc)·iV(v) = iV(cc·v)·σ(cc).
γ ↦ σ(ρ'γ) is continuous (it factors through the discrete Bg/M).
Forward map of the semidirect bijection: a crossed cocycle c gives the continuous hom
γ ↦ iV(c γ) · σ(ρ'γ) over ρ'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The V-coordinate of a hom g : Γ → Q over ρ' exists: g γ · σ(ρ'γ)⁻¹ ∈ ker piQbar.
Inverse map of the semidirect bijection: the V-coordinate cocycle of a hom g over
ρ', c γ := iV⁻¹(g γ · σ(ρ'γ)⁻¹).
Equations
- GQ2.SectionEight.AffineTLift.cocycleOfQ DD ρ σ hσ g = { c := fun (γ : Γ) => Classical.choose ⋯, cont := ⋯, crossed := ⋯ }
Instances For
The defining spec of cocycleOfQ: iV(c γ) = g γ · σ(ρ'γ)⁻¹.
The semidirect bijection Z¹_{Γ,ρ}(V) ≃ {Γ →ₜ Q over ρ'} (the Prop. 8.9 assembly): via a splitting
σ of piQbar, crossed V-cocycles are exactly the continuous homs Γ → Q = Bg/T lying over
the lower map ρ'. This is the paper's B/T ≅ V ⋊ C₀ presentation at the level of Γ-points.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Conjugation ↔ coboundary translation (the semidirect action, the algebraic heart of the
Bug-1 recalibration): conjugating the hom qOfCocycle c by iV(v) adds the principal coboundary
vCob v to its cocycle. V (via iV) acts on the fibre {Γ →ₜ Q over ρ'} by translation
through B¹.
The B¹-translation fact (the Prop. 8.9 assembly, the algebraic core of Bug 1): conjugating an
M-lift f by m ∈ M translates the V-cocycle of its T-reduction by the principal
coboundary vCob (descend m). Together with mConj_central this shows V (via descend) acts
on the central red_T-image by B¹-translation — free when V^C = 0 (vCob_c_eq_zero_iff), so
the image carries the missing |B¹| = #V factor (c1s).