The local Tate-duality pairing on explicit cocycles #
The local Tate-duality pairing TauCeti.ClassFieldTheory.tateDualityPairing of a Galois
representation A : GalRep n F is the canonical cup product on Mathlib's continuous cohomology of
Field.absoluteGaloisGroup F, along the evaluation pairing Hom(A, μₙ) × A → μₙ. Tate's duality
maps TauCeti.ContCohomology.dualityMap0, dualityMap1, dualityMap2, and the local duality
theorems about them, live on explicit inhomogeneous cocycles of AbsoluteGaloisGroup F, the Galois
group of the separable closure, with coefficients μₙ = TauCeti.KummerCoeff F n and the internal
hom Hom(A, μₙ). This file identifies the two.
The carrier of A is a module over AbsoluteGaloisGroup F through the comparison
absoluteGaloisGroupRestrictEquiv (TauCeti.ClassFieldTheory.absoluteGaloisGroupAction), and the
internal hom from A to KummerCoeff F n for that action is the Tate dual
(TauCeti.ClassFieldTheory.internalHomEquivTateDual). Pulling the explicit cocycles back along
the comparison and passing to continuous cohomology, the Tate-duality pairing of the resulting
classes is the image in ZMod n of their explicit evaluation cup, in each of the three bidegrees
of total degree two.
Main definitions #
TauCeti.ClassFieldTheory.absoluteGaloisGroupAction: the action ofAbsoluteGaloisGroup Fon the carrier of a Galois representation.TauCeti.ClassFieldTheory.internalHomEquivTateDual: the internal hom fromAtoμₙover the separable closure is the Tate dual.
Main results #
TauCeti.ClassFieldTheory.tateDualityPairing_eq_explicitDualityPairing02,tateDualityPairing_eq_explicitDualityPairing11andtateDualityPairing_eq_explicitDualityPairing20: the Tate-duality pairing on explicit cocycles.
Restricting the action to the separable closure #
The action of AbsoluteGaloisGroup F on a Galois representation A, through the comparison
absoluteGaloisGroupRestrictEquiv with Field.absoluteGaloisGroup F.
Instances For
AbsoluteGaloisGroup F acts through the inverse of absoluteGaloisGroupRestrictEquiv.
Restricting the action back along absoluteGaloisGroupRestrictEquiv recovers the action of
A.
The restricted action is continuous when the action of A is.
The Tate dual over the separable closure #
The Tate dual read over the separable closure: the internal hom from A to
μₙ = KummerCoeff F n for the restricted action of AbsoluteGaloisGroup F is the Tate dual
tateDual A, a homomorphism φ going to kummerCoeffEquivMuNRep ∘ φ.
Instances For
internalHomEquivTateDual sends φ to the character kummerCoeffEquivMuNRep ∘ φ.
internalHomEquivTateDual intertwines the restricted action with the action on the Tate
dual.
The pairing on explicit cocycles #
The (0, 2) Tate-duality pairing on explicit cocycles. For an invariant x of the
internal hom and a two-cocycle class y of A over AbsoluteGaloisGroup F, pulled back along
absoluteGaloisGroupRestrictEquiv and read in continuous cohomology, the Tate-duality pairing is
the class of the explicit evaluation cup explicitDualityPairing02 x y, read in ZMod n through
tr.
The (1, 1) Tate-duality pairing on explicit cocycles. For one-cocycle classes x of
the internal hom and y of A over AbsoluteGaloisGroup F, pulled back along
absoluteGaloisGroupRestrictEquiv and read in continuous cohomology, the Tate-duality pairing is
the class of the explicit evaluation cup explicitDualityPairing11 x y, read in ZMod n through
tr.
The (2, 0) Tate-duality pairing on explicit cocycles. For a two-cocycle class x of
the internal hom and an invariant y of A over AbsoluteGaloisGroup F, pulled back along
absoluteGaloisGroupRestrictEquiv and read in continuous cohomology, the Tate-duality pairing is
the class of the explicit evaluation cup explicitDualityPairing20 x y, read in ZMod n through
tr.