Brauer classes split by a cyclic extension are carry classes

Let K be a field and E/K a finite Galois extension inside Kˢ whose Galois group is cyclic, generated by g, and let χ : Gal(E/K) → ℚ/ℤ be the character with χ(g) = 1 / [E : K]. Read on G_K through restriction to E, the character has open kernel, and for a ∈ Kˣ its carry cocycle

(σ, τ) ↦ a ^ ⌊χ'(σ|_E) + χ'(τ|_E)⌋

represents the Brauer class classically written a ∪ δχ. This file identifies these classes with the cyclic classes: the inflation to Br K of the class cyclicClass hg a of a in H²(Gal(E/K), Eˣ) is the carry class of χ and a (relBrInfl_cyclicClass). Indeed, on (gⁱ, gʲ) with i, j < [E : K] the carry of χ is 1 if i + j ≥ [E : K] and 0 otherwise, which are the values of the cocycle representing the cyclic class.

Every class of H²(Gal(E/K), Eˣ) is a cyclic class, so every Brauer class split by E is the carry class of χ and some a ∈ Kˣ (exists_characterCarryCocycle_eq_relBrInfl), and that carry class vanishes exactly when a is a norm from E (unitsRepH2Equiv_characterCarryCocycle_eq_zero_iff). This is how the character formula inv (a ∪ δχ) = χ (Art a) reaches every class split by a cyclic extension: over a number field it turns a product formula for the local Artin symbols of a cyclic extension into the vanishing of the sum of the local invariants of the classes it splits.

Main results

• TauCeti.ClassFieldTheory.relBrInfl_cyclicClass: the inflated cyclic class of a is the carry class of χ and a.
• TauCeti.ClassFieldTheory.exists_characterCarryCocycle_eq_relBrInfl: every Brauer class split by E is a carry class of χ.
• TauCeti.ClassFieldTheory.unitsRepH2Equiv_characterCarryCocycle_eq_zero_iff: the carry class of χ and a vanishes exactly when a is a norm from E.

References

• J. S. Milne, Class Field Theory, Chapter VII, Lemma 8.5.
• J.-P. Serre, Local Fields, Chapter XIV, §1.

theorem TauCeti.ClassFieldTheory.relBrInfl_cyclicClass {K : Type} [Field K] (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [IsGalois K ↥E] {g : Gal(↥E/K)} (hg : ∀ (σ : Gal(↥E/K)), σ ∈ Subgroup.zpowers g) {χ : Additive Gal(↥E/K) →+ AddCircle 1} (hχ : χ (Additive.ofMul g) = ↑(1 / ↑(Module.finrank K ↥E))) (a : Kˣ) : (relBrInfl K (↥E) E.val) ((cyclicClass hg) (Additive.ofMul a)) = (unitsRepH2Equiv K) ↑((ContCohomology.characterCarryCocycle (χ.comp (MonoidHom.toAdditive (AlgEquiv.restrictNormalHom ↥E))) ⋯) ((baseUnitsEquivInvariants K) (Additive.ofMul a)))

The inflated cyclic class is a carry class. Let E/K be a cyclic Galois extension inside Kˢ with generator g, and χ the character of Gal(E/K) with χ(g) = 1 / [E : K]. Then for a ∈ Kˣ, the inflation to Br K of the class of a in H²(Gal(E/K), Eˣ) at g is the class of the carry cocycle of χ, read on G_K, and a: classically, a ∪ δχ.

theorem TauCeti.ClassFieldTheory.exists_characterCarryCocycle_eq_relBrInfl {K : Type} [Field K] (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [IsGalois K ↥E] {g : Gal(↥E/K)} (hg : ∀ (σ : Gal(↥E/K)), σ ∈ Subgroup.zpowers g) {χ : Additive Gal(↥E/K) →+ AddCircle 1} (hχ : χ (Additive.ofMul g) = ↑(1 / ↑(Module.finrank K ↥E))) (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(↥E/K) (↥E)ˣ) 2)) : ∃ (a : Kˣ), (unitsRepH2Equiv K) ↑((ContCohomology.characterCarryCocycle (χ.comp (MonoidHom.toAdditive (AlgEquiv.restrictNormalHom ↥E))) ⋯) ((baseUnitsEquivInvariants K) (Additive.ofMul a))) = (relBrInfl K (↥E) E.val) y

Every Brauer class split by a cyclic extension is a carry class. If E/K is cyclic with generator g and χ(g) = 1 / [E : K], every class inflated from H²(Gal(E/K), Eˣ) to Br K is the carry class of χ, read on G_K, and some a ∈ Kˣ.

theorem TauCeti.ClassFieldTheory.unitsRepH2Equiv_characterCarryCocycle_eq_zero_iff {K : Type} [Field K] (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [IsGalois K ↥E] {g : Gal(↥E/K)} (hg : ∀ (σ : Gal(↥E/K)), σ ∈ Subgroup.zpowers g) {χ : Additive Gal(↥E/K) →+ AddCircle 1} (hχ : χ (Additive.ofMul g) = ↑(1 / ↑(Module.finrank K ↥E))) {a : Kˣ} : (unitsRepH2Equiv K) ↑((ContCohomology.characterCarryCocycle (χ.comp (MonoidHom.toAdditive (AlgEquiv.restrictNormalHom ↥E))) ⋯) ((baseUnitsEquivInvariants K) (Additive.ofMul a))) = 0 ↔ a ∈ normGroup K ↥E

The carry class of a generating character vanishes exactly on norms. If E/K is cyclic with generator g and χ(g) = 1 / [E : K], the carry class of χ, read on G_K, and a ∈ Kˣ is zero in Br K exactly when a is a norm from E.