Inflation from the layer of a finite Galois extension into the Brauer group

For a finite Galois extension L/K presented by an embedding ι : L →ₐ[K] Kˢ, the layer of TauCeti.ClassFieldTheory.unitsFormation K cut out by L has two inflations into Br K: the layer inflation brInfl, and the relative inflation relBrInfl K L ι of the concrete Galois cohomology H²(Gal(L/K), Lˣ). This file proves that the identification TauCeti.ClassFieldTheory.layerCohomologyEquiv ι of the two cohomology groups intertwines them. Nothing here uses that K is local.

Main results

• TauCeti.ClassFieldTheory.embeddedUnitsEquivInvariants_layerCoefficientEquiv: the concrete coefficient comparison agrees with the embedding of Lˣ into (Kˢ)ˣ.
• TauCeti.ClassFieldTheory.relBrInfl_layerCohomologyEquiv: the concrete cohomology identification of the layer is compatible with inflation into Br K.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §1.
• J.-P. Serre, Local Fields, Chapter X, §1.

theorem TauCeti.ClassFieldTheory.embeddedUnitsEquivInvariants_layerCoefficientEquiv (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (x : ↑((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).rep (unitsFormation K))) : ↑((embeddedUnitsEquivInvariants K L ι) (Rep.toAdditive ((layerCoefficientEquiv ι) x))) = (unitsCoeffEquivUnitsFormation K).symm ↑x

The concrete coefficient comparison agrees with the embedding of Lˣ into the units of the separable closure.

theorem TauCeti.ClassFieldTheory.relBrInfl_layerCohomologyEquiv (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (x : ↑((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).H (unitsFormation K) 2)) : (relBrInfl K L ι) ((layerCohomologyEquiv ι 2) x) = (brInfl (fixingOpenNormalSubgroup K L)) x

The concrete cohomology identification of a finite Galois layer is compatible with inflation into the Brauer group.