The local invariant of an open subgroup of the absolute Galois group

Let K be a nonarchimedean local field with separable closure Kˢ and absolute Galois group G_K. An open subgroup U ≤ G_K is the absolute Galois group of its fixed field E, a finite extension of K, so H²(U, (Kˢ)ˣ) is the Brauer group Br E, and the local invariant of E gives an invariant on it. This file constructs that invariant directly on H²(U, (Kˢ)ˣ), inside the single Galois module (Kˢ)ˣ over G_K, which is the form in which the class-formation axioms for the units of Kˢ are stated.

Corestriction H²(U, (Kˢ)ˣ) → H²(G_K, (Kˢ)ˣ) = Br K is bijective (explicitCor2_unitsCoeff_bijective): read through G_E ≃ U, it is corestriction of Brauer classes along E/K, which preserves the local invariant (TauCeti.ClassFieldTheory.brCor_bijective). The invariant of U is therefore defined as

inv_U = inv_K ∘ cor_U^{G_K} : H²(U, (Kˢ)ˣ) ≃+ ℚ/ℤ

(subgroupInvMap). It satisfies the compatibilities that the invariant maps of a class formation are required to have:

• on a class transported from Br L along a K-embedding σ : L → Kˢ, it is the local invariant of L (subgroupInvMap_explicitMap2);
• restriction to an open subgroup V ≤ U multiplies the invariant by the index [U : V] (subgroupInvMap_explicitMap2_subgroupInclusion, and subgroupInvMap_explicitRes2 for U = G_K);
• corestriction from V to U preserves the invariant (subgroupInvMap_explicitCor2Le);
• conjugation by g : G_K, from U to gUg⁻¹, preserves the invariant (subgroupInvMap_explicitMap2_of_conj).

Main definitions

• TauCeti.ClassFieldTheory.subgroupInvMap K U hU: the local invariant H²(U, (Kˢ)ˣ) ≃+ ℚ/ℤ of an open subgroup U of G_K.

Main results

• TauCeti.ClassFieldTheory.explicitCor2_unitsCoeff_bijective: corestriction from an open subgroup of G_K is bijective on H² of (Kˢ)ˣ.
• TauCeti.ClassFieldTheory.subgroupInvMap_explicitMap2: the invariant of the subgroup cut out by a finite extension L/K is the local invariant of L.
• TauCeti.ClassFieldTheory.subgroupInvMap_explicitMap2_subgroupInclusion: restriction multiplies the invariant by the relative index.
• TauCeti.ClassFieldTheory.subgroupInvMap_explicitCor2Le: corestriction preserves the invariant.
• TauCeti.ClassFieldTheory.subgroupInvMap_explicitMap2_of_conj: conjugation preserves the invariant.

Implementation notes

The subgroup U is a plain Subgroup with a proof of openness, and its finite index is an instance argument, as for TauCeti.ContCohomology.explicitCor2. For an OpenSubgroup the instance is OpenSubgroup.finiteIndex_toSubgroup, and for the subgroup Gal(Kˢ/σ(L)) fixing the image of a K-embedding it is TauCeti.finiteIndex_fixingSubgroup_fieldRange, so both kinds of subgroup are accepted without transport.

References

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

theorem TauCeti.ClassFieldTheory.explicitCor2_unitsCoeff_bijective (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : Subgroup (AbsoluteGaloisGroup K)) [U.FiniteIndex] (hU : IsOpen ↑U) : Function.Bijective ⇑(ContCohomology.explicitCor2 (AbsoluteGaloisGroup K) (UnitsCoeff K) U hU)

Corestriction from an open subgroup of G_K is bijective on H² of (Kˢ)ˣ. The subgroup is the absolute Galois group of its fixed field E, a finite extension of K, and through this identification corestriction is corestriction of Brauer classes along E/K (TauCeti.ClassFieldTheory.brCor_bijective).

noncomputable def TauCeti.ClassFieldTheory.subgroupInvMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : Subgroup (AbsoluteGaloisGroup K)) [U.FiniteIndex] (hU : IsOpen ↑U) : ContCohomology.H2 (↥U) (UnitsCoeff K) ≃+ AddCircle 1

The local invariant of an open subgroup U of G_K: the invariant H²(U, (Kˢ)ˣ) ≃+ ℚ/ℤ obtained by corestriction to Br K = H²(G_K, (Kˢ)ˣ), which is bijective (explicitCor2_unitsCoeff_bijective), followed by the local invariant invMap K. On a class transported from the Brauer group of a finite extension L/K it is the local invariant of L (subgroupInvMap_explicitMap2).

theorem TauCeti.ClassFieldTheory.subgroupInvMap_apply (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : Subgroup (AbsoluteGaloisGroup K)) [U.FiniteIndex] (hU : IsOpen ↑U) (x : ContCohomology.H2 (↥U) (UnitsCoeff K)) : (subgroupInvMap K U hU) x = (invMap K) ((unitsRepH2Equiv K) ((ContCohomology.explicitCor2 (AbsoluteGaloisGroup K) (UnitsCoeff K) U hU) x))

