The formation of the units of a separable closure

For a field K with separable closure Kˢ and absolute Galois group G_K = Gal(Kˢ/K), this file builds the formation unitsFormation K whose coefficient module is the multiplicative group (Kˢ)ˣ, written additively. Its level at an open subgroup U is the unit group of the fixed field of U (mem_level_unitsFormation_iff), presented as Eˣ when that fixed field is the image of a K-embedding of E (unitsLevelEquiv), and its finite normal layers are the finite Galois extensions E/F inside Kˢ. It is the formation on which the local class formation is to be built.

For a finite extension L/K embedded in Kˢ, restriction of this formation from G_K to the open subgroup identified with G_L is canonically isomorphic to unitsFormation L (localFormationRestrict). On coefficients this isomorphism is induced by the identification Lˢ ≃ Kˢ extending the chosen embedding.

The first input of the class-formation axioms is proved here, for every field K: Hilbert 90 on every finite normal layer (subsingleton_h1_unitsFormation), H¹(U ⧸ V, ((Kˢ)ˣ)^V) = 0 for open subgroups V ◁ U. The finite-layer description of the Brauer group through this formation is in TauCeti.NumberTheory.ClassFieldTheory.Brauer.Formation.

Implementation notes

The body of unitsFormation is not exposed; its coefficient module is read through the dictionary unitsCoeffEquivUnitsFormation, as TauCeti.ClassFieldTheory.unitsRep is read through TauCeti.ClassFieldTheory.unitsCoeffEquivUnitsRep.

Main definitions

• TauCeti.ClassFieldTheory.unitsFormation K: the formation of (Kˢ)ˣ over G_K.
• TauCeti.ClassFieldTheory.unitsCoeffEquivUnitsFormation K: its coefficient module as TauCeti.UnitsCoeff K.
• TauCeti.ClassFieldTheory.localFormationRestrict K L σ: restriction from G_K to G_L as an isomorphism of topological representations.
• TauCeti.ClassFieldTheory.localFormationHomInv K L σ h: the inverse U' → U of the embedding G_L → G_K on a subgroup U' of the image of U ≤ G_L.
• TauCeti.ClassFieldTheory.unitsLevelEquiv ι hU: the level of an open subgroup U whose fixed field is the image of ι : E →ₐ[K] Kˢ is Eˣ.

Main results

• TauCeti.ClassFieldTheory.mem_level_unitsFormation_iff: the level of an open subgroup is the unit group of its fixed field.
• TauCeti.ClassFieldTheory.subsingleton_h1_unitsFormation: H¹ of every finite normal layer vanishes.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §1.
• J.-P. Serre, Local Fields, Chapter X, §1, and Chapter XI, §1.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (6.2.1).

noncomputable def TauCeti.ClassFieldTheory.unitsFormation (K : Type) [Field K] : Formation (AbsoluteGaloisGroup K)

The formation of the units of a separable closure: the discrete module (Kˢ)ˣ, written additively as TauCeti.UnitsCoeff K, over the absolute Galois group G_K = Gal(Kˢ/K). Its elements are read through unitsCoeffEquivUnitsFormation, and its level at an open subgroup is the unit group of the fixed field of that subgroup (mem_level_unitsFormation_iff).

noncomputable def TauCeti.ClassFieldTheory.unitsCoeffEquivUnitsFormation (K : Type) [Field K] : UnitsCoeff K ≃+ ↑(unitsFormation K).toRep

The coefficient dictionary between TauCeti.UnitsCoeff K and the coefficient module of unitsFormation K. It is equivariant by unitsCoeffEquivUnitsFormation_smul.

@[simp]

theorem TauCeti.ClassFieldTheory.unitsCoeffEquivUnitsFormation_smul (K : Type) [Field K] (g : AbsoluteGaloisGroup K) (x : UnitsCoeff K) : (unitsCoeffEquivUnitsFormation K) (g • x) = ((unitsFormation K).toRep.ρ g) ((unitsCoeffEquivUnitsFormation K) x)

The coefficient dictionary is equivariant: G_K acts on the coefficient module of unitsFormation K as it acts on (Kˢ)ˣ.

Restriction to a finite extension

noncomputable def TauCeti.ClassFieldTheory.localFormationHom (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) : AbsoluteGaloisGroup L →* AbsoluteGaloisGroup K

The homomorphism G_L → G_K obtained by identifying G_L with the subgroup fixing σ(L) and including that subgroup in G_K.

