Stage F — Local continuous cohomology and Q₂ local Tate duality

This file is the local side of the lifting comparison of reference/q2_manuscript.tex §5 ("Linear lifting theory and duality"). For the local source Γ = G_{ℚ₂} the manuscript (l.1276–1283) sets

  H^i_{F,ρ}(A) = H^i_cont(G_{ℚ₂}, A_ρ),   Z^1_{F,ρ}(A) = Z^1_cont(G_{ℚ₂}, A_ρ),

the ordinary continuous Galois cohomology groups ("No two-relator complex is assigned to G_{ℚ₂}"). We build this low-degree continuous cohomology for a finite discrete F₂[Γ]-module A, and isolate the two irreducible local class-field-theory inputs of Stage F as documented axioms:

• q2_local_tate_duality — Q₂ local Tate duality (prop:localduality, Prop. 5.16): the perfect cup-product pairings H^i_{F,ρ}(A) × H^{2-i}_{F,ρ}(A^∨) → F₂. The mod-2 cyclotomic twist μ₂ is trivial ((ℤ/2)^× = 1), so A^∨(1) = A^∨.
• q2_local_euler_poincare — Tate's local Euler–Poincaré characteristic for ℚ₂: dim H⁰ − dim H¹ + dim H² = −[ℚ₂:ℚ₂]·dim A = −dim A, matching the candidate complex's term dimensions 1 − 4 + 2.

Both are standard local CFT (Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, Ch. VII §2–3), not in mathlib, and are the only non-structural inputs here.

Construction (everything below the two axioms is proven sorry-free)

