The local invariant of a finite normal layer of the units formation

Let K be a field with separable closure Kˢ and absolute Galois group G_K, and let V ◁ U be a finite normal layer of open subgroups of G_K in the formation TauCeti.ClassFieldTheory.unitsFormation K of (Kˢ)ˣ; in field notation it is the finite Galois extension E'/E of the fixed fields of U and V. This file carries the second cohomology H²(U ⧸ V, ((Kˢ)ˣ)^V) of the layer into the continuous cohomology H²(U, (Kˢ)ˣ) of the ground subgroup by the inflation TauCeti.ClassFieldTheory.NormalLayer.explicitInfl2 of a layer, read on (Kˢ)ˣ through the coefficient dictionary unitsCoeffEquivUnitsFormation K, and, for a nonarchimedean local field K, composes with the local invariant TauCeti.ClassFieldTheory.subgroupInvMap of U to obtain the invariant of the layer

inv_{E'/E} : H²(U ⧸ V, ((Kˢ)ˣ)^V) → ℚ/ℤ

(layerInv). This is the invariant map of a layer that the class-formation axioms for unitsFormation K constrain, and this file proves the properties of it that come from Hilbert 90 and from the restriction and corestriction squares of the local invariant:

• it is injective (layerInv_injective), because inflation into H²(U, (Kˢ)ˣ) is injective by Hilbert 90 for V (NormalLayer.explicitInfl2_injective_of_subsingleton);
• its values have order dividing the degree [U : V] (degree_nsmul_layerInv), because restriction to V kills inflated classes (NormalLayer.explicitMap2_explicitInfl2_eq_zero) and multiplies the invariant by [U : V];
• restriction to an intermediate ground field multiplies it by the relative degree (layerInv_cohomologyRes), and inflation to a larger top field does not change it (layerInv_cohomologyInfl), because inflation into the cohomology of the ground subgroup is compatible with both operations on layers (NormalLayer.explicitInfl2_cohomologyRes, NormalLayer.explicitInfl2_cohomologyInfl);
• its range is exactly the subgroup of ℚ/ℤ of order [U : V] (range_layerInv). Every class of H²(U, (Kˢ)ˣ) is inflated from a layer V' ◁ U with V' ≤ V (NormalLayer.exists_explicitInfl2_eq), and by the inflation-restriction sequence of the refinement V' ◁ U of V ◁ U (LayerRefinement.range_cohomologyInfl_eq_ker_cohomologyRes) together with Hilbert 90, a class of V' ◁ U whose restriction to V' ◁ V vanishes comes from V ◁ U;
• conjugation by g : G_K preserves it (layerInv_conjugateCohomologyIso), because inflation carries the conjugation of layers to the conjugation H²(U, (Kˢ)ˣ) → H²(gUg⁻¹, (Kˢ)ˣ) (NormalLayer.explicitInfl2_conjugateCohomologyIso), which preserves the local invariant (subgroupInvMap_explicitMap2_of_conj).

Main definitions

• TauCeti.ClassFieldTheory.layerInv K L: the invariant of a layer, for a nonarchimedean local field K.

Main results

• TauCeti.ClassFieldTheory.layerInv_injective: the invariant of a layer is injective.
• TauCeti.ClassFieldTheory.degree_nsmul_layerInv: the invariant of a layer is killed by its degree.
• TauCeti.ClassFieldTheory.layerInv_cohomologyRes: restriction multiplies the invariant by the relative degree.
• TauCeti.ClassFieldTheory.layerInv_cohomologyInfl: inflation preserves the invariant.
• TauCeti.ClassFieldTheory.range_layerInv: the invariants of a layer form the subgroup of ℚ/ℤ of order its degree.
• TauCeti.ClassFieldTheory.layerInv_conjugateCohomologyIso: conjugation preserves the invariant.

Implementation notes

The continuous cohomology of the ground subgroup is that of its underlying subgroup L.ground.toSubgroup of G_K, as in TauCeti.ClassFieldTheory.subgroupInvMap, and the Galois group of the layer is read as the quotient of that subgroup by L.top.toSubgroup.subgroupOf L.ground.toSubgroup; this quotient is definitionally the Galois group L.Gal of the layer. Inflation from a layer is the generic construction of TauCeti.NumberTheory.ClassFieldTheory.Formation.Layer.Inflation at the coefficient dictionary unitsCoeffEquivUnitsFormation K, and so is its compatibility with the conjugation of layers; only Hilbert 90 is specific to the formation of units here.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §1.
• J.-P. Serre, Local Fields, Chapter XI, §1 and Chapter XIII, §3.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.6.7), for the injectivity of inflation in degree two.

