Galois cocycles over fields containing a prescribed subextension

A finite Galois cocycle can be refined to a finite Galois field containing any prescribed finite subextension of the separable closure. The refinement preserves its Brauer class and its inflated cocycle on the absolute Galois group, with equality of cocycles rather than only equality of cohomology classes.

Consequently every Brauer class has a crossed-product presentation over a field containing the prescribed subextension. This is the reduction needed to compare scalar extension with restriction: the same finite field can then be regarded as Galois over either base field.

The prescribed subextension need not be normal. Its normal closure, composed with the original cocycle's field, provides the refinement.

References

• J.-P. Serre, Local Fields, Chapter X, §5.
• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology, §4.4.

theorem TauCeti.GaloisCocycle.exists_refinement {K : Type u} [Field K] (g : GaloisCocycle K) (S : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥S] : ∃ (h : GaloisCocycle K), g.extension ≤ h.extension ∧ S ≤ h.extension ∧ h.brauerClass = g.brauerClass ∧ TwoCocycle.inflate h.extension h.cocycle = TwoCocycle.inflate g.extension g.cocycle

A Galois cocycle admits a refinement whose field contains both its original field and any prescribed finite subextension. Both the Brauer class and the inflated absolute-Galois cocycle are unchanged. No normality assumption on the prescribed subextension is needed.

theorem BrauerGroup.exists_galoisCocycle_brauerClass_eq_with_le {K : Type u} [Field K] (x : BrauerGroup K) (S : IntermediateField K (SeparableClosure K)) [FiniteDimensional K ↥S] : ∃ (g : TauCeti.GaloisCocycle K), S ≤ g.extension ∧ g.brauerClass = x

Every Brauer class is represented by a finite Galois cocycle over a field containing any prescribed finite subextension of the separable closure. In particular, for a finite separable extension embedded by σ, one may take the prescribed field to be σ.fieldRange.