The invariant of an open subgroup is the local invariant of the corestriction to G_K.

@[simp]

theorem TauCeti.ClassFieldTheory.subgroupInvMap_explicitMap2 (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (y : Br L) : (subgroupInvMap K σ.fieldRange.fixingSubgroup ⋯) ((ContCohomology.explicitMap2 (AbsoluteGaloisGroup L) (UnitsCoeff L) (↥σ.fieldRange.fixingSubgroup) (UnitsCoeff K) (↑(absoluteGaloisGroupEquivFixingSubgroup K L σ).symm) (unitsCoeffMapSymm K L σ) ⋯ ⋯) ((unitsRepH2Equiv L).symm y)) = (invMap L) y

The normalization of the invariant of an open subgroup: for a finite extension L/K embedded in Kˢ by σ, a Brauer class of L, transported to H² of the subgroup Gal(Kˢ/σ(L)) of G_K along G_L ≃ Gal(Kˢ/σ(L)) and the identification of separable closures, has the local invariant of L as invariant.

@[simp]

theorem TauCeti.ClassFieldTheory.subgroupInvMap_explicitRes2 (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U : Subgroup (AbsoluteGaloisGroup K)) [U.FiniteIndex] (hU : IsOpen ↑U) (x : ContCohomology.H2 (AbsoluteGaloisGroup K) (UnitsCoeff K)) : (subgroupInvMap K U hU) ((ContCohomology.explicitRes2 (AbsoluteGaloisGroup K) (UnitsCoeff K) U) x) = U.index • (invMap K) ((unitsRepH2Equiv K) x)

Restriction from G_K multiplies the invariant by the index: inv_U (res x) = [G_K : U] • inv_K x, since cor ∘ res is multiplication by the index.

theorem TauCeti.ClassFieldTheory.subgroupInvMap_explicitCor2Le (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U V : Subgroup (AbsoluteGaloisGroup K)) [U.FiniteIndex] [V.FiniteIndex] (hU : IsOpen ↑U) (hV : IsOpen ↑V) (hVU : V ≤ U) (y : ContCohomology.H2 (↥V) (UnitsCoeff K)) : (subgroupInvMap K U hU) ((ContCohomology.explicitCor2Le (AbsoluteGaloisGroup K) (UnitsCoeff K) U V hVU ⋯) y) = (subgroupInvMap K V hV) y

Corestriction preserves the invariant: for open subgroups V ≤ U of G_K, inv_U (cor_V^U y) = inv_V y, by transitivity of corestriction.

theorem TauCeti.ClassFieldTheory.subgroupInvMap_explicitMap2_subgroupInclusion (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U V : Subgroup (AbsoluteGaloisGroup K)) [U.FiniteIndex] [V.FiniteIndex] (hU : IsOpen ↑U) (hV : IsOpen ↑V) (hVU : V ≤ U) (x : ContCohomology.H2 (↥U) (UnitsCoeff K)) : (subgroupInvMap K V hV) ((ContCohomology.explicitMap2 (↥U) (UnitsCoeff K) (↥V) (UnitsCoeff K) (ContinuousMonoidHom.subgroupInclusion hVU) (AddMonoidHom.id (UnitsCoeff K)) ⋯ ⋯) x) = V.relIndex U • (subgroupInvMap K U hU) x

Restriction multiplies the invariant by the relative index: for open subgroups V ≤ U of G_K, inv_V (res_U^V x) = [U : V] • inv_U x.

theorem TauCeti.ClassFieldTheory.subgroupInvMap_explicitMap2_of_conj (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (U V : Subgroup (AbsoluteGaloisGroup K)) [U.FiniteIndex] [V.FiniteIndex] (hU : IsOpen ↑U) (hV : IsOpen ↑V) (g : AbsoluteGaloisGroup K) (κ : ↥V →ₜ* ↥U) (hκ : ∀ (v : ↥V), ↑(κ v) = g⁻¹ * ↑v * g) (f : UnitsCoeff K →+ UnitsCoeff K) (hf : ∀ (m : UnitsCoeff K), f m = g • m) (hVU : V = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) U) (x : ContCohomology.H2 (↥U) (UnitsCoeff K)) : (subgroupInvMap K V hV) ((ContCohomology.explicitMap2 (↥U) (UnitsCoeff K) (↥V) (UnitsCoeff K) κ f ⋯ ⋯) x) = (subgroupInvMap K U hU) x

Conjugation preserves the invariant: for g : G_K, an open subgroup U and its conjugate V = gUg⁻¹, the class (g)_* x ∈ H²(V, (Kˢ)ˣ) of the compatible pair of κ : V → U, v ↦ g⁻¹ v g, and the action f of g on (Kˢ)ˣ has the invariant of x, because corestriction to G_K does not see the conjugation (TauCeti.ContCohomology.explicitCor2_explicitMap2_of_conj).