theorem TauCeti.ClassFieldTheory.localFormationHom_apply (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (g : AbsoluteGaloisGroup L) : (localFormationHom K L σ) g = ↑((galoisSubgroupEquiv K L σ) g)

The embedding G_L → G_K is TauCeti.galoisSubgroupEquiv followed by the inclusion of the open subgroup fixing σ(L).

theorem TauCeti.ClassFieldTheory.range_localFormationHom (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) : (localFormationHom K L σ).range = ↑(galoisSubgroup K L σ)

The image of the embedding G_L → G_K is the open subgroup of G_K fixing σ(L).

theorem TauCeti.ClassFieldTheory.continuous_localFormationHom (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) : Continuous ⇑(localFormationHom K L σ)

The embedding of absolute Galois groups underlying restriction of the units formation is continuous.

theorem TauCeti.ClassFieldTheory.injective_localFormationHom (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) : Function.Injective ⇑(localFormationHom K L σ)

The embedding of absolute Galois groups underlying restriction of the units formation is injective.

theorem TauCeti.ClassFieldTheory.isOpenMap_localFormationHom (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) : IsOpenMap ⇑(localFormationHom K L σ)

The embedding of absolute Galois groups underlying restriction of the units formation is an open map.

noncomputable def TauCeti.ClassFieldTheory.localFormationHomInv (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) {U : Subgroup (AbsoluteGaloisGroup L)} {U' : Subgroup (AbsoluteGaloisGroup K)} (h : U' ≤ Subgroup.map (localFormationHom K L σ) U) : ↥U' →ₜ* ↥U

The inverse of the embedding G_L → G_K on a subgroup of the image of U ≤ G_L: the continuous homomorphism U' → U, for U' ≤ U.map (localFormationHom K L σ), given by the inverse of TauCeti.galoisSubgroupEquiv (localFormationHom_localFormationHomInv).

theorem TauCeti.ClassFieldTheory.localFormationHomInv_apply_coe (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) {U : Subgroup (AbsoluteGaloisGroup L)} {U' : Subgroup (AbsoluteGaloisGroup K)} (h : U' ≤ Subgroup.map (localFormationHom K L σ) U) (u : ↥U') : ↑((localFormationHomInv K L σ h) u) = (galoisSubgroupEquiv K L σ).symm ⟨↑u, ⋯⟩

On underlying elements, localFormationHomInv is the inverse of TauCeti.galoisSubgroupEquiv.

@[simp]

theorem TauCeti.ClassFieldTheory.localFormationHom_localFormationHomInv (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) {U : Subgroup (AbsoluteGaloisGroup L)} {U' : Subgroup (AbsoluteGaloisGroup K)} (h : U' ≤ Subgroup.map (localFormationHom K L σ) U) (u : ↥U') : (localFormationHom K L σ) ↑((localFormationHomInv K L σ h) u) = ↑u

localFormationHomInv is a right inverse of the embedding G_L → G_K.

noncomputable def TauCeti.ClassFieldTheory.localFormationCoeffEquiv (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) : UnitsCoeff K ≃+ UnitsCoeff L

The additive equivalence on the coefficient modules underlying restriction of the units formation along L/K. It sends a unit of Kˢ to its image in Lˢ under the inverse of the chosen identification Lˢ ≃ Kˢ.

@[simp]

theorem TauCeti.ClassFieldTheory.toMul_localFormationCoeffEquiv_symm_apply (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (y : UnitsCoeff L) : Additive.toMul ((localFormationCoeffEquiv K L σ).symm y) = (Units.map (separableClosureRingEquiv K L σ).toMonoidHom) (Additive.toMul y)

The inverse of the coefficient equivalence sends a unit of Lˢ to its image in Kˢ under the chosen identification Lˢ ≃ Kˢ.

@[simp]

theorem TauCeti.ClassFieldTheory.localFormationCoeffEquiv_smul (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (g : AbsoluteGaloisGroup L) (x : UnitsCoeff K) : (localFormationCoeffEquiv K L σ) ((localFormationHom K L σ) g • x) = g • (localFormationCoeffEquiv K L σ) x

The coefficient equivalence underlying localFormationRestrict is equivariant for the embedding G_L → G_K.

noncomputable def TauCeti.ClassFieldTheory.localFormationRestrict (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) : TopRep.res (localFormationHom K L σ) (unitsFormation K).module ≅ (unitsFormation L).module

Restriction of the units formation to a finite extension. A K-embedding σ : L →ₐ[K] Kˢ identifies G_L with the open subgroup of G_K fixing σ(L). After restricting the G_K-representation (Kˢ)ˣ along this embedding, the inverse of separableClosureRingEquiv K L σ : Lˢ ≃+* Kˢ identifies it with the G_L-representation (Lˢ)ˣ. This is the coefficient comparison used to regard a finite layer over L as a layer of the formation over K.

@[simp]

theorem TauCeti.ClassFieldTheory.localFormationRestrict_hom_apply (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (x : UnitsCoeff K) : (CategoryTheory.ConcreteCategory.hom (localFormationRestrict K L σ).hom) ((unitsCoeffEquivUnitsFormation K) x) = (unitsCoeffEquivUnitsFormation L) ((localFormationCoeffEquiv K L σ) x)

localFormationRestrict sends a coefficient x ∈ (Kˢ)ˣ to its image in (Lˢ)ˣ under the inverse identification of separable closures.

@[simp]

theorem TauCeti.ClassFieldTheory.localFormationRestrict_inv_apply (K : Type) [Field K] (L : Type) [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (y : UnitsCoeff L) : (CategoryTheory.ConcreteCategory.hom (localFormationRestrict K L σ).inv) ((unitsCoeffEquivUnitsFormation L) y) = (unitsCoeffEquivUnitsFormation K) ((localFormationCoeffEquiv K L σ).symm y)

The inverse of localFormationRestrict sends a coefficient y ∈ (Lˢ)ˣ along the chosen identification Lˢ ≃ Kˢ.

@[simp]

theorem TauCeti.ClassFieldTheory.mem_level_unitsFormation_iff {K : Type} [Field K] {U : OpenSubgroup (AbsoluteGaloisGroup K)} {x : UnitsCoeff K} : (unitsCoeffEquivUnitsFormation K) x ∈ (unitsFormation K).level U ↔ ↑(Additive.toMul x) ∈ IntermediateField.fixedField ↑U

The level of an open subgroup U is the unit group of its fixed field: a unit of Kˢ lies in the level ((Kˢ)ˣ)^U exactly when it lies in the fixed field of U. Its simp priority is high so that simp uses it in preference to the generic Formation.mem_level.

Levels as unit groups of embedded fields

noncomputable def TauCeti.ClassFieldTheory.unitsLevelEquiv {K : Type} [Field K] {E : Type u_1} [Field E] [Algebra K E] (ι : E →ₐ[K] SeparableClosure K) {U : OpenSubgroup (AbsoluteGaloisGroup K)} (hU : IntermediateField.fixedField ↑U = ι.fieldRange) : Additive Eˣ ≃+ ↥((unitsFormation K).level U)

The level of an open subgroup is the unit group of its fixed field, presented as Eˣ: if the fixed field of U is the image of a K-embedding ι : E →ₐ[K] Kˢ, then ι identifies Eˣ with the level ((Kˢ)ˣ)^U of unitsFormation K. Applied to K itself and to a finite Galois extension L, it identifies the ground and top levels of the layer of L with Kˣ and Lˣ.

@[simp]

theorem TauCeti.ClassFieldTheory.unitsLevelEquiv_apply_coe {K : Type} [Field K] {E : Type u_1} [Field E] [Algebra K E] (ι : E →ₐ[K] SeparableClosure K) {U : OpenSubgroup (AbsoluteGaloisGroup K)} (hU : IntermediateField.fixedField ↑U = ι.fieldRange) (x : Additive Eˣ) : ↑((unitsLevelEquiv ι hU) x) = (unitsCoeffEquivUnitsFormation K) (Additive.ofMul ((Units.map ↑ι) (Additive.toMul x)))

unitsLevelEquiv ι hU sends a unit x of E to the unit ι x of Kˢ.

Hilbert 90 on the finite normal layers

theorem TauCeti.ClassFieldTheory.subsingleton_h1_unitsFormation {K : Type} [Field K] (L : NormalLayer (AbsoluteGaloisGroup K)) : Subsingleton ↑(L.H (unitsFormation K) 1)

Hilbert 90 on a finite normal layer of the formation of units: for open subgroups V ◁ U of G_K, H¹(U ⧸ V, ((Kˢ)ˣ)^V) = 0. In field notation, H¹(Gal(E/F), Eˣ) = 0 for the finite Galois extension E/F of fixed fields of V and U; this is the first axiom of a class formation.