Inflation from a layer of the formation of units

The invariant of a layer of the formation of units of a local field

noncomputable def TauCeti.ClassFieldTheory.layerInv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : ↑(L.H (unitsFormation K) 2) →+ AddCircle 1

The invariant of a layer V ◁ U of the formation of units of a nonarchimedean local field K: inflation NormalLayer.explicitInfl2 into H²(U, (Kˢ)ˣ) followed by the local invariant subgroupInvMap of the open subgroup U. In field notation it is the invariant inv_{E'/E} : H²(Gal(E'/E), E'ˣ) → ℚ/ℤ of the finite Galois extension E'/E that the layer cuts out. It is injective (layerInv_injective) with values killed by the degree (degree_nsmul_layerInv).

theorem TauCeti.ClassFieldTheory.layerInv_apply (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (x : ↑(L.H (unitsFormation K) 2)) : (layerInv K L) x = (subgroupInvMap K ↑L.ground ⋯) ((L.explicitInfl2 (unitsCoeffEquivUnitsFormation K) ⋯) x)

The invariant of a layer is the local invariant of the ground subgroup on the inflated class.

theorem TauCeti.ClassFieldTheory.layerInv_injective (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : Function.Injective ⇑(layerInv K L)

The invariant of a layer is injective.

theorem TauCeti.ClassFieldTheory.degree_nsmul_layerInv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (x : ↑(L.H (unitsFormation K) 2)) : L.degree • (layerInv K L) x = 0

The invariant of a layer is killed by its degree: [U : V] • inv_{E'/E} x = 0, so the invariants of a layer lie in the subgroup of ℚ/ℤ of order [U : V].

@[simp]

theorem TauCeti.ClassFieldTheory.layerInv_cohomologyRes (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {small big : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRestriction small big) (x : ↑(big.H (unitsFormation K) 2)) : (layerInv K small) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes (unitsFormation K) 2)) x) = T.relativeDegree • (layerInv K big) x

Restriction multiplies the invariant by the relative degree: for a restriction of a layer to an intermediate ground field E'', inv_{E'/E''} (res x) = [E'' : E] • inv_{E'/E} x.

@[simp]

theorem TauCeti.ClassFieldTheory.layerInv_cohomologyInfl (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {old new : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement old new) (x : ↑(old.H (unitsFormation K) 2)) : (layerInv K new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (unitsFormation K) 2)) x) = (layerInv K old) x

Inflation preserves the invariant: for a refinement of a layer to a larger top field, inv (infl x) = inv x.

@[simp]

theorem TauCeti.ClassFieldTheory.range_layerInv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : Set.range ⇑(layerInv K L) = ↑(AddSubgroup.torsionBy (AddCircle 1) ↑L.degree)

The invariants of a layer are the subgroup of ℚ/ℤ of order its degree: the range of inv_{E'/E} is the [E' : E]-torsion of ℚ/ℤ. Together with layerInv_injective, this makes H²(Gal(E'/E), E'ˣ) cyclic of order [E' : E].

@[simp]

theorem TauCeti.ClassFieldTheory.layerInv_conjugateCohomologyIso (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (g : AbsoluteGaloisGroup K) (x : ↑(L.H (unitsFormation K) 2)) : (layerInv K (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso (unitsFormation K) g 2).hom) x) = (layerInv K L) x

Conjugation preserves the invariant: for g : G_K, the conjugate class in the conjugate layer gV ◁ gU has the same invariant, inv_{gE'/gE} (g_* x) = inv_{E'/E} x.