B6: local Tate duality for ℚ₂ — the dual module and the duality bundle

This file provides the statement infrastructure for the paper's local Tate duality leaf (B6): the μₙ-dual of a finite discrete G_ℚ₂-module, the evaluation cup pairing, and the bundle TateDuality n packaging the invariant map inv : H²(G_ℚ₂, μₙ) ≃+ ℤ/n together with perfectness of the cup pairing in the three degree pairs. The axiom itself (GQ2.tateDualityAt : ∀ n [NeZero n], TateDuality n) lives in GQ2/Foundations/Axioms.lean; everything here is definitions plus axiom-free, bundle-parametrized stress tests.

Encoding decisions

• Per-n form, not the colimit. The literature states duality with μ = ⋃ₙ μₙ and H²(G_k, μ) ≅ ℚ/ℤ. We state it per n (for n-torsion modules), which suffices for the paper (only n = 2 and 𝔽₂-modules are used, §§5–8) and avoids colimits of modules. Deviation flagged: cross-n compatibility of the inv's (restriction along μₙ ⊆ μₙₘ) is not asserted.
• Pontryagin-dual encoding. For an n-torsion finite abelian A, Hom(A, ℚ/ℤ) = Hom(A, ⅟n·ℤ/ℤ) ≅ Hom(A, ℤ/n); so "the dual of H" is encoded as the plain hom-group H →+ ZMod n, and no AddCircle/ℚ⧸ℤ is needed.
• The dual module M′ = Hom(M, μₙ) is MuDual n M, a def (not abbrev) type synonym of M →+ MuN n: Mathlib has a codomain-only action instance on A →+ B (DistribMulAction M (A →+ B), Mathlib/Algebra/GroupWithZero/Action/Hom.lean), so the Galois conjugation action (g • φ)(m) = g • φ(g⁻¹ • m) must live on a synonym to avoid an instance diamond. Continuity of the conjugation action is via open stabilizers (continuousSMul_iff_stabilizer_isOpen + isOpen_iInf_stabilizer: the joint action kernel on M and μₙ is open and stabilizes every φ).
• Perfectness, single currying. For each degree pair — (0,2), (1,1), (2,0), i.e. exactly the three cup shapes with M′ in the left slot and the evaluation pairing muDualPairing : M′ →+ M →+ μₙ — the clause asserts that x ↦ inv ∘ (x ∪ ·) : Hⁱ(M′) → (H^{2−i}(M) →+ ZMod n) is bijective. Deviation flagged: the opposite currying (H^{2−i}(M) → Hom(Hⁱ(M′), ℤ/n)) is not asserted; for finite cohomology groups (B7) it follows by counting, and the paper consumes only the stated direction.
• No normalization of inv. The literature pins inv down (via the valuation map and Frobenius); the bundle only asserts existence of an inv making the pairings perfect, which is what the paper's dimension counts use. The explicit n = 2 cup values enter through B7′ (the Hilbert symbol), not through inv. Deviation flagged for review.

Citations

NSW, Ch. VII §7.2, Theorem (7.2.6) (local Tate duality: the cup pairing Hⁱ(G_k, M′) × H^{2−i}(G_k, M) → H²(G_k, μ) = ℚ/ℤ is non-degenerate for finite M); Serre, Galois Cohomology II §5.2, Theorem 2; Milne, Arithmetic Duality Theorems, I.2.3. Paper: §§5–8 (dimension counts over 𝔽₂), docs/literature-axioms.md B6.

The μₙ-dual of a discrete module

def GQ2.MuDual (n : ℕ) (M : Type u_2) [AddCommGroup M] : Type u_2

The μₙ-dual module M′ = Hom(M, μₙ) of a discrete G-module M, with the conjugation action (g • φ)(m) = g • φ(g⁻¹ • m) (G a local Galois group, e.g. G_ℚ₂ or a finite-index subgroup G_K). A def (not abbrev): Mathlib's codomain-only action on M →+ MuN n must not be found here (see module docstring). The type is group-free; only the action below depends on G.

Equations

• GQ2.MuDual n M = (M →+ GQ2.MuN n)

@[implicit_reducible]

noncomputable instance GQ2.instAddCommGroupMuDual (n : ℕ) (M : Type u_2) [AddCommGroup M] : AddCommGroup (MuDual n M)

Equations

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

@[implicit_reducible]

noncomputable instance GQ2.instFunLikeMuDualMuN (n : ℕ) (M : Type u_2) [AddCommGroup M] : FunLike (MuDual n M) M (MuN n)

Equations

• GQ2.instFunLikeMuDualMuN n M = { coe := GQ2.instFunLikeMuDualMuN._aux_1 n M, coe_injective := ⋯ }

instance GQ2.instAddMonoidHomClassMuDualMuN (n : ℕ) (M : Type u_2) [AddCommGroup M] : AddMonoidHomClass (MuDual n M) M (MuN n)

theorem GQ2.MuDual.ext (n : ℕ) (M : Type u_2) [AddCommGroup M] {φ ψ : MuDual n M} (h : ∀ (m : M), φ m = ψ m) : φ = ψ

Extensionality for the dual module, keyed to the synonym's own head.

theorem GQ2.MuDual.ext_iff {n : ℕ} {M : Type u_2} [AddCommGroup M] {φ ψ : MuDual n M} : φ = ψ ↔ ∀ (m : M), φ m = ψ m

@[simp]

theorem GQ2.MuDual.zero_apply (n : ℕ) (M : Type u_2) [AddCommGroup M] (m : M) : 0 m = 0

Evaluation of the zero dual (the synonym's FunLike head keeps Mathlib's AddMonoidHom simp set from firing; these rfl-lemmas replace it).

@[simp]

theorem GQ2.MuDual.add_apply (n : ℕ) (M : Type u_2) [AddCommGroup M] (φ ψ : MuDual n M) (m : M) : (φ + ψ) m = φ m + ψ m

@[implicit_reducible]

instance GQ2.instTopologicalSpaceMuDual (n : ℕ) (M : Type u_2) [AddCommGroup M] : TopologicalSpace (MuDual n M)

Equations

• GQ2.instTopologicalSpaceMuDual n M = ⊥

instance GQ2.instDiscreteTopologyMuDual (n : ℕ) (M : Type u_2) [AddCommGroup M] : DiscreteTopology (MuDual n M)

instance GQ2.instFiniteMuDual (n : ℕ) [NeZero n] (M : Type u_2) [AddCommGroup M] [Finite M] : Finite (MuDual n M)

@[implicit_reducible]

noncomputable instance GQ2.instDistribMulActionMuDual {G : Type u_1} [Group G] (n : ℕ) [NeZero n] [DistribMulAction G (MuN n)] (M : Type u_2) [AddCommGroup M] [DistribMulAction G M] : DistribMulAction G (MuDual n M)

The conjugation action of G on Hom(M, μₙ).

Equations

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

@[simp]

theorem GQ2.muDual_smul_apply {G : Type u_1} [Group G] (n : ℕ) [NeZero n] [DistribMulAction G (MuN n)] (M : Type u_2) [AddCommGroup M] [DistribMulAction G M] (g : G) (φ : MuDual n M) (m : M) : (g • φ) m = g • φ (g⁻¹ • m)

instance GQ2.instContinuousSMulMuDualOfFinite {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) [NeZero n] [DistribMulAction G (MuN n)] [ContinuousSMul G (MuN n)] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] : ContinuousSMul G (MuDual n M)

Continuity of the conjugation action (for finite M): the joint action kernel on M and μₙ is an open subgroup fixing every φ, so all stabilizers are open.

noncomputable def GQ2.muDualPairing (n : ℕ) (M : Type u_2) [AddCommGroup M] : MuDual n M →+ M →+ MuN n

The evaluation pairing Hom(M, μₙ) →+ M →+ μₙ — under the type synonym, literally the identity. This is the μ fed to the cup products in the duality clauses.

Equations

• GQ2.muDualPairing n M = AddMonoidHom.id (M →+ GQ2.MuN n)

@[simp]

theorem GQ2.muDualPairing_apply (n : ℕ) (M : Type u_2) [AddCommGroup M] (φ : MuDual n M) (m : M) : ((muDualPairing n M) φ) m = φ m

theorem GQ2.muDualPairing_equivariant {G : Type u_1} [Group G] (n : ℕ) [NeZero n] [DistribMulAction G (MuN n)] (M : Type u_2) [AddCommGroup M] [DistribMulAction G M] (g : G) (φ : MuDual n M) (m : M) : ((muDualPairing n M) (g • φ)) (g • m) = g • ((muDualPairing n M) φ) m

Equivariance of the evaluation pairing — the hμ hypothesis of the cup products.

μₙ is n-torsion (needed to feed μₙ itself to the duality)

theorem GQ2.nsmul_muN_eq_zero (n : ℕ) [NeZero n] (x : MuN n) : n • x = 0

μₙ is n-torsion: n • x = 0 additively, i.e. ζⁿ = 1.

The duality bundle

structure GQ2.TateDualityG (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) [NeZero n] [DistribMulAction G (MuN n)] [ContinuousSMul G (MuN n)] : Type

B6 (local Tate duality), the bundle at a local Galois group G — per-n form (see the module docstring for the encoding decisions and flagged deviations). G is a local Galois group (G_ℚ₂, or a finite-index subgroup G_K for K/ℚ₂ finite; the axiom GQ2.tateDualityAt supplies an instance for exactly these G). inv identifies H²(G, μₙ) with ℤ/n, and for every finite discrete n-torsion G-module M the evaluation cup pairing is perfect in the three degree pairs, in the sense that x ↦ inv ∘ (x ∪ ·) is a bijection onto the Pontryagin dual H^{2−i}(G, M) →+ ZMod n.

Modules are quantified over Type (Type 0): every finite module is isomorphic to one there, and all of the paper's coefficients (𝔽₂-modules, μₙ, duals) live there.

• inv : ContCoh.H2 G (MuN n) ≃+ ZMod n

  The invariant map: H²(G, μₙ) ≅ ℤ/n (unnormalized; see deviations).

• perfect02 (M : Type) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] : (∀ (x : M), n • x = 0) → Function.Bijective fun (c : ↥(ContCoh.H0 G (MuDual n M))) => self.inv.toAddMonoidHom.comp ((ContCoh.cup02 (muDualPairing n M) ⋯) c)

  Perfectness in degrees (0, 2): H⁰(M′) ≅ Hom(H²(M), ℤ/n).

• perfect11 (M : Type) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] : (∀ (x : M), n • x = 0) → Function.Bijective fun (c : ContCoh.H1 G (MuDual n M)) => self.inv.toAddMonoidHom.comp ((ContCoh.cup11 (muDualPairing n M) ⋯) c)

  Perfectness in degrees (1, 1): H¹(M′) ≅ Hom(H¹(M), ℤ/n).

• perfect20 (M : Type) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] : (∀ (x : M), n • x = 0) → Function.Bijective fun (c : ContCoh.H2 G (MuDual n M)) => self.inv.toAddMonoidHom.comp ((ContCoh.cup20 (muDualPairing n M) ⋯) c)

  Perfectness in degrees (2, 0): H²(M′) ≅ Hom(H⁰(M), ℤ/n).

@[reducible, inline]

abbrev GQ2.TateDuality (n : ℕ) [NeZero n] : Type

B6 at the base field ℚ₂ — the bundle over G_ℚ₂ = AbsGalQ2 (the k = ℚ₂ member of the base-generalized family). An abbreviation, so every existing G_ℚ₂ consumer of TateDuality is unchanged.

Equations

• GQ2.TateDuality n = GQ2.TateDualityG GQ2.AbsGalQ2 n

def GQ2.IsLocalDualizingGroup (G : Type) [Group G] [TopologicalSpace G] (n : ℕ) [NeZero n] [DistribMulAction G (MuN n)] : Prop

G is a local dualizing group over ℚ₂ — the truth-side hypothesis gating the base-generalized B6 axiom GQ2.tateDualityAt: G embeds topologically as a open finite-index subgroup of G_ℚ₂, compatibly with the μₙ-action. Such G are exactly the G_K = Gal(ℚ̄₂/K) for K/ℚ₂ finite (K = the fixed field of the image), for which local Tate duality holds; G = G_ℚ₂ is the identity embedding.

Equations

• GQ2.IsLocalDualizingGroup G n = ∃ (ι : G →* GQ2.AbsGalQ2), Topology.IsOpenEmbedding ⇑ι ∧ ι.range.FiniteIndex ∧ ∀ (g : G) (x : GQ2.MuN n), g • x = ι g • x

theorem GQ2.isLocalDualizingGroup_absGalQ2 (n : ℕ) [NeZero n] : IsLocalDualizingGroup AbsGalQ2 n

G_ℚ₂ itself is a local dualizing group (the identity embedding).

Stress tests (axiom-free: parametrized over an arbitrary bundle)

Each consequence below takes D : TateDuality n, so it exercises the bundle's clauses without consuming the axiom; #print axioms stays at the standard three.

theorem GQ2.TateDuality.card_H0_dual {n : ℕ} [NeZero n] (D : TateDuality n) (M : Type) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction AbsGalQ2 M] [ContinuousSMul AbsGalQ2 M] [Finite M] (htor : ∀ (x : M), n • x = 0) : Nat.card ↥(ContCoh.H0 AbsGalQ2 (MuDual n M)) = Nat.card (ContCoh.H2 AbsGalQ2 M →+ ZMod n)

Duality, (0,2) cardinality form: #H⁰(M′) = #Hom(H²(M), ℤ/n).

theorem GQ2.TateDuality.card_H1_dual {n : ℕ} [NeZero n] (D : TateDuality n) (M : Type) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction AbsGalQ2 M] [ContinuousSMul AbsGalQ2 M] [Finite M] (htor : ∀ (x : M), n • x = 0) : Nat.card (ContCoh.H1 AbsGalQ2 (MuDual n M)) = Nat.card (ContCoh.H1 AbsGalQ2 M →+ ZMod n)

Duality, (1,1) cardinality form: #H¹(M′) = #Hom(H¹(M), ℤ/n).

theorem GQ2.TateDuality.card_H2_dual {n : ℕ} [NeZero n] (D : TateDuality n) (M : Type) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction AbsGalQ2 M] [ContinuousSMul AbsGalQ2 M] [Finite M] (htor : ∀ (x : M), n • x = 0) : Nat.card (ContCoh.H2 AbsGalQ2 (MuDual n M)) = Nat.card (↥(ContCoh.H0 AbsGalQ2 M) →+ ZMod n)

Duality, (2,0) cardinality form: #H²(M′) = #Hom(H⁰(M), ℤ/n).

theorem GQ2.TateDuality.exists_cup_ne_zero_of_ne_zero {n : ℕ} [NeZero n] (D : TateDuality n) (M : Type) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction AbsGalQ2 M] [ContinuousSMul AbsGalQ2 M] [Finite M] (htor : ∀ (x : M), n • x = 0) {c : ContCoh.H1 AbsGalQ2 (MuDual n M)} (hc : c ≠ 0) : ∃ (d : ContCoh.H1 AbsGalQ2 M), ((ContCoh.cup11 (muDualPairing n M) ⋯) c) d ≠ 0

Injectivity extraction (the form used for dimension counts): a nonzero H¹(M′)-class cups non-trivially against some H¹(M)-class.