Documentation

TauCeti.FieldTheory.GaloisCohomology.MuTwo.Cup

Cup products of mod-two Kummer classes #

For a field K in which 2 is invertible, multiplication in 𝔽₂ gives a pairing on the trivial coefficient object (TauCeti.trivialF2TopPairing). Composing its degree-(1,1) cup product with the Kummer isomorphism gives the bilinear pairing

Kˣ/(Kˣ)² × Kˣ/(Kˣ)² → H²(G_K, 𝔽₂),   ([a], [b]) ↦ [a] ⌣ [b].

The source is the additive square-class group TauCeti.SquareClassGroup K; consequently biadditivity and invariance under changing representatives are carried by the type. The representative formula TauCeti.kummerCup_squareClass_squareClass identifies this pairing with the cup of the classes constructed in TauCeti.FieldTheory.GaloisCohomology.MuTwo.Basic, and TauCeti.kummerCup_comm records that the pairing is symmetric.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.kummerCup (K : Type u) [Field K] [Invertible 2] :
SquareClassGroup K →+ SquareClassGroup K →+ ↑(continuousCohomology 2 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat

The mod-two Kummer cup pairing on square classes. It sends ([a], [b]) to the cup product of their Kummer classes in H²(G_K, 𝔽₂).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.kummerCup_apply (K : Type u) [Field K] [Invertible 2] (x y : SquareClassGroup K) :
    ((kummerCup K) x) y = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) ((kummerSquareClassEquiv K) x)) ((kummerSquareClassEquiv K) y)

    The Kummer cup pairing is the cup product after applying the square-class Kummer isomorphism in both variables.

    source
    theorem TauCeti.kummerCup_squareClass_squareClass (K : Type u) [Field K] [Invertible 2] (a b : Kˣ) :
    ((kummerCup K) (squareClass a)) (squareClass b) = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass a)) (kummerClass b)

    The Kummer cup on representatives is the cup product of their Kummer classes.

    source
    theorem TauCeti.kummerCup_comm (K : Type u) [Field K] [Invertible 2] (x y : SquareClassGroup K) :
    ((kummerCup K) x) y = ((kummerCup K) y) x

    The Kummer cup pairing is symmetric: [a] ⌣ [b] = [b] ⌣ [a].