A finite discrete F₂[Γ]-module is bundled as FiniteDiscreteRep Γ: a finite F₂-vector space V with a continuous action. Continuity is encoded as IsLocallyConstant (fun g => ρ g) — equivalently the action factors through a finite quotient. This needs no topology on V (IsLocallyConstant f := ∀ s, IsOpen (f⁻¹' s) constrains only the source), which keeps the dual module and all cochain spaces instance-clean.

H^i_cont is the cohomology of the complex of continuous (= locally constant, since Γ is profinite and V discrete) inhomogeneous cochains C^n_cont = {f : Γ^n → V | IsLocallyConstant f}, with the standard inhomogeneous differentials (signs are irrelevant over F₂):

 (d⁰ a)(g)     = ρ(g) a − a
 (d¹ f)(g,h)   = ρ(g)(f h) − f(g·h) + f(g)
 (d² f)(g,h,k) = ρ(g)(f(h,k)) − f(g·h,k) + f(g,h·k) − f(g,h)

We prove d¹∘d⁰ = 0, d²∘d¹ = 0, that the differentials preserve local constancy, and H⁰ = A^Γ (invariants). Then Z¹ = ker d¹ ∩ C¹_cont, H¹ = Z¹ / im d⁰, H² = (ker d² ∩ C²_cont) / d¹(C¹_cont).

instance Q2Presentation.Local.instFactPrimeOfNatNat_q2Presentation : Fact (Nat.Prime 2)

ZMod 2 = F₂ is a field; needed for Module.Dual dimension counts and FiniteDimensional over ZMod 2.

structure Q2Presentation.Local.FiniteDiscreteRep (Γ : ProfiniteGrp.{u_1}) : Type (max 1 u_1)

A finite discrete F₂[Γ]-module: a finite-dimensional F₂-vector space V with a continuous (locally constant) Γ-action ρ. Because V is finite and discrete, "continuous action" means g ↦ ρ g is locally constant, i.e. the action factors through a finite quotient of the profinite group Γ.

• V : Type

  the underlying F₂-vector space

• addCommGroup : AddCommGroup self.V
• module : Module (ZMod 2) self.V
• finite : Module.Finite (ZMod 2) self.V
• ρ : Representation (ZMod 2) (↑Γ.toProfinite.toTop) self.V

  the Γ-action

• smooth : IsLocallyConstant fun (g : ↑Γ.toProfinite.toTop) => self.ρ g

  continuity of the action (locally constant ⟺ factors through a finite quotient)

theorem Q2Presentation.Local.FiniteDiscreteRep.smooth_apply {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) (a : A.V) : IsLocallyConstant fun (g : ↑Γ.toProfinite.toTop) => (A.ρ g) a

The orbit map g ↦ ρ(g) a is locally constant, for each a.

The contragredient (dual) module A∨

def Q2Presentation.Local.FiniteDiscreteRep.dual {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : FiniteDiscreteRep Γ

The contragredient module A∨ = Hom_{F₂}(A, F₂) with the dual Γ-action (g·φ) = φ ∘ ρ(g⁻¹). Over F₂ the cyclotomic twist μ₂ is trivial, so this is the A^∨(1) appearing in Tate duality.

Equations

• A.dual = { V := Module.Dual (ZMod 2) A.V, addCommGroup := LinearMap.addCommGroup, module := LinearMap.module, finite := ⋯, ρ := A.ρ.dual, smooth := ⋯ }

@[simp]

theorem Q2Presentation.Local.FiniteDiscreteRep.dual_V {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : A.dual.V = Module.Dual (ZMod 2) A.V

The inhomogeneous continuous-cochain complex (degrees 0,1,2,3)

def Q2Presentation.Local.FiniteDiscreteRep.d0 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : A.V →ₗ[ZMod 2] ↑Γ.toProfinite.toTop → A.V

d⁰ : V → (Γ → V), (d⁰ a)(g) = ρ(g) a − a.

Equations

• A.d0 = { toFun := fun (a : A.V) (g : ↑Γ.toProfinite.toTop) => (A.ρ g) a - a, map_add' := ⋯, map_smul' := ⋯ }

def Q2Presentation.Local.FiniteDiscreteRep.d1 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : (↑Γ.toProfinite.toTop → A.V) →ₗ[ZMod 2] ↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop → A.V

d¹ : (Γ → V) → (Γ × Γ → V), (d¹ f)(g,h) = ρ(g)(f h) − f(g·h) + f(g).

Equations

• A.d1 = { toFun := fun (f : ↑Γ.toProfinite.toTop → A.V) (p : ↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop) => (A.ρ p.1) (f p.2) - f (p.1 * p.2) + f p.1, map_add' := ⋯, map_smul' := ⋯ }

def Q2Presentation.Local.FiniteDiscreteRep.d2 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : (↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop → A.V) →ₗ[ZMod 2] ↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop → A.V

d² : (Γ × Γ → V) → (Γ × Γ × Γ → V), (d² f)(g,h,k) = ρ(g)(f(h,k)) − f(g·h,k) + f(g,h·k) − f(g,h).

Equations

• One or more equations did not get rendered due to their size.

The complex property

theorem Q2Presentation.Local.FiniteDiscreteRep.d1_comp_d0 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : A.d1 ∘ₗ A.d0 = 0

d¹ ∘ d⁰ = 0 (the 1-cocycle identity).

theorem Q2Presentation.Local.FiniteDiscreteRep.d2_comp_d1 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : A.d2 ∘ₗ A.d1 = 0

d² ∘ d¹ = 0 (the 2-cocycle identity).

Local constancy of cochains is preserved by the differentials

theorem Q2Presentation.Local.FiniteDiscreteRep.isLocallyConstant_d0 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) (a : A.V) : IsLocallyConstant (A.d0 a)

d⁰ a is locally constant.

theorem Q2Presentation.Local.FiniteDiscreteRep.isLocallyConstant_d1 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) {f : ↑Γ.toProfinite.toTop → A.V} (hf : IsLocallyConstant f) : IsLocallyConstant (A.d1 f)

d¹ sends locally constant cochains to locally constant cochains.

theorem Q2Presentation.Local.FiniteDiscreteRep.isLocallyConstant_d2 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) {f : ↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop → A.V} (hf : IsLocallyConstant f) : IsLocallyConstant (A.d2 f)

d¹ as a linear map on the continuous cochains: closure used to form H².

The continuous-cochain submodules

def Q2Presentation.Local.FiniteDiscreteRep.lc1 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : Submodule (ZMod 2) (↑Γ.toProfinite.toTop → A.V)

C¹_cont = {f : Γ → V | IsLocallyConstant f}, the continuous 1-cochains.

Equations

• A.lc1 = { carrier := {f : ↑Γ.toProfinite.toTop → A.V | IsLocallyConstant f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def Q2Presentation.Local.FiniteDiscreteRep.lc2 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : Submodule (ZMod 2) (↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop → A.V)

C²_cont = {f : Γ × Γ → V | IsLocallyConstant f}, the continuous 2-cochains.

Equations

• A.lc2 = { carrier := {f : ↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop → A.V | IsLocallyConstant f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Q2Presentation.Local.FiniteDiscreteRep.mem_lc1 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) {f : ↑Γ.toProfinite.toTop → A.V} : f ∈ A.lc1 ↔ IsLocallyConstant f

@[simp]

theorem Q2Presentation.Local.FiniteDiscreteRep.mem_lc2 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) {f : ↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop → A.V} : f ∈ A.lc2 ↔ IsLocallyConstant f

Cocycles, coboundaries, and the cohomology groups

def Q2Presentation.Local.FiniteDiscreteRep.Z1 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : Submodule (ZMod 2) (↑Γ.toProfinite.toTop → A.V)

Z¹_{F,ρ}(A) = ker d¹ ∩ C¹_cont, the continuous 1-cocycles.

Equations

• A.Z1 = A.d1.ker ⊓ A.lc1

def Q2Presentation.Local.FiniteDiscreteRep.B1 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : Submodule (ZMod 2) (↑Γ.toProfinite.toTop → A.V)

B¹ = im d⁰, the 1-coboundaries (automatically continuous and in Z¹).

Equations

• A.B1 = A.d0.range

def Q2Presentation.Local.FiniteDiscreteRep.Z2 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : Submodule (ZMod 2) (↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop → A.V)

Z²_{F,ρ}(A) = ker d² ∩ C²_cont, the continuous 2-cocycles.

Equations

• A.Z2 = A.d2.ker ⊓ A.lc2

def Q2Presentation.Local.FiniteDiscreteRep.B2 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : Submodule (ZMod 2) (↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop → A.V)

B² = d¹(C¹_cont), the continuous 2-coboundaries.

Equations

• A.B2 = Submodule.map A.d1 A.lc1

def Q2Presentation.Local.FiniteDiscreteRep.Hcont0 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : Submodule (ZMod 2) A.V

H⁰_{F,ρ}(A) = ker d⁰, the continuous 0-cohomology.

Equations

• A.Hcont0 = A.d0.ker

@[reducible, inline]

abbrev Q2Presentation.Local.FiniteDiscreteRep.Hcont1 {Γ : ProfiniteGrp.{0}} (A : FiniteDiscreteRep Γ) : Type

H¹_{F,ρ}(A) = Z¹ / B¹, the continuous 1-cohomology.

Equations

• A.Hcont1 = (↥A.Z1 ⧸ Submodule.comap A.Z1.subtype A.B1)

@[reducible, inline]

abbrev Q2Presentation.Local.FiniteDiscreteRep.Hcont2 {Γ : ProfiniteGrp.{0}} (A : FiniteDiscreteRep Γ) : Type

H²_{F,ρ}(A) = Z² / B², the continuous 2-cohomology.

Equations

• A.Hcont2 = (↥A.Z2 ⧸ Submodule.comap A.Z2.subtype A.B2)

theorem Q2Presentation.Local.FiniteDiscreteRep.Hcont0_eq_invariants {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : A.Hcont0 = A.ρ.invariants

H⁰ is the invariants A^Γ (= A^C, since the action factors through the finite quotient C).

theorem Q2Presentation.Local.FiniteDiscreteRep.B1_le_Z1 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : A.B1 ≤ A.Z1

B¹ ≤ Z¹: coboundaries are continuous cocycles (the complex property range d⁰ ≤ ker d¹ together with local constancy of d⁰ a).

theorem Q2Presentation.Local.FiniteDiscreteRep.B2_le_Z2 {Γ : ProfiniteGrp.{u_1}} (A : FiniteDiscreteRep Γ) : A.B2 ≤ A.Z2

B² ≤ Z²: continuous coboundaries are continuous cocycles.

The local class-field-theory inputs for Q₂ (axioms)

Γ = GQ2Profinite = G_{ℚ₂} is the absolute Galois group of ℚ₂ (Local/GQ2.lean). The following two facts are the irreducible local arithmetic of Stage F. They are genuine theorems of local class field theory (NSW Ch. VII §2–3) but are not in mathlib, so they are isolated here as heavily-documented axioms, exactly as the Stage-C Demushkin / tame axioms are. Everything structural above is proven.

axiom Q2Presentation.Local.q2_local_tate_duality (A : FiniteDiscreteRep GQ2Profinite) : Nonempty (↥A.Hcont0 ≃ₗ[ZMod 2] Module.Dual (ZMod 2) A.dual.Hcont2) ∧ Nonempty (A.Hcont1 ≃ₗ[ZMod 2] Module.Dual (ZMod 2) A.dual.Hcont1) ∧ Nonempty (A.Hcont2 ≃ₗ[ZMod 2] Module.Dual (ZMod 2) ↥A.dual.Hcont0)

Q₂ LOCAL TATE DUALITY (prop:localduality, manuscript Prop. 5.16; NSW VII.2, Thm 7.2.6). For a finite discrete F₂[G_{ℚ₂}]-module A, the local cup product into H²(G_{ℚ₂}, μ₂) ≅ F₂ and the local invariant map give perfect pairings H^i_{F,ρ}(A) × H^{2-i}_{F,ρ}(A^∨) → F₂, equivalently linear duality isomorphisms H^i_{F,ρ}(A) ≅ (H^{2-i}_{F,ρ}(A^∨))^∨ for i = 0,1,2. The mod-2 cyclotomic twist is trivial, so A^∨(1) = A^∨ = A.dual.

Non-degeneracy is encoded by the linear equivalences to the duals; the i = 2 clause gives the manuscript's H²_{F,ρ}(A)^∨ ≅ (A^∨)^{G_{ℚ₂}} = (A^∨)^C (= Hcont0 (A.dual) = invariants). This axiom also forces the dual-dimension equality dim H^i(A) = dim H^{2-i}(A^∨) (see q2_local_dim_duality_H1/_H2).

axiom Q2Presentation.Local.q2_local_euler_poincare (A : FiniteDiscreteRep GQ2Profinite) : FiniteDimensional (ZMod 2) A.Hcont1 ∧ FiniteDimensional (ZMod 2) A.Hcont2 ∧ ↑(Module.finrank (ZMod 2) ↥A.Hcont0) - ↑(Module.finrank (ZMod 2) A.Hcont1) + ↑(Module.finrank (ZMod 2) A.Hcont2) = -↑(Module.finrank (ZMod 2) A.V)

LOCAL EULER–POINCARÉ CHARACTERISTIC for ℚ₂ (Tate; manuscript proof of prop:localduality; NSW VII.3, Thm 7.3.1). For a finite discrete F₂[G_{ℚ₂}]-module A, the low-degree continuous cohomology is finite-dimensional and

  dim H⁰ − dim H¹ + dim H² = −[ℚ₂:ℚ₂]·dim A = −dim A.

(The first two conjuncts are Tate's finiteness of local Galois cohomology of a finite module; H⁰ ⊆ A is finite-dimensional unconditionally.) This matches the candidate linear-lifting complex's term dimensions 1 − 4 + 2 = −1 for A = F₂.

Consequences derived from the two local axioms (proven)

instance Q2Presentation.Local.instFiniteDimensionalHcont1 (A : FiniteDiscreteRep GQ2Profinite) : FiniteDimensional (ZMod 2) A.Hcont1

Finite-dimensionality of all three local cohomology groups (Tate). H⁰ is free (submodule of the finite-dimensional A); H¹, H² come from the Euler axiom.

instance Q2Presentation.Local.instFiniteDimensionalHcont2 (A : FiniteDiscreteRep GQ2Profinite) : FiniteDimensional (ZMod 2) A.Hcont2

theorem Q2Presentation.Local.q2_local_dim_duality_H1 (A : FiniteDiscreteRep GQ2Profinite) : Module.finrank (ZMod 2) A.Hcont1 = Module.finrank (ZMod 2) A.dual.Hcont1

Dual-dimension equality dim H^i_{F,ρ}(A) = dim H^{2-i}_{F,ρ}(A^∨) for the self-dual middle degree, derived from local Tate duality + local finiteness.

theorem Q2Presentation.Local.q2_local_dim_duality_H2 (A : FiniteDiscreteRep GQ2Profinite) : Module.finrank (ZMod 2) A.Hcont2 = Module.finrank (ZMod 2) ↥A.dual.Hcont0

dim H²_{F,ρ}(A) = dim H⁰_{F,ρ}(A^∨) = dim (A^∨)^{G_{ℚ₂}} — the manuscript's H²_{F,ρ}(A)^∨ ≅ (A^∨)^C.

theorem Q2Presentation.Local.q2_local_Z1_dim (A : FiniteDiscreteRep GQ2Profinite) : Module.finrank (ZMod 2) ↥A.Z1 = 2 * Module.finrank (ZMod 2) A.V + Module.finrank (ZMod 2) ↥A.dual.Hcont0

The local cocycle-dimension formula dim Z¹_{F,ρ}(A) = 2·dim A + dim (A^∨)^C (prop:localduality, eq:localobdual). This is the local half of the numerical agreement of cor:adjointboundary: it matches the candidate dim Z¹_{A,ρ}(A).

Proof: dim Z¹ = dim H¹ + dim B¹ (Z¹/B¹ = H¹, both finite), dim B¹ = dim A − dim H⁰ (rank–nullity for d⁰), dim H¹ = dim H⁰ + dim H² + dim A (Euler–Poincaré), and dim H² = dim (A^∨)^C (Tate duality, q2_local_dim_duality_H2). Combining gives dim Z¹ = dim H² + 2·dim A.