Prop 5.16 (local lifting duality) from B6 + B7 #
The paper's local lifting duality prop_5_16 (§5.16) is the local Tate duality bundle B6
(GQ2.tateDuality) plus the local Euler characteristic B7
(GQ2.Foundations.absGalQ2_localEulerCharacteristic), re-expressed against the 𝔽₂-valued
ElemDual/dualEval cup framework (the Tate-duality interface) used in §5.
The bridge is the n = 2 transport MuN 2 ≅ ZMod 2 (the second roots of unity are {±1} ⊂ ℚ₂,
so G_ℚ₂ acts trivially); it carries MuDual 2 A ≅ ElemDual A and muDualPairing ≅ dualEval.
The numeric clauses then follow from B6's card_H*_dual + B7 Euler-characteristic counting, and the
cup-bijectivity clauses from B6's perfect* plus the opposite-currying-by-counting argument.
The n = 2 transport MuN 2 ≅ ZMod 2 (trivial G-module). #
An abstract additive isomorphism MuN 2 ≃+ ZMod 2 (order-2 group).
Equations
- GQ2.LocalLiftingDuality.muNTwoEquiv = (GQ2.LocalLiftingDuality.card_muN_two ▸ zmodAddCyclicAddEquiv GQ2.LocalLiftingDuality.muNTwoEquiv._proof_1).symm
Instances For
G_ℚ₂ acts trivially on μ₂: the second roots of unity are {±1} ⊆ ℚ₂, fixed by every
ℚ₂-algebra automorphism.
Counting: #(V →+ 𝔽₂) = #V for a finite 𝔽₂-vector space. #
For a finite 2-torsion abelian group V (a finite 𝔽₂-vector space), the 𝔽₂-dual has the
same cardinality: #(V →+ ZMod 2) = #V. (Additive homs to 𝔽₂ are 𝔽₂-linear, and a
finite-dimensional space is isomorphic to its dual.)
Separation of points by 𝔽₂-functionals: a nonzero vector in a finite 𝔽₂-vector space
is detected by some additive functional to 𝔽₂. (Extend the singleton to a basis; the
corresponding coordinate functional is nonzero on it.)
Two-torsion of H¹ for a 2-torsion coefficient module.
Two-torsion of H² for a 2-torsion coefficient module.
Opposite currying by counting (B6's flagged deviation, discharged via B7 finiteness): for a
biadditive cup map Φ : V →+ W →+ H with H ≃+ 𝔽₂, if #V = #W (both finite 2-torsion) and the
τ-twisted opposite currying f ↦ (∃ w, ∀ c, τ(Φ c w) = f c) is surjective onto V →+ 𝔽₂, then
Φ is a perfect pairing: c ↦ Φ c is bijective onto W →+ H.
Degree-0 transport #H⁰(MuDual 2 A) = #fixedPts C (ElemDual A). #
The μ₂-dual and the 𝔽₂-dual agree through muNTwoEquiv, and the G_ℚ₂-conjugation action on
MuDual 2 A matches the C-contragredient action on ElemDual A through ρ (hcomp + trivial
action on μ₂/𝔽₂). So the invariants correspond.
Post-composition with muNTwoEquiv sends the μ₂-dual to the 𝔽₂-dual.
Equations
- GQ2.LocalLiftingDuality.dualMap φ = GQ2.LocalLiftingDuality.muNTwoEquiv.toAddMonoidHom.comp φ
Instances For
Inverse direction.
Equations
- GQ2.LocalLiftingDuality.dualMapInv lam = GQ2.LocalLiftingDuality.muNTwoEquiv.symm.toAddMonoidHom.comp lam
Instances For
The μ₂-dual and the 𝔽₂-dual are additively isomorphic (post-composition with
muNTwoEquiv). Not G-equivariant on its own, but a bijection — enough for cardinalities.
Equations
- GQ2.LocalLiftingDuality.dualAddEquiv = { toFun := GQ2.LocalLiftingDuality.dualMap, invFun := GQ2.LocalLiftingDuality.dualMapInv, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
The G_ℚ₂-invariance of φ (a μ₂-dual) rewritten pointwise, then transported to C-orbits
via ρ: φ (c • a) = φ a for every c : C.
The C-invariance of a 𝔽₂-dual lam, rewritten pointwise: lam (c • a) = lam a.
Degree-0 transport: the G_ℚ₂-invariants of the μ₂-dual biject with the C-invariants
of the 𝔽₂-dual (via post-composition with muNTwoEquiv).
H²(A) is 2-torsion when A is (it is a subquotient of 𝔽₂-valued cochains).
Clause (i): #H²(A) = #fixedPts C (ElemDual A) — B6's (0,2) duality (H⁰(A′) ≅ Hom(H²(A), 𝔽₂)), the self-dual count #Hom(H²(A),𝔽₂) = #H²(A), and the degree-0 transport.
Structural cardinalities for clause (ii). #
ker(d⁰) = H⁰.
#A = #B¹ · #H⁰ (first isomorphism theorem for d⁰: B¹ = im d⁰ ≅ A/ker d⁰ = A/H⁰).
#Z¹ = #H¹ · #B¹ (Lagrange on H¹ = Z¹/B¹).
2 ^ v₂(#A) = #A for finite 2-torsion A (a finite 𝔽₂-vector space).
Clause (ii): #Z¹(A) = #A² · #fixedPts C (ElemDual A) — from #Z¹ = #H¹·#B¹, the B7 Euler
characteristic #H¹ = #H⁰·#H²·#A, #A = #B¹·#H⁰, and clause (i).
Clause (iii): #H²(𝔽₂) = 2. #
Clause (iii): #H²(G_ℚ₂, 𝔽₂) = 2. With G_ℚ₂ acting trivially the μ₂-dual
invariants are
everything, so #H⁰(MuDual 2 𝔽₂) = #(𝔽₂ →+ μ₂) = #(𝔽₂ →+ 𝔽₂) = 2; B6's (0,2) duality then pins
#H²(𝔽₂).
Cup clauses (iv)–(vi): perfectness of the evaluation cup pairings. #
B6's perfect02/11/20 pair with the μ₂-dual MuDual 2 A in the left slot; the paper's
prop_5_16 puts A (resp. ElemDual A) in the left slot — the transpose. The bridge is
graded-commutativity (GQ2.ContCoh.cup11_comm, char 2 so the sign is +1) plus the
G-equivariant coefficient transport dualAddEquiv : MuDual 2 A ≃+ ElemDual A (from hpair),
carried across H¹/H²/H⁰ by H1congr/H2congr/H0congr and across the μ₂/𝔽₂ target by
muNTwoEquiv. Perfectness of the transpose then follows by the opposite-currying count
bijective_cup (B7 supplies the finiteness).
muNTwoEquiv : μ₂ ≃+ 𝔽₂ is G-equivariant (both actions are trivial).
dualAddEquiv : MuDual 2 A ≃+ ElemDual A is G-equivariant: the conjugation action on the
μ₂-dual matches the contragredient action on the 𝔽₂-dual, which hpair pins down.
Clause (iv): the (1,1) evaluation cup c ↦ (d ↦ c ∪ d) : H¹(A) → Hom(H¹(A′), H²(𝔽₂)) is
bijective — the transpose of B6's perfect11, discharged by graded-commutativity + counting.
Clause (v): the (0,2) evaluation cup c ↦ (d ↦ c ∪ d) : H⁰(A) → Hom(H²(A′), H²(𝔽₂)) is
bijective — the transpose of B6's perfect20 (cup02 = cup20ᵀ swaps the degree pair).
Clause (vi): the (2,0) evaluation cup c ↦ (d ↦ c ∪ d) : H²(A) → Hom(H⁰(A′), H²(𝔽₂)) is
bijective — the transpose of B6's perfect02 (cup20 = cup02ᵀ swaps the degree pair).
prop_5_16 (local lifting duality), fully assembled — all six clauses, stated with the
paper's exact signature (GQ2.FoxH.prop_5_16). This is the complete the Prop. 5.16 proof result: clauses
(i)–(iii) are the numeric/Euler-characteristic content, (iv)–(vi) the cup-perfectness content.
GQ2.FoxH.prop_5_16 could not be proved by an exact splice in its original home, because
FoxHeisenberg (where it was declared) would then have had to import this file, which already
imports FoxHeisenberg (for ElemDual/dualEval) — an import cycle. The statement was
therefore relocated out of FoxHeisenberg.lean and is proved from this bundle below.
§5.16–§5.17, relocated from GQ2/FoxHeisenberg.lean. #
prop_5_16 and cor_5_17_card are declared here (in their original GQ2.FoxH namespace, so
qualified names are unchanged) rather than in FoxHeisenberg.lean, because their proofs need B6
(GQ2.tateDuality) and the 𝔽₂-cup transport — infrastructure in files that import
FoxHeisenberg, so proving them there would be an import cycle.
Prop 5.16 (local lifting duality): for a finite elementary module with G_ℚ₂-action
factoring through ρ : G_ℚ₂ ↠ C, the display-(57) numerics hold and the cup-product API evaluation-cup
pairings are perfect in all three degree pairs (the Tate-duality interface phrasing; the clause #H²(𝔽₂) = 2
certifies the target line). The two-actions setup follows the continuous-cohomology API's compatible-pair pattern:
separate C- and G_ℚ₂-actions related pointwise through ρ — no double instance on one
type.
The proof is GQ2.LocalLiftingDuality.prop_5_16_bundle; this is where axioms B6 and B7 enter
(App. D row). It lives outside GQ2/FoxHeisenberg.lean to break an
public import cycle (the 𝔽₂-cup/B6 infrastructure imports that file).
Corollary 5.17, numerics half (proved wiring): the obstruction-space and unobstructed-lift-multiplicity cardinalities agree for the two sources. (The adjoint-boundary identity (58) is deferred: it needs connecting-map infrastructure in both theories — see the module docstring.)
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Corollary 5.17 = ⟦cor-adjointboundary⟧
- Prop 5.16 = ⟦prop-localduality⟧