Documentation

TauCeti.Algebra.CrossedProduct.Comparison

The Brauer group as continuous H² of the absolute Galois group #

For a field K with separable closure Kˢ, this file constructs the comparison isomorphism

brauerCohomologyEquiv K : Additive (Br K) ≃+ H²_cont(G_K, (Kˢ)ˣ)

and characterizes it: on the Brauer class of the crossed product of a cocycle z of a finite Galois subextension L ⊆ Kˢ, it takes the value z.inflateClass L, the continuous class of the inflation of z (brauerCohomologyEquiv_crossedProductClass). Every Brauer class is such a crossed-product class, so this equation determines the comparison (brauerCohomologyEquiv_unique).

The equation is consistent because both sides only depend on the Brauer class. Two bundled Galois cocycles can be compared over the compositum of their splitting fields, where neither side changes (crossedProductClass_comap, TwoCocycle.inflateClass_comap). Over a single finite Galois L ⊆ Kˢ the two sides are then equal together (BrauerGroup.crossedProductClass_eq_iff_inflateClass_eq): cohomologous cocycles inflate to the same class, and conversely a cocycle whose inflation is a continuous coboundary d b presents the trivial Brauer class. For the converse, the continuous cochain b descends to a finite Galois M ⊇ L with values in Mˣ (ContCohomology.exists_openNormalSubgroup_descendContinuous and the fixed-field theorem for units), so that the cocycle refined to M is a coboundary there. Multiplicativity of crossed-product classes (crossedProductClass_mul) and additivity of inflation (TwoCocycle.inflateClass_mul) make the comparison a homomorphism, and the two exhaustion theorems BrauerGroup.exists_galoisCocycle_brauerClass_eq and exists_galoisCocycle_inflateClass make it bijective.

Main definitions #

Main results #

References #

Refining a cocycle to a larger subextension #

source
theorem TauCeti.BrauerGroup.crossedProductClass_eq_iff_inflateClass_eq {K : Type} [Field K] {L : IntermediateField K (SeparableClosure K)} [FiniteDimensional K ↥L] [IsGalois K ↥L] {z w : TwoCocycle K ↥L} :
crossedProductClass z = crossedProductClass w ↔ TwoCocycle.inflateClass L z = TwoCocycle.inflateClass L w

Over a fixed finite Galois L ⊆ Kˢ, the Brauer class and the inflated continuous class determine each other: two cocycles of Gal(L/K) have the same crossed-product class exactly when their inflations to the absolute Galois group have the same class in H²_cont(G_K, (Kˢ)ˣ).

source
theorem TauCeti.BrauerGroup.crossedProductClass_eq_one_iff_inflateClass_eq_zero {K : Type} [Field K] {L : IntermediateField K (SeparableClosure K)} [FiniteDimensional K ↥L] [IsGalois K ↥L] {c : TwoCocycle K ↥L} :
crossedProductClass c = 1 ↔ TwoCocycle.inflateClass L c = 0

A crossed product over a finite Galois L ⊆ Kˢ is split exactly when the inflation of its cocycle is a continuous coboundary.

source
theorem TauCeti.GaloisCocycle.brauerClass_eq_iff_inflateClass_eq {K : Type} [Field K] {g₁ g₂ : GaloisCocycle K} :
g₁.brauerClass = g₂.brauerClass ↔ g₁.inflateClass = g₂.inflateClass

Two Galois cocycles have the same Brauer class exactly when they inflate to the same continuous class, possibly over different finite Galois subextensions of Kˢ/K.

The comparison isomorphism #

source
noncomputable def TauCeti.brauerCohomologyEquiv (K : Type) [Field K] :
Additive (BrauerGroup K) ≃+ ↑(continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K))).toModuleCat

The comparison isomorphism Br(K) ≃ H²_cont(G_K, (Kˢ)ˣ), with multiplication of Brauer classes going to addition of cohomology classes. It is characterized by brauerCohomologyEquiv_crossedProductClass: the class of the crossed product of a cocycle of a finite Galois L ⊆ Kˢ goes to the continuous class of the inflation of that cocycle; see brauerCohomologyEquiv_unique.

Equations
Instances For
    source
    theorem TauCeti.brauerCohomologyEquiv_galoisCocycle_brauerClass {K : Type} [Field K] (g : GaloisCocycle K) :
    (brauerCohomologyEquiv K) (Additive.ofMul g.brauerClass) = g.inflateClass

    The comparison on a bundled Galois cocycle: the Brauer class of a Galois cocycle goes to its inflated continuous class.

    source
    @[simp]
    theorem TauCeti.brauerCohomologyEquiv_crossedProductClass {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [IsGalois K ↥L] (z : TwoCocycle K ↥L) :
    (brauerCohomologyEquiv K) (Additive.ofMul (BrauerGroup.crossedProductClass z)) = TwoCocycle.inflateClass L z

    The equation that determines the comparison. On the class of the crossed product of a cocycle z of a finite Galois L ⊆ Kˢ, the comparison is the continuous class of the inflation of z to the absolute Galois group.

    source
    @[simp]
    theorem TauCeti.brauerCohomologyEquiv_symm_inflateClass {K : Type} [Field K] (L : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥L] [IsGalois K ↥L] (z : TwoCocycle K ↥L) :
    (brauerCohomologyEquiv K).symm (TwoCocycle.inflateClass L z) = Additive.ofMul (BrauerGroup.crossedProductClass z)

    The inverse comparison sends the inflated class of a cocycle of a finite Galois L ⊆ Kˢ to the Brauer class of its crossed product.

    source
    theorem TauCeti.brauerCohomologyEquiv_unique {K : Type} [Field K] (e : Additive (BrauerGroup K) ≃+ ↑(continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K))).toModuleCat) (h : ∀ (g : GaloisCocycle K), e (Additive.ofMul g.brauerClass) = g.inflateClass) :
    e = brauerCohomologyEquiv K

    There is only one such comparison. Any additive equivalence sending the Brauer class of each Galois cocycle to its inflated continuous class is brauerCohomologyEquiv K, because every Brauer class is the class of a Galois cocycle.