Documentation

TauCeti.NumberTheory.ClassFieldTheory.Local.CyclicClass

Cup products of Kummer classes and cyclic classes #

Let K be a field containing a primitive n-th root of unity ζ, with n invertible in K, and let a, b ∈ Kˣ. Through ζ, the cup product of the Kummer classes (a), (b) ∈ H¹(G_K, μₙ) along kummerCupPairing ζ lies in H²(G_K, μₙ), which injects into the Brauer group Br K (h2MuToBr_injective). This file identifies its image there with a cyclic class.

Let L/K be a cyclic Galois extension of degree d ∣ n, generated by g, and s ∈ L with sⁿ = b and g s = ζ ^ (n / d) • s; for L = K(s) such a generator always exists (TauCeti.exists_forall_mem_zpowers_apply_eq). Then (a) ∪ (b) is minus the inflation to Br K of the cyclic class TauCeti.cyclicClass of a at g (kummerBrauerClass_eq_neg_relBrInfl_cyclicClass), which is classically the class of the cyclic algebra (L/K, g, a). Since inflation into Br K is injective (relBrInfl_injective) and the cyclic class of a vanishes exactly when a is a norm from L (TauCeti.cyclicClass_eq_zero_iff), the cup product (a) ∪ (b), and with it the local symbol (a, b), vanishes exactly when a is a norm from K(ⁿ√b) (cup_kummerClass_eq_zero_iff_mem_normGroup, localSymbol_eq_zero_iff_mem_normGroup). Nothing here uses local class field theory, and K need not be a local field. For a field isomorphic to ℝ, such as the completion of a field at a real place, K(√b) is ℂ when b < 0, whose norms are the positive reals, so the mod-two cup product (a) ∪ (b) vanishes exactly when a > 0 or b > 0 (cup_kummerClass_eq_zero_iff_of_ringEquiv_real).

The comparison is made on explicit cocycles. If αⁿ = a and κ_a(σ) = σ α / α, and χ(σ) ∈ [0, n) is the exponent of σ (ⁿ√b) / ⁿ√b with respect to ζ, then the cup cocycle is (σ, τ) ↦ κ_a(σ) ^ χ(τ), and the coboundary of the cochain σ ↦ α ^ χ(σ) is its product with (σ, τ) ↦ a ^ ⌊(χ(σ) + χ(τ)) / n⌋. With χ(g ^ i) = (n / d) i for 0 ≤ i < d, the latter is the inflation of the carry cocycle representing the cyclic class of a at g. This generalizes to any n, and to the continuous-cohomology Br K of class field theory, the quadratic (n = 2) cocycle computation TauCeti.TwoCocycle.inflateClass_quadratic_eq_h2MuToUnits_cup in TauCeti.Algebra.CrossedProduct.CupProduct, which this file follows as its template.

Main results #

References #

Exponents of roots of unity with respect to ζ #

The cup product of Kummer classes as a cyclic class #

source
theorem TauCeti.ClassFieldTheory.kummerBrauerClass_eq_neg_relBrInfl_cyclicClass {K : Type} [Field K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (a b : Kˣ) {s : L} (hs : s ^ n = (algebraMap K L) ↑b) {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) (hd : Module.finrank K L ∣ n) (hgs : g s = (algebraMap K L) (ζ ^ (n / Module.finrank K L)) * s) (ι : L →ₐ[K] SeparableClosure K) :
kummerBrauerClass ζ hζ a b = -(relBrInfl K L ι) ((cyclicClass hg) (Additive.ofMul a))

The cup product of two Kummer classes is a cyclic class. Let ζ ∈ K be a primitive n-th root of unity, L/K a Galois extension of degree d ∣ n whose Galois group is generated by g, and s ∈ L with sⁿ = b and g s = ζ ^ (n / d) • s. Then the image in Br K of the cup product (a) ∪ (b) along kummerCupPairing ζ hζ is minus the inflation, along any K-embedding ι : L → Kˢ, of the cyclic class of a at g.

The symbol–norm criterion #

source
theorem TauCeti.ClassFieldTheory.cup_kummerClass_eq_zero_iff_mem_normGroup {K : Type} [Field K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (hn : IsUnit ↑n) {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (a b : Kˣ) {s : L} (hs : s ^ n = (algebraMap K L) ↑b) (hgen : K⟮s⟯ = ⊤) :
(((kummerCupPairing ζ hζ).cup 1 1) (kummerClass K hn a)) (kummerClass K hn b) = 0 ↔ a ∈ normGroup K L

The cup–norm criterion. Let ζ ∈ K be a primitive n-th root of unity, with n invertible in K, and let L = K(s) with sⁿ = b. Then the cup product (a) ∪ (b) of the Kummer classes along kummerCupPairing ζ hζ vanishes exactly when a is a norm from L. K need not be a local field.

source
theorem TauCeti.ClassFieldTheory.localSymbol_eq_zero_iff_mem_normGroup {K : Type} [Field K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (tr : ↑(continuousCohomology 2 (muNRep n K)).toModuleCat ≃+ ZMod n) (hn : IsUnit ↑n) {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] (a b : Kˣ) {s : L} (hs : s ^ n = (algebraMap K L) ↑b) (hgen : K⟮s⟯ = ⊤) :
((localSymbol (kummerCupPairing ζ hζ) tr) (kummerClass K hn a)) (kummerClass K hn b) = 0 ↔ a ∈ normGroup K L

The symbol–norm criterion. Let ζ ∈ K be a primitive n-th root of unity, with n invertible in K, and let L = K(s) with sⁿ = b. Then the local symbol (a, b) along kummerCupPairing ζ hζ vanishes exactly when a is a norm from L. The identification tr : H²(G_K, μₙ) ≃+ ZMod n is arbitrary, and K need not be a local field.

Fields isomorphic to the reals #

source
theorem TauCeti.ClassFieldTheory.cup_kummerClass_eq_zero_iff_of_ringEquiv_real {K : Type} [Field K] (a b : Kˣ) (e : K ≃+* ℝ) (hζ : IsPrimitiveRoot (-1) 2) (hn : IsUnit ↑2) :
(((kummerCupPairing (-1) hζ).cup 1 1) (kummerClass K hn a)) (kummerClass K hn b) = 0 ↔ 0 < e ↑a ∨ 0 < e ↑b

The real quadratic symbol. Let K be a field isomorphic to ℝ through e, such as the completion of a field at a real place. The cup product (a) ∪ (b) of the mod-two Kummer classes of a, b ∈ Kˣ along the pairing of -1 vanishes exactly when a or b is positive.