The Tate dual and its evaluation pairing

For a ZMod n-representation A of the absolute Galois group of a field F, its Tate dual is

A' = Hom(A, μₙ),

with the conjugation action. This file packages Tau Ceti's generic InternalHom as a Galois coefficient object and records the evaluation pairing A' × A → μₙ. It also defines the cohomological pairing in complementary degrees whose perfectness is local Tate duality.

The construction uses the internal hom and evaluation pairing from TauCeti.Topology.Algebra.GroupAction.InternalHom, rather than introducing a parallel dual. The contravariant map on duals is precomposition, and evaluation is natural with respect to it. When n is invertible in F, μₙ is cyclic of order n, hence an injective ZMod n-module, and the dual of a short exact sequence is short exact.

The definitions follow the coefficient conventions of Neukirch--Schmidt--Wingberg, Cohomology of Number Fields, 2nd ed., (7.2.6), and Serre, Galois Cohomology, Chapter II, §5.2.

Main definitions

• TauCeti.ClassFieldTheory.tateDual: the conjugation module Hom(A, μₙ).
• TauCeti.ClassFieldTheory.tateEvaluationPairing: the named evaluation pairing.
• TauCeti.ClassFieldTheory.pairingToTateDual: the morphism A → B' curried from a pairing A × B → μₙ.
• TauCeti.ClassFieldTheory.tateDualMap: precomposition on Tate duals.
• TauCeti.ClassFieldTheory.tateDualInvariantsEquivHom: the invariants of Hom(A, μₙ) are the equivariant maps A → μₙ, as ZMod n-modules.
• TauCeti.ClassFieldTheory.tateDualityPairing: evaluation cup product in complementary degrees, followed by a chosen local invariant on H²(F, μₙ).

Main results

• TauCeti.ClassFieldTheory.tateDualMap_exact: for n invertible in F, the Tate dual of a short exact sequence is short exact.

The coefficient object

theorem TauCeti.ClassFieldTheory.nsmul_internalHom_eq_zero {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) (φ : InternalHom (Field.absoluteGaloisGroup F) ↑A ↑(muNRep n F)) : n • φ = 0

The internal hom Hom(A, μₙ) is killed by n.

@[instance_reducible]

noncomputable def TauCeti.ClassFieldTheory.internalHomModule {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) : Module (ZMod n) (InternalHom (Field.absoluteGaloisGroup F) ↑A ↑(muNRep n F))

The ZMod n-module structure on Hom(A, μₙ).

theorem TauCeti.ClassFieldTheory.internalHom_continuousSMul {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) : ContinuousSMul (ZMod n) (InternalHom (Field.absoluteGaloisGroup F) ↑A ↑(muNRep n F))

Scalar multiplication on the discrete internal hom is continuous.

noncomputable def TauCeti.ClassFieldTheory.tateDual {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) : GalRep n F

The Tate dual A' = Hom(A, μₙ), with the conjugation action.

instance TauCeti.ClassFieldTheory.instDiscreteTopologyTateDual {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) : DiscreteTopology ↑(tateDual A)

The Tate dual carries the discrete topology.

noncomputable def TauCeti.ClassFieldTheory.tateDualEquiv {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) : ↑(tateDual A) ≃+ (↑A →+ ↑(muNRep n F))

The carrier of the Tate dual is the group of additive maps A →+ μₙ.

theorem TauCeti.ClassFieldTheory.tateDualEquiv_ρ {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) (g : Field.absoluteGaloisGroup F) (φ : ↑(tateDual A)) : (tateDualEquiv A) (((tateDual A).ρ g) φ) = homAction g ((tateDualEquiv A) φ)

The action on the Tate dual is the conjugation action homAction on additive maps.

@[simp]

theorem TauCeti.ClassFieldTheory.tateDualEquiv_ρ_apply {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) (g : Field.absoluteGaloisGroup F) (φ : ↑(tateDual A)) (a : ↑A) : ((tateDualEquiv A) (((tateDual A).ρ g) φ)) a = ((muNRep n F).ρ g) (((tateDualEquiv A) φ) ((A.ρ g⁻¹) a))

The action on the Tate dual is conjugation: (g · φ)(a) = g · φ(g⁻¹ · a).

instance TauCeti.ClassFieldTheory.instFiniteTateDual {n : ℕ} {F : Type u} [Field F] [NeZero n] (A : GalRep n F) [Finite ↑A] : Finite ↑(tateDual A)

Hom(A, μₙ) is finite when A is finite and n is nonzero.

theorem TauCeti.ClassFieldTheory.isSmoothDiscrete_tateDual {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [Finite ↑A] (hA : IsSmoothDiscrete (ZMod n) A) : IsSmoothDiscrete (ZMod n) (tateDual A)

The Tate dual of a finite smooth discrete module is smooth discrete.

instance TauCeti.ClassFieldTheory.instFactIsSmoothDiscreteTateDual {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [Finite ↑A] [hA : Fact (IsSmoothDiscrete (ZMod n) A)] : Fact (IsSmoothDiscrete (ZMod n) (tateDual A))

Smoothness of the Tate dual, available to local-duality consumers by instance search.

theorem TauCeti.ClassFieldTheory.tateDual_ρ_eq_self_iff {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) (g : Field.absoluteGaloisGroup F) (φ : ↑(tateDual A)) : ((tateDual A).ρ g) φ = φ ↔ ∀ (a : ↑A), ((tateDualEquiv A) φ) ((A.ρ g) a) = ((muNRep n F).ρ g) (((tateDualEquiv A) φ) a)

An element of the Tate dual is fixed by g exactly when it intertwines the action of g.

noncomputable def TauCeti.ClassFieldTheory.tateDualInvariantsEquivHom {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] : ↥(tateDual A).ρ.invariants ≃ₗ[ZMod n] A ⟶ muNRep n F

The invariants of the Tate dual are the equivariant maps A → μₙ, as ZMod n-modules, so that H⁰(F, Hom(A, μₙ)) = Hom_{G_F}(A, μₙ): a homomorphism A → μₙ is fixed by G_F exactly when it is equivariant (tateDual_ρ_eq_self_iff), and every homomorphism out of the discrete A is continuous.

@[simp]

theorem TauCeti.ClassFieldTheory.tateDualInvariantsEquivHom_apply_hom {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] (φ : ↥(tateDual A).ρ.invariants) (a : ↑A) : (TopRep.Hom.hom ((tateDualInvariantsEquivHom A) φ)) a = ((tateDualEquiv A) ↑φ) a

tateDualInvariantsEquivHom keeps the underlying homomorphism.

@[simp]

theorem TauCeti.ClassFieldTheory.tateDualEquiv_tateDualInvariantsEquivHom_symm_apply {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] (f : A ⟶ muNRep n F) (a : ↑A) : ((tateDualEquiv A) ↑((tateDualInvariantsEquivHom A).symm f)) a = (TopRep.Hom.hom f) a

The inverse of tateDualInvariantsEquivHom keeps the underlying homomorphism.

Evaluation and contravariance

noncomputable def TauCeti.ClassFieldTheory.tateEvaluationPairing {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] : TopPairing (tateDual A) A (muNRep n F)

The evaluation pairing Hom(A, μₙ) × A → μₙ, ( φ, a ) ↦ φ(a).

@[simp]

theorem TauCeti.ClassFieldTheory.tateEvaluationPairing_bil {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] (φ : ↑(tateDual A)) (a : ↑A) : ((tateEvaluationPairing A).bil φ) a = ((tateDualEquiv A) φ) a

The named Tate evaluation pairing is ordinary evaluation.

noncomputable def TauCeti.ClassFieldTheory.pairingToTateDual {n : ℕ} {F : Type u} [Field F] {A B : GalRep n F} [DiscreteTopology ↑A] (P : TopPairing A B (muNRep n F)) : A ⟶ tateDual B

Currying a pairing into the Tate dual: a coefficient pairing A × B → μₙ on a discrete module A induces the morphism A → B', a ↦ (b ↦ P a b).

@[simp]

theorem TauCeti.ClassFieldTheory.tateDualEquiv_pairingToTateDual_apply {n : ℕ} {F : Type u} [Field F] {A B : GalRep n F} [DiscreteTopology ↑A] (P : TopPairing A B (muNRep n F)) (a : ↑A) (b : ↑B) : ((tateDualEquiv B) ((TopRep.Hom.hom (pairingToTateDual P)) a)) b = (P.bil a) b

pairingToTateDual P sends a to the character b ↦ P a b.

noncomputable def TauCeti.ClassFieldTheory.tateDualMap {n : ℕ} {F : Type u} [Field F] {A B : GalRep n F} (f : A ⟶ B) : tateDual B ⟶ tateDual A

The Tate dual is contravariant: f : A ⟶ B induces f* : B' ⟶ A' by precomposition.

@[simp]

theorem TauCeti.ClassFieldTheory.tateDualEquiv_tateDualMap_apply {n : ℕ} {F : Type u} [Field F] {A B : GalRep n F} (f : A ⟶ B) (ψ : ↑(tateDual B)) (a : ↑A) : ((tateDualEquiv A) ((TopRep.Hom.hom (tateDualMap f)) ψ)) a = ((tateDualEquiv B) ψ) ((TopRep.Hom.hom f) a)

tateDualMap f acts by precomposition with f.

@[simp]

theorem TauCeti.ClassFieldTheory.tateDualMap_id {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) : tateDualMap (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (tateDual A)

Precomposition with the identity is the identity on the Tate dual.

@[simp]

theorem TauCeti.ClassFieldTheory.tateDualMap_comp {n : ℕ} {F : Type u} [Field F] {A B C : GalRep n F} (f : A ⟶ B) (g : B ⟶ C) : tateDualMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (tateDualMap g) (tateDualMap f)

The Tate dual reverses composition: (f ≫ g)* = g* ≫ f*.

Exactness

theorem TauCeti.ClassFieldTheory.tateDualMap_injective_of_surjective {n : ℕ} {F : Type u} [Field F] {B C : GalRep n F} {g : B ⟶ C} (hg : Function.Surjective ⇑(TopRep.Hom.hom g)) : Function.Injective ⇑(TopRep.Hom.hom (tateDualMap g))

The Tate dual turns surjections into injections: if g is surjective, a character of C vanishing on the image of g is zero.

theorem TauCeti.ClassFieldTheory.exact_tateDualMap {n : ℕ} {F : Type u} [Field F] {A B C : GalRep n F} {f : A ⟶ B} {g : B ⟶ C} (hfg : Function.Exact ⇑(TopRep.Hom.hom f) ⇑(TopRep.Hom.hom g)) (hg : Function.Surjective ⇑(TopRep.Hom.hom g)) : Function.Exact ⇑(TopRep.Hom.hom (tateDualMap g)) ⇑(TopRep.Hom.hom (tateDualMap f))

The Tate dual is exact in the middle: if f, g are exact with g surjective, then g*, f* are exact, a character of B killing the image of f factoring through g.

theorem TauCeti.ClassFieldTheory.tateDualMap_surjective_of_injective {n : ℕ} {F : Type u} [Field F] (hn : IsUnit ↑n) {A B : GalRep n F} {f : A ⟶ B} (hf : Function.Injective ⇑(TopRep.Hom.hom f)) : Function.Surjective ⇑(TopRep.Hom.hom (tateDualMap f))

The Tate dual turns injections into surjections when n is invertible in F: every character of A extends along an injection A ⟶ B, because μₙ is then an injective ZMod n-module (baer_muNRep).

theorem TauCeti.ClassFieldTheory.tateDualMap_exact {n : ℕ} {F : Type u} [Field F] (hn : IsUnit ↑n) {A B C : GalRep n F} {f : A ⟶ B} {g : B ⟶ C} (hf : Function.Injective ⇑(TopRep.Hom.hom f)) (hfg : Function.Exact ⇑(TopRep.Hom.hom f) ⇑(TopRep.Hom.hom g)) (hg : Function.Surjective ⇑(TopRep.Hom.hom g)) : Function.Injective ⇑(TopRep.Hom.hom (tateDualMap g)) ∧ Function.Exact ⇑(TopRep.Hom.hom (tateDualMap g)) ⇑(TopRep.Hom.hom (tateDualMap f)) ∧ Function.Surjective ⇑(TopRep.Hom.hom (tateDualMap f))

The Tate dual of a short exact sequence is short exact when n is invertible in F: for 0 → A → B → C → 0 exact, 0 → C' → B' → A' → 0 is exact.

theorem TauCeti.ClassFieldTheory.tateEvaluationPairing_tateDualMap {n : ℕ} {F : Type u} [Field F] {A B : GalRep n F} [DiscreteTopology ↑A] [DiscreteTopology ↑B] (f : A ⟶ B) (ψ : ↑(tateDual B)) (a : ↑A) : ((tateEvaluationPairing A).bil ((TopRep.Hom.hom (tateDualMap f)) ψ)) a = ((tateEvaluationPairing B).bil ψ) ((TopRep.Hom.hom f) a)

Evaluation is natural in the coefficient module: ⟨f* ψ, a⟩ = ⟨ψ, f a⟩.

The cohomological pairing

noncomputable def TauCeti.ClassFieldTheory.tateDualityPairing {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) (x : ↑(continuousCohomology i (tateDual A)).toModuleCat) (y : ↑(continuousCohomology j A).toModuleCat) : ZMod n

The local Tate-duality pairing in complementary degrees, formed from the named evaluation pairing and an identification of H²(F, μₙ) with ZMod n.

theorem TauCeti.ClassFieldTheory.tateDualityPairing_def {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) (x : ↑(continuousCohomology i (tateDual A)).toModuleCat) (y : ↑(continuousCohomology j A).toModuleCat) : tateDualityPairing A tr i j hij x y = tr (hij ▸ (((tateEvaluationPairing A).cup i j) x) y)

The local Tate-duality pairing is the chosen invariant of the evaluation cup product.

theorem TauCeti.ClassFieldTheory.tateDualityPairing_add_left {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) (x x' : ↑(continuousCohomology i (tateDual A)).toModuleCat) (y : ↑(continuousCohomology j A).toModuleCat) : tateDualityPairing A tr i j hij (x + x') y = tateDualityPairing A tr i j hij x y + tateDualityPairing A tr i j hij x' y

The local Tate-duality pairing is additive in its first argument.

theorem TauCeti.ClassFieldTheory.tateDualityPairing_add_right {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) (x : ↑(continuousCohomology i (tateDual A)).toModuleCat) (y y' : ↑(continuousCohomology j A).toModuleCat) : tateDualityPairing A tr i j hij x (y + y') = tateDualityPairing A tr i j hij x y + tateDualityPairing A tr i j hij x y'

The local Tate-duality pairing is additive in its second argument.

@[simp]

theorem TauCeti.ClassFieldTheory.tateDualityPairing_zero_left {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) (y : ↑(continuousCohomology j A).toModuleCat) : tateDualityPairing A tr i j hij 0 y = 0

The local Tate-duality pairing vanishes when its first argument is zero.

@[simp]

theorem TauCeti.ClassFieldTheory.tateDualityPairing_zero_right {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) (x : ↑(continuousCohomology i (tateDual A)).toModuleCat) : tateDualityPairing A tr i j hij x 0 = 0

The local Tate-duality pairing vanishes when its second argument is zero.

theorem TauCeti.ClassFieldTheory.tateDualityPairing_tateDualMap {n : ℕ} {F : Type u} [Field F] {A B : GalRep n F} [DiscreteTopology ↑A] [DiscreteTopology ↑B] (f : A ⟶ B) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) (x : ↑(continuousCohomology i (tateDual B)).toModuleCat) (y : ↑(continuousCohomology j A).toModuleCat) : tateDualityPairing A tr i j hij ((TopModuleCat.Hom.hom (ContinuousCohomology.coeffMap (tateDualMap f) i)) x) y = tateDualityPairing B tr i j hij x ((TopModuleCat.Hom.hom (ContinuousCohomology.coeffMap f j)) y)

Naturality of the local Tate-duality pairing: ⟨f* x, y⟩ = ⟨x, f* y⟩.

theorem TauCeti.ClassFieldTheory.tateDualityPairing_pairingToTateDual {n : ℕ} {F : Type u} [Field F] {A B : GalRep n F} [DiscreteTopology ↑A] [DiscreteTopology ↑B] (P : TopPairing A B (muNRep n F)) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) (x : ↑(continuousCohomology i A).toModuleCat) (y : ↑(continuousCohomology j B).toModuleCat) : tateDualityPairing B tr i j hij ((TopModuleCat.Hom.hom (ContinuousCohomology.coeffMap (pairingToTateDual P) i)) x) y = tr (hij ▸ ((P.cup i j) x) y)

The Tate pairing transported along a curried pairing: for a pairing P : A × B → μₙ, pairing the image of x under A → B' with y is the chosen invariant of P.cup x y.