Documentation

GQ2.RepIndependence

Representative independence of Q⁰_loc (Lemma 6.4 layer ⟹ Lemma 6.14) #

The base quadratic connecting map Q⁰_loc (GQ2/SectionSix.lean, eq. (92)) is defined on H¹-classes through the canonical cocycle representative Quotient.out. Its well-definedness — that H2ofFun (graphPullback dat ρ ·) is invariant under a cohomologous change of the Z¹ representative — is Lemma 6.4. We prove it (repIndep) by exhibiting the explicit conjugation coboundary (a 6.22-style char-2 cochain identity), then read off Lemma 6.14 (eq. (102), regular-module realization) via the on-the-nose comap identity + mapCoeff1 functoriality. Axioms: ∅ (std-3).

The SectionSix.lemma_6_14 statement is amended (documented) with the compatibility hypotheses its use of Q⁰_loc requires: hdatW (equivariant factor set on W), hiC (i is a C-module map — eq. (77)'s i ⋊ 1), and hρW (G_ℚ₂ acts on W through ρ).

source
theorem GQ2.RepIndependence.h2ofFun_eq_of_sub_mem_B2 {φ ψ : AbsGalQ2 × AbsGalQ2 → ZMod 2} (h : φ - ψ ∈ ContCoh.B2 AbsGalQ2 (ZMod 2)) :
H2ofFun AbsGalQ2 φ = H2ofFun AbsGalQ2 ψ

If two raw 2-cochains differ by a continuous coboundary, their H2ofFun classes agree. (Replica of ShapiroLedger.H2ofFun_eq_of_sub_mem_B2, kept local to avoid a cross-module import.)

source
theorem GQ2.RepIndependence.kappa0_cocycle {C : Type} [Group C] {W : Type} [AddCommGroup W] [DistribMulAction C W] {q : W → ZMod 2} {dat : FactorSet C W} (hdat : IsEquivariantFactorSet q dat) (a b c : SectionSix.SemiProd C W) :
kappa0 dat a b + kappa0 dat (a * b) c = kappa0 dat a (b * c) + kappa0 dat b c

κ⁰ is a 2-cocycle on V ⋊ C (the factor-set cocycle identity — display (61)/Lemma 6.1 — from the equivariant factor-set axioms m_mul, m_quad, f_cocycle).

source
def GQ2.RepIndependence.etaS {C : Type u_1} {W : Type u_2} [Group C] [AddCommGroup W] [DistribMulAction C W] (dat : FactorSet C W) (s x : SectionSix.SemiProd C W) :
ZMod 2

The inner-conjugation 1-cochain η_s(x) = κ⁰(s, x) + κ⁰(sxs⁻¹, s) on V ⋊ C.

Equations
Instances For
    source
    theorem GQ2.RepIndependence.innerConj {C : Type} [Group C] {W : Type} [AddCommGroup W] [DistribMulAction C W] {q : W → ZMod 2} {dat : FactorSet C W} (hdat : IsEquivariantFactorSet q dat) (s x y : SectionSix.SemiProd C W) :
    etaS dat s y + etaS dat s (x * y) + etaS dat s x = kappa0 dat (s * x * s⁻¹) (s * y * s⁻¹) + kappa0 dat x y

    Inner automorphisms act trivially on H² (pointwise): c_s^*κ⁰ − κ⁰ = δ¹(η_s), i.e. η_s(y) + η_s(xy) + η_s(x) = κ⁰(sxs⁻¹, sys⁻¹) + κ⁰(x, y) in char 2. Three instances of the 2-cocycle identity kappa0_cocycle at (s,x,y), (sxs⁻¹, s, y), (sxs⁻¹, sys⁻¹, s).

    source
    theorem GQ2.RepIndependence.graphPullback_sub_mem_B2 {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {W : Type} [AddCommGroup W] [TopologicalSpace W] [DiscreteTopology W] [DistribMulAction AbsGalQ2 W] [DistribMulAction C W] {q : W → ZMod 2} (dat : FactorSet C W) (hdat : IsEquivariantFactorSet q dat) (ρ : AbsGalQ2 →ₜ* C) (hρ : ∀ (g : AbsGalQ2) (w : W), g • w = ρ g • w) (b : ↥(ContCoh.Z1 AbsGalQ2 W)) (w₀ : W) :
    (graphPullback dat ⇑ρ fun (g : AbsGalQ2) => ↑b g + (g • w₀ - w₀)) - graphPullback dat ⇑ρ ↑b ∈ ContCoh.B2 AbsGalQ2 (ZMod 2)

    Core cochain identity (Lemma 6.4 / conjugation coboundary). Shifting a cocycle b by the principal coboundary g ↦ g·w₀ − w₀ changes graphPullback dat ρ b by a 2-coboundary — the (−w₀,1)-conjugation phase ψ = η_s ∘ φ_b on V ⋊ C (φ_b(g) = (b g, ρ g), s = (−w₀,1); graphPullback(b) = φ_b^*κ⁰ and φ_{b+δ⁰w₀} = c_s ∘ φ_b).

    source
    theorem GQ2.RepIndependence.repIndep {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {W : Type} [AddCommGroup W] [TopologicalSpace W] [DiscreteTopology W] [DistribMulAction AbsGalQ2 W] [DistribMulAction C W] {q : W → ZMod 2} (dat : FactorSet C W) (hdat : IsEquivariantFactorSet q dat) (ρ : AbsGalQ2 →ₜ* C) (hρ : ∀ (g : AbsGalQ2) (w : W), g • w = ρ g • w) (b₁ b₂ : ↥(ContCoh.Z1 AbsGalQ2 W)) (hcoh : (ContCoh.H1mk AbsGalQ2 W) b₁ = (ContCoh.H1mk AbsGalQ2 W) b₂) :
    H2ofFun AbsGalQ2 (graphPullback dat ⇑ρ ↑b₁) = H2ofFun AbsGalQ2 (graphPullback dat ⇑ρ ↑b₂)

    Representative independence (Lemma 6.4). H2ofFun (graphPullback dat ρ ·) depends only on the H¹-class of the cocycle.

    source
    theorem GQ2.RepIndependence.H1mk_out {M : Type u_1} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction AbsGalQ2 M] [ContinuousSMul AbsGalQ2 M] (y : ContCoh.H1 AbsGalQ2 M) :
    (ContCoh.H1mk AbsGalQ2 M) (Quotient.out y) = y

    H1mk of the canonical representative is the identity.

    source
    theorem GQ2.RepIndependence.lemma_6_14 {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] {V : Type} [AddCommGroup V] [TopologicalSpace V] [DiscreteTopology V] [DistribMulAction AbsGalQ2 V] [ContinuousSMul AbsGalQ2 V] [DistribMulAction C V] {W : Type} [AddCommGroup W] [TopologicalSpace W] [DiscreteTopology W] [DistribMulAction AbsGalQ2 W] [ContinuousSMul AbsGalQ2 W] [DistribMulAction C W] (D : TateDuality 2) (datW : FactorSet C W) (ρ : AbsGalQ2 →ₜ* C) (i : V →+ W) (hic : Continuous ⇑i) (hicompat : ∀ (g : AbsGalQ2) (v : V), i (g • v) = g • i v) {q : W → ZMod 2} (hdatW : IsEquivariantFactorSet q datW) (hiC : ∀ (c : C) (v : V), i (c • v) = c • i v) (hρW : ∀ (g : AbsGalQ2) (w : W), g • w = ρ g • w) (x : ContCoh.H1 AbsGalQ2 V) :
    SectionSix.Q0loc D (datW.comap i) ρ x = SectionSix.Q0loc D datW ρ ((ContCoh.mapCoeff1 i hic hicompat) x)

    Lemma 6.14 (regular-module realization), eq. (102). Amended (documented) with the compatibility hypotheses Q⁰_loc requires: hdatW (equivariant factor set on W), hiC (i a C-module map, eq. (77)'s i ⋊ 1), hρW (G_ℚ₂ acts on W through ρ).

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