Inflation from the layers of the units formation into the Brauer group

For a field K with separable closure Kˢ and absolute Galois group G_K = Gal(Kˢ/K), the layers V ◁ G_K of the formation TauCeti.ClassFieldTheory.unitsFormation K are the finite layers of the Brauer group Br K = H²(G_K, (Kˢ)ˣ). This file gives the finite-layer description of the Brauer group for this formation: the second cohomology of the layer V ◁ G_K of an open normal subgroup V inflates into Br K (brInfl); the inflation is injective (brInfl_injective), and every Brauer class is inflated from some layer (exists_brInfl_eq). This is the map through which the invariant of the Brauer group is to be transported to the finite layers.

Main definitions

• TauCeti.ClassFieldTheory.layerBrLevelEquiv V: the second cohomology of the layer V ◁ G_K as the explicit H²(G_K ⧸ V, ((Kˢ)ˣ)^V) of the finite level V.
• TauCeti.ClassFieldTheory.brInfl V: inflation from the layer V ◁ G_K into Br K.

Main results

• TauCeti.ClassFieldTheory.brInfl_injective: inflation from a layer into Br K is injective.
• TauCeti.ClassFieldTheory.brInfl_H2π: on the class of a layer cocycle, inflation is the Brauer class of the inflated cocycle on G_K.
• TauCeti.ClassFieldTheory.exists_brInfl_eq: every Brauer class is inflated from a layer.

References

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

Inflation from the layers of open normal subgroups into the Brauer group

noncomputable def TauCeti.ClassFieldTheory.layerBrLevelEquiv {K : Type} [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : ↑((NormalLayer.ofOpenNormal V).H (unitsFormation K) 2) ≃+ ContCohomology.H2 (AbsoluteGaloisGroup K ⧸ ↑V.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) (UnitsCoeff K))

The second cohomology of the layer V ◁ G_K is that of the finite level V: Mathlib's H²(G_K ⧸ V, ((Kˢ)ˣ)^V) of the layer, carried along NormalLayer.galOfOpenNormalEquiv, is the explicit H² of the discrete finite level by TauCeti.ContCohomology.explicitH2IsoGroupCohomology. The coefficient modules are the same subgroup of (Kˢ)ˣ, the level of V.

noncomputable def TauCeti.ClassFieldTheory.brInfl {K : Type} [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : ↑((NormalLayer.ofOpenNormal V).H (unitsFormation K) 2) →+ Br K

Inflation from the layer V ◁ G_K into the Brauer group Br K = H²(G_K, (Kˢ)ˣ): the identification layerBrLevelEquiv of the layer's H² with the level of V, followed by brLevelInfl. It is injective (brInfl_injective), and every Brauer class is inflated from some layer (exists_brInfl_eq).

@[simp]

theorem TauCeti.ClassFieldTheory.brInfl_apply {K : Type} [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (x : ↑((NormalLayer.ofOpenNormal V).H (unitsFormation K) 2)) : (brInfl V) x = (brLevelInfl V) ((layerBrLevelEquiv V) x)

brInfl V is brLevelInfl after the identification layerBrLevelEquiv.

theorem TauCeti.ClassFieldTheory.brInfl_injective {K : Type} [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : Function.Injective ⇑(brInfl V)

Inflation from a layer into the Brauer group is injective, by Hilbert 90 for V (brLevelInfl_injective).

theorem TauCeti.ClassFieldTheory.brInfl_H2π {K : Type} [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (c : ↥(groupCohomology.cocycles₂ ((NormalLayer.ofOpenNormal V).rep (unitsFormation K)))) (z : ↥(ContCohomology.Z2 (AbsoluteGaloisGroup K) (UnitsCoeff K))) (hz : ∀ (g h : AbsoluteGaloisGroup K), ↑z (g, h) = (unitsCoeffEquivUnitsFormation K).symm ↑(c ((NormalLayer.galOfOpenNormalEquiv V).symm ↑g, (NormalLayer.galOfOpenNormalEquiv V).symm ↑h))) : (brInfl V) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π ((NormalLayer.ofOpenNormal V).rep (unitsFormation K)))) c) = (unitsRepH2Equiv K) ↑z

Inflation into the Brauer group on cocycle classes. brInfl V sends the class of a 2-cocycle c of the layer V ◁ G_K to the Brauer class of every continuous 2-cocycle z on G_K whose value at (g, h) is the value of c at the classes of g and h in G_K ⧸ V, read in (Kˢ)ˣ.

theorem TauCeti.ClassFieldTheory.exists_brInfl_eq (K : Type) [Field K] (x : Br K) : ∃ (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) (y : ↑((NormalLayer.ofOpenNormal V).H (unitsFormation K) 2)), (brInfl V) y = x

Every Brauer class is inflated from a layer V ◁ G_K of the formation of units (exists_brLevelInfl_eq).

theorem TauCeti.ClassFieldTheory.brInfl_surjective_of_toSubgroup_eq_bot {K : Type} [Field K] {V : OpenNormalSubgroup (AbsoluteGaloisGroup K)} (hV : ↑V.toOpenSubgroup = ⊥) : Function.Surjective ⇑(brInfl V)

If the trivial subgroup is open, its layer contains every Brauer class.