Documentation

TauCeti.NumberTheory.ClassFieldTheory.Global.InvariantSum

The localization map and the sum of the local invariants #

Let K be a number field. A cohomological Brauer class x ∈ Br K has a local invariant TauCeti.ClassFieldTheory.finiteInvAt K v x at every finite place v and TauCeti.ClassFieldTheory.infiniteInvAt K w x at every infinite place w. This file proves that only finitely many of the finite invariants are nonzero, names the finite set where they are, brauerSupport K x, and defines the two maps of the global Brauer sequence

0 → Br K → ⨁_v Br K_v → ℚ/ℤ → 0:

the localization map brLocalization K : Br K → ⨁_v Br K_v, and the sum of the local invariants sumLocalInv K : ⨁_v Br K_v → ℚ/ℤ. The direct sum is modelled as the product of the finitely supported families Π₀ v, Br K_v over the finite places with the families Π w, Br K_w over the finitely many infinite places. The composite sumLocalInv K ∘ brLocalization K is the sum of the local invariants of a global class (sumLocalInv_brLocalization).

Finiteness is the classical argument. The class x is inflated from H²(Gal(E/K), Eˣ) for a finite Galois subextension E of Kˢ (TauCeti.ClassFieldTheory.exists_relBrInfl_eq), so it is represented by a cocycle c with finitely many values in Eˣ. Outside a finite set of places of E, the place w is unramified over K, since it does not divide the different ideal, and all values of c are w-adic units. For a finite place v of K below such a place w, the localization of x at v is inflated from H²(Gal(E_w/K_v), E_wˣ) (TauCeti.ClassFieldTheory.brBaseChange_relBrInfl), where the extension E_w/K_v is unramified and c takes unit values, so the localization vanishes (TauCeti.ClassFieldTheory.brBaseChange_relBrInfl_eq_zero).

Main definitions #

Main results #

References #

Finiteness of the ramification set #

source
theorem TauCeti.ClassFieldTheory.hasFiniteSupport_finiteInvAt (K : Type) [Field K] [NumberField K] (x : Br K) :
Function.HasFiniteSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => (finiteInvAt K v) x

A global Brauer class is unramified almost everywhere: its local invariant vanishes at all but finitely many finite places.

source
noncomputable def TauCeti.ClassFieldTheory.brauerSupport (K : Type) [Field K] [NumberField K] (x : Br K) :
Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

The ramification set of a global Brauer class: the finite set of the finite places where its local invariant is nonzero.

Instances For
    source
    @[simp]
    theorem TauCeti.ClassFieldTheory.mem_brauerSupport (K : Type) [Field K] [NumberField K] {x : Br K} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} :
    v ∈ brauerSupport K x ↔ (finiteInvAt K v) x ≠ 0

    A finite place lies in the ramification set of x exactly when the local invariant of x there is nonzero.

    source
    theorem TauCeti.ClassFieldTheory.finiteInvAt_eq_zero_of_notMem_brauerSupport (K : Type) [Field K] [NumberField K] {x : Br K} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : v ∉ brauerSupport K x) :
    (finiteInvAt K v) x = 0

    Outside its ramification set, the local invariant of a global Brauer class vanishes.

    The localization map and the sum of the local invariants #

    source
    noncomputable def TauCeti.ClassFieldTheory.brLocalization (K : Type) [Field K] [NumberField K] :
    Br K →+ (Π₀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Br (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) × ((w : NumberField.InfinitePlace K) → Br w.Completion)

    The localization map of the global Brauer sequence Br K → ⨁_v Br K_v: base change of a global Brauer class to every completion, as a finitely supported family at the finite places together with a family at the (finitely many) infinite places. The family at the finite places is supported on the ramification set brauerSupport K x.

    Instances For
      source
      @[simp]
      theorem TauCeti.ClassFieldTheory.brLocalization_fst_apply (K : Type) [Field K] [NumberField K] (x : Br K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
      ((brLocalization K) x).1 v = (brBaseChange K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x

      The component of the localization map at a finite place v is base change to K_v.

      source
      @[simp]
      theorem TauCeti.ClassFieldTheory.brLocalization_snd_apply (K : Type) [Field K] [NumberField K] (x : Br K) (w : NumberField.InfinitePlace K) :
      ((brLocalization K) x).2 w = (brBaseChange K w.Completion) x

      The component of the localization map at an infinite place w is base change to K_w.

      source
      noncomputable def TauCeti.ClassFieldTheory.sumLocalInv (K : Type) [Field K] [NumberField K] :
      (Π₀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Br (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) × ((w : NumberField.InfinitePlace K) → Br w.Completion) →+ AddCircle 1

      The sum of the local invariants, the map ⨁_v Br K_v → ℚ/ℤ of the global Brauer sequence: the sum of the invariants inv_{K_v} of a finitely supported family of local Brauer classes at the finite places, plus the archimedean invariants of a family at the infinite places (sumLocalInv_eq_sum).

      Instances For
        source
        theorem TauCeti.ClassFieldTheory.sumLocalInv_eq_sum (K : Type) [Field K] [NumberField K] (y : (Π₀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Br (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) × ((w : NumberField.InfinitePlace K) → Br w.Completion)) {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : ∀ v ∉ S, y.1 v = 0) :
        (sumLocalInv K) y = ∑ v ∈ S, (invMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (y.1 v) + ∑ w : NumberField.InfinitePlace K, (infiniteInvMap w) (y.2 w)

        The sum of the local invariants of a family of local Brauer classes may be computed over any finite set of finite places outside which the family vanishes.

        source
        @[simp]
        theorem TauCeti.ClassFieldTheory.sumLocalInv_single (K : Type) [Field K] [NumberField K] [DecidableEq (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : Br (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) :
        (sumLocalInv K) (DFinsupp.single v x, 0) = (invMap (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x

        The sum of the local invariants of a family supported at one finite place is its local invariant there.

        source
        theorem TauCeti.ClassFieldTheory.sumLocalInv_brLocalization (K : Type) [Field K] [NumberField K] (x : Br K) {S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : brauerSupport K x ⊆ S) :
        (sumLocalInv K) ((brLocalization K) x) = ∑ v ∈ S, (finiteInvAt K v) x + ∑ w : NumberField.InfinitePlace K, (infiniteInvAt K w) x

        The sum of the local invariants of a global Brauer class, the composite of the localization map with the sum of the local invariants, may be computed over any finite set of finite places containing the ramification set.