Documentation

GQ2.HalfTorsorGammaA

The nonzero variation class over Γ_A #

Assembling the ledger identity with the prop_5_15 self-duality: from NoDescent, there is a crossed T-cocycle u whose variation class [varCoc u] ∈ H²(Γ_A, 𝔽₂) is nonzero. This is the hvar input to the abstract half-torsor count CentralObstruction.n (the Γ_A half-torsor proof).

theorem GQ2.SectionEight.LedgerGammaA.exists_nonzero_varCoc_gammaA {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : CentralObstruction.TComplement D) (hedge : D.NoDescent) (ρ : WordCohBridge.GA →ₜ* Bg D.M) ( : Function.Surjective ρ) [DistribMulAction WordCohBridge.GA (ZMod 2)] [ContinuousSMul WordCohBridge.GA (ZMod 2)] (htriv : ∀ (x : WordCohBridge.GA) (m : ZMod 2), x m = m) :
∃ (u : CentralObstruction.TCocycle D ρ), (ContCoh.H2mk WordCohBridge.GA (ZMod 2)) CentralObstruction.varCoc D ρ S u, 0

The nonzero variation class over Γ_A (the Γ_A half-torsor proof). For a lower epimorphism ρ : Γ_A ↠ B/M with nonzero radical edge (NoDescent), there is a crossed T-cocycle u whose variation class is a nonzero element of H²(Γ_A, 𝔽₂).

theorem GQ2.SectionEight.LedgerGammaA.card_H2_gammaA_eq_two {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) (S : CentralObstruction.TComplement D) (hedge : D.NoDescent) (ρ : WordCohBridge.GA →ₜ* Bg D.M) ( : Function.Surjective ρ) [DistribMulAction WordCohBridge.GA (ZMod 2)] [ContinuousSMul WordCohBridge.GA (ZMod 2)] (htriv : ∀ (x : WordCohBridge.GA) (m : ZMod 2), x m = m) :
Nat.card (ContCoh.H2 WordCohBridge.GA (ZMod 2)) = 2

#H²(Γ_A, 𝔽₂) = 2 (the Γ_A half-torsor proof hcard). The obstruction injection obsH2 : H² ↪ 𝔽₂ (c2) gives ≤ 2; the nonzero variation class makes it surjective, hence a bijection.

theorem GQ2.SectionEight.LedgerGammaA.half_torsor_gammaA {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) (hedge : D.NoDescent) (ρ : GammaA.toProfinite.toTop →ₜ* Bg D.M) ( : Function.Surjective ρ) :
2 * Nat.card { f : MLifts D ρ // MLifts.Central D f } = Nat.card (MLifts D ρ)

Lemma 8.6, Γ_A source (the Γ_A half-torsor proof): with a nonzero radical edge, exactly half of the unrestricted M-lifts of a lower epimorphism ρ : Γ_A ↠ B/M satisfy the central relation. The abstract half-count CentralObstruction.half_count fed by the nonzero variation class (exists_nonzero_varCoc_gammaA) and #H² = 2 (card_H2_gammaA_eq_two); the counted lift set is finite because Γ_A is topologically finitely generated.

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