Bundled Galois cocycles

A TauCeti.GaloisCocycle K bundles a finite Galois subextension L of the separable closure Kˢ/K with a 2-cocycle of Gal(L/K) with values in Lˣ. Bundling the extension together with its instances lets a statement quantify over "some finite Galois splitting field and some cocycle of its Galois group" without quantifying over instances.

Main definitions

• TauCeti.GaloisCocycle K: a finite Galois subextension of Kˢ/K with a 2-cocycle of its Galois group.

References

• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), §4.4.

structure TauCeti.GaloisCocycle (K : Type u) [Field K] : Type u

A Galois cocycle of K: a finite Galois subextension L of the separable closure Kˢ/K, together with a 2-cocycle of Gal(L/K) with values in Lˣ. The extension is taken inside Kˢ so that it determines an open subgroup of the absolute Galois group.

• extension : IntermediateField K (SeparableClosure K)

  The finite Galois subextension L of Kˢ/K.

• finiteDimensional : FiniteDimensional K ↥self.extension
• isGalois : IsGalois K ↥self.extension
• cocycle : TwoCocycle K ↥self.extension

  The 2-cocycle of Gal(L/K).