Reciprocity and Brauer invariants in composita of cyclotomic towers

The cyclotomic product formula at each prime implies reciprocity on every normal subextension of a finite compositum of prime-power cyclotomic towers. In particular, the local invariants of a Brauer class split by a cyclic subextension of such a compositum sum to zero. This allows the splitting extension to involve several primes, rather than requiring it to lie in a single prime-power tower. The theorem sumLocalInv_brLocalization_relBrInfl_eq_zero_of_le_adjoin_nth_roots gives the result for every cyclic subextension of K(μ_m)/K, for any nonzero conductor m.

The simultaneous cyclotomic characters have values in a finite product of groups of p-adic units. Their common kernel fixes the compositum. A character of its Galois group therefore factors through the image of this product map. Finiteness of the family is essential when choosing a common finite support for the local factors.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Lemmas 8.4 and 8.5.
• J. Tate, Global class field theory, in Cassels–Fröhlich, Algebraic Number Theory, Chapter VII, §11.

The prime-by-prime product formula and the cyclic-class comparison are supplied by Global.Cyclotomic.ProductFormula and Global.CharacterCarry, respectively.

theorem TauCeti.ClassFieldTheory.finsum_add_sum_apply_restrictNormalHom_eq_zero_of_le_iSup_adjoin {ι : Type u_1} [Finite ι] (p : ι → ℕ) [∀ (i : ι), Fact (Nat.Prime (p i))] {K : Type} [Field K] [NumberField K] (E : IntermediateField K (SeparableClosure K)) [Normal K ↥E] (τ : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (τ' : (w : NumberField.InfinitePlace K) → SeparableClosure K →ₐ[K] SeparableClosure w.Completion) (σ : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → Field.absoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (σ' : (w : NumberField.InfinitePlace K) → Field.absoluteGaloisGroup w.Completion) (hE : E ≤ ⨆ (i : ι), IntermediateField.adjoin K {ζ : SeparableClosure K | ∃ (n : ℕ), ζ ^ p i ^ n = 1}) {M : Type u_2} [AddCommGroup M] (χ : Additive Gal(↥E/K) →+ M) (a : Kˣ) (hσ : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑(σ v) = (artinMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) a)) (hσ' : ∀ (w : NumberField.InfinitePlace K), ↑(σ' w) = (infiniteArtinAt w) ((Units.map ↑(algebraMap K w.Completion)) a)) : ∑ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), χ (Additive.ofMul ((AlgEquiv.restrictNormalHom ↥E) ((absoluteGaloisGroupMap (τ v)) ((absoluteGaloisGroupRestrictEquiv (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (σ v))))) + ∑ w : NumberField.InfinitePlace K, χ (Additive.ofMul ((AlgEquiv.restrictNormalHom ↥E) ((absoluteGaloisGroupMap (τ' w)) ((absoluteGaloisGroupRestrictEquiv w.Completion) (σ' w))))) = 0

The local Artin symbols of a nonzero global element satisfy reciprocity on every normal subextension of a finite compositum of prime-power cyclotomic towers, after applying any additive character of its Galois group.

theorem TauCeti.ClassFieldTheory.sumLocalInv_brLocalization_relBrInfl_eq_zero_of_le_iSup_adjoin {ι : Type u_1} [Finite ι] (p : ι → ℕ) [∀ (i : ι), Fact (Nat.Prime (p i))] {K : Type} [Field K] [NumberField K] (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [IsGalois K ↥E] [IsCyclic Gal(↥E/K)] (hE : E ≤ ⨆ (i : ι), IntermediateField.adjoin K {ζ : SeparableClosure K | ∃ (n : ℕ), ζ ^ p i ^ n = 1}) (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(↥E/K) (↥E)ˣ) 2)) : (sumLocalInv K) ((brLocalization K) ((relBrInfl K (↥E) E.val) y)) = 0

The local invariants of a Brauer class split by a cyclic subextension of a finite compositum of prime-power cyclotomic towers sum to zero.

theorem TauCeti.ClassFieldTheory.sumLocalInv_brLocalization_relBrInfl_eq_zero_of_le_adjoin_nth_roots {K : Type} [Field K] [NumberField K] (E : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥E] [IsGalois K ↥E] [IsCyclic Gal(↥E/K)] {m : ℕ} (hm : m ≠ 0) (hE : E ≤ IntermediateField.adjoin K {ζ : SeparableClosure K | ζ ^ m = 1}) (y : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(↥E/K) (↥E)ˣ) 2)) : (sumLocalInv K) ((brLocalization K) ((relBrInfl K (↥E) E.val) y)) = 0

The sum of local invariants vanishes on every Brauer class split by a cyclic subextension of K(μ_m)/K, for any nonzero m.