Documentation

TauCeti.NumberTheory.ClassFieldTheory.Global.Brauer.LocalizationKernel

Idele-class H¹ and the kernel of Brauer localization #

Let L/K be a finite Galois extension of number fields with Galois group G, embedded in Kˢ by σ. The long exact cohomology sequence of 0 → Lˣ → I_L → C_L → 0 (principalIdeleShortComplex_shortExact) contains

H¹(G, I_L) → H¹(G, C_L) → H²(G, Lˣ) → H²(G, I_L).

Its first term vanishes by Hilbert 90 for ideles (subsingleton_groupCohomology_one_idelesRep), so the connecting map ideleClassToUnitsH2 K L : H¹(G, C_L) → H²(G, Lˣ) is injective (ideleClassToUnitsH2_injective), and its image is the kernel of the map induced by the principal ideles (mem_range_ideleClassToUnitsH2_iff). A class x ∈ H²(G, Lˣ) dies in H²(G, I_L) exactly when every localization of its Brauer class relBrInfl K L σ x vanishes (map_unitsToIdeles_eq_zero_iff_brLocalization_eq_zero). Hence the split Brauer classes with trivial localizations are exactly the images of H¹(G, C_L) (brLocalization_relBrInfl_eq_zero_iff_mem_range_ideleClassToUnitsH2), and

0 → H¹(G, C_L) → Br(L/K) → ⨁_v Br K_v

is exact. In particular H¹(G, C_L) vanishes exactly when localization is injective on the Brauer classes split by L (subsingleton_groupCohomology_one_ideleClassRep_iff). Since every Brauer class is split by some finite Galois extension, the injectivity of Br K → ⨁_v Br K_v (Albert–Brauer–Hasse–Noether) follows from the vanishing of H¹(Gal(L/K), C_L) for all finite Galois L/K (brLocalization_injective_of_subsingleton_groupCohomology_one), which comes from the fundamental inequalities. Equivalently, it follows from the vanishing of H¹ on the layers V ◁ G_K of the idele-class formation globalFormation K (brLocalization_injective_of_subsingleton_h1_globalFormation), the form in which the fundamental inequalities give it.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.ClassFieldTheory.ideleClassToUnitsH2 (K : Type) [Field K] (L : Type) [Field L] [NumberField L] [Algebra K L] :
↑(groupCohomology (ideleClassRep K L) 1) →+ ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2)

The connecting map H¹(Gal(L/K), C_L) → H²(Gal(L/K), Lˣ) of the exact sequence 0 → Lˣ → I_L → C_L → 0.

Instances For
    source
    theorem TauCeti.ClassFieldTheory.mem_range_ideleClassToUnitsH2_iff {K : Type} [Field K] {L : Type} [Field L] [NumberField L] [Algebra K L] (x : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2)) :
    x ∈ (ideleClassToUnitsH2 K L).range ↔ (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id Gal(L/K)) (unitsToIdeles K L) 2)) x = 0

    Exactness at H²(Gal(L/K), Lˣ): a class comes from H¹(Gal(L/K), C_L) exactly when it dies in H²(Gal(L/K), I_L).

    source
    theorem TauCeti.ClassFieldTheory.ideleClassToUnitsH2_injective {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] :
    Function.Injective ⇑(ideleClassToUnitsH2 K L)

    The connecting map H¹(Gal(L/K), C_L) → H²(Gal(L/K), Lˣ) is injective, since H¹(Gal(L/K), I_L) vanishes by Hilbert 90 for ideles.

    source
    theorem TauCeti.ClassFieldTheory.brLocalization_relBrInfl_eq_zero_iff_mem_range_ideleClassToUnitsH2 {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ : L →ₐ[K] SeparableClosure K) (x : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2)) :
    (brLocalization K) ((relBrInfl K L σ) x) = 0 ↔ x ∈ (ideleClassToUnitsH2 K L).range

    A split Brauer class has trivial localizations exactly when it comes from idele-class H¹. For L/K finite Galois, embedded in Kˢ by σ, every localization of the Brauer class relBrInfl K L σ x of x ∈ H²(Gal(L/K), Lˣ) vanishes exactly when x is the image of a class of H¹(Gal(L/K), C_L) under the connecting map of 0 → Lˣ → I_L → C_L → 0.

    source
    theorem TauCeti.ClassFieldTheory.subsingleton_groupCohomology_one_ideleClassRep_iff {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (σ : L →ₐ[K] SeparableClosure K) :
    Subsingleton ↑(groupCohomology (ideleClassRep K L) 1) ↔ ∀ (x : ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2)), (brLocalization K) ((relBrInfl K L σ) x) = 0 → x = 0

    Idele-class H¹ vanishes exactly when localization is injective on the Brauer classes split by L. For L/K finite Galois, embedded in Kˢ by σ, H¹(Gal(L/K), C_L) = 0 exactly when every x ∈ H²(Gal(L/K), Lˣ) whose Brauer class relBrInfl K L σ x has trivial localizations at all places of K is zero.

    source
    theorem TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_groupCohomology_one (K : Type) [Field K] [NumberField K] (h : ∀ (L : Type) [inst : Field L] [inst_1 : NumberField L] [inst_2 : Algebra K L] [IsGalois K L], Subsingleton ↑(groupCohomology (ideleClassRep K L) 1)) :
    Function.Injective ⇑(brLocalization K)

    The Hasse principle for Brauer classes, from idele-class H¹. If H¹(Gal(L/K), C_L) vanishes for every finite Galois extension L/K, then a Brauer class of K whose localizations at all places vanish is zero: Br K → ⨁_v Br K_v is injective.

    source
    theorem TauCeti.ClassFieldTheory.brLocalization_injective_of_subsingleton_h1_globalFormation (K : Type) [Field K] [NumberField K] (h : ∀ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)), Subsingleton ↑((NormalLayer.ofOpenNormal V).H (globalFormation K) 1)) :
    Function.Injective ⇑(brLocalization K)

    The Hasse principle from the vanishing of H¹ on the idele-class formation: if H¹ vanishes on every layer V ◁ G_K of globalFormation K, then a Brauer class of K whose localizations all vanish is zero: Br K → ⨁_v Br K_v is injective.