The layer of a finite Galois extension in the formation of units

Let L/K be a finite Galois extension. Every K-embedding ι : L →ₐ[K] Kˢ into the separable closure has the same image, so the subgroup of G_K = Gal(Kˢ/K) fixing it does not depend on ι: it is the open normal subgroup TauCeti.fixingOpenNormalSubgroup K L, the fixing subgroup of the normal closure of L in Kˢ, equal to TauCeti.galoisOpenNormalSubgroup K L ι for every ι. Its layer V ◁ G_K in the formation unitsFormation K of (Kˢ)ˣ is the abstract counterpart of L/K, and this file identifies its two ends with the concrete objects of finite class field theory:

• the Galois group G_K ⧸ V of the layer is Gal(L/K) (layerGalEquiv ι), through restriction along ι (TauCeti.quotientFixingSubgroupFieldRangeEquiv); another embedding changes this identification by an inner automorphism of Gal(L/K) (layerGalEquiv_comp), so its abelianization does not depend on ι (abelianizationCongr_layerGalEquiv);
• the ground and top levels of the layer are Kˣ and Lˣ (TauCeti.ClassFieldTheory.unitsLevelEquiv), the norm of the layer is the field norm N_{L/K} (norm_unitsLevelEquiv), and so the norm quotient of the layer is Kˣ / N_{L/K}(Lˣ) (layerNormQuotientEquiv);
• the layer cohomology is ordinary Galois cohomology of L/K with coefficients in Lˣ (layerCohomologyEquiv).

These are the two identifications through which the abstract Artin map of a class formation on unitsFormation K becomes the norm-residue map Kˣ / N_{L/K}(Lˣ) ≃ Gal(L/K)^ab of finite local reciprocity. Nothing here uses that K is local.

The norm computation is done more generally, for the level of an arbitrary finite subextension ι : E →ₐ[K] Kˢ, with no normality assumption: the norm Formation.levelNorm from that level to the level of G_K is the field norm N_{E/K} (levelNorm_unitsLevelEquiv). The norm of the layer of L is the field norm N_{L/K} (norm_unitsLevelEquiv), the case E = L, because the norm of a layer is Formation.levelNorm between its top and ground levels (TauCeti.ClassFieldTheory.NormalLayer.toAddMonoidHom_norm). The non-normal case is needed for the norm functoriality of the absolute local Artin map, where the ground level of a restricted layer is cut out by a subextension that need not be normal.

Main definitions

• TauCeti.ClassFieldTheory.layerGalEquiv ι: the Galois group of the layer is Gal(L/K).
• TauCeti.ClassFieldTheory.layerNormQuotientEquiv K L: the norm quotient of the layer is Kˣ / N_{L/K}(Lˣ).
• TauCeti.ClassFieldTheory.layerCohomologyEquiv ι: the cohomology of the layer is the concrete Galois cohomology of L/K with coefficients in Lˣ.

Main results

• TauCeti.ClassFieldTheory.fixedField_top_ofOpenNormal_fixingOpenNormalSubgroup: the top level of the layer is cut out by the image of any embedding of L, so that TauCeti.ClassFieldTheory.unitsLevelEquiv identifies it with Lˣ.
• TauCeti.ClassFieldTheory.eq_top_of_fixedField_toSubgroup_eq: the only open subgroup of G_K with fixed field K is G_K.
• TauCeti.ClassFieldTheory.abelianizationCongr_layerGalEquiv: the identification of the abelianized Galois group does not depend on the embedding.
• TauCeti.ClassFieldTheory.levelNorm_unitsLevelEquiv: for a finite extension E/K embedded in Kˢ, not necessarily normal, the norm Formation.levelNorm from the level of Gal(Kˢ/E) to the level of G_K is the field norm N_{E/K}.
• TauCeti.ClassFieldTheory.norm_unitsLevelEquiv: in particular, the norm of the layer of L is the field norm N_{L/K}.
• TauCeti.ClassFieldTheory.unitsLevelEquiv_mem_normSubgroup_iff: an element of Kˣ lies in the norm subgroup of the layer exactly when it is a field norm from L.

References

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

The ground and top levels of the layer

theorem TauCeti.ClassFieldTheory.fixedField_toSubgroup_top_eq_fieldRange (K : Type) [Field K] : IntermediateField.fixedField ↑⊤ = (Algebra.ofId K (SeparableClosure K)).fieldRange

The fixed field of the whole group G_K is K, the image of the structure map K →ₐ[K] Kˢ. This is the hypothesis under which unitsLevelEquiv identifies the level ((Kˢ)ˣ)^{G_K} with Kˣ.

theorem TauCeti.ClassFieldTheory.eq_top_of_fixedField_toSubgroup_eq {K : Type} [Field K] {W : OpenSubgroup (AbsoluteGaloisGroup K)} (h : IntermediateField.fixedField ↑W = (Algebra.ofId K (SeparableClosure K)).fieldRange) : W = ⊤

The only open subgroup of G_K whose fixed field is K is G_K itself.

theorem TauCeti.ClassFieldTheory.fixedField_ground_ofOpenNormal (K : Type) [Field K] (V : OpenNormalSubgroup (AbsoluteGaloisGroup K)) : IntermediateField.fixedField ↑(NormalLayer.ofOpenNormal V).ground = (Algebra.ofId K (SeparableClosure K)).fieldRange

The fixed field of the ground subgroup G_K of a layer V ◁ G_K is K, the image of the structure map K →ₐ[K] Kˢ. This is the hypothesis under which unitsLevelEquiv identifies the ground level of such a layer with Kˣ.

theorem TauCeti.ClassFieldTheory.fixedField_top_ofOpenNormal_fixingOpenNormalSubgroup {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : IntermediateField.fixedField ↑(NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).top = ι.fieldRange

The fixed field of the top subgroup of the layer of a finite Galois extension L/K is the image of L under any K-embedding ι. This is the hypothesis under which unitsLevelEquiv identifies the top level of the layer with Lˣ.

The Galois group of the layer

noncomputable def TauCeti.ClassFieldTheory.layerGalEquiv {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).Gal ≃* Gal(L/K)

The Galois group of the layer of a finite Galois extension L/K is Gal(L/K): the class of σ ∈ G_K in G_K ⧸ V, for V = fixingOpenNormalSubgroup K L, is sent to the restriction ι.restrictNormalHom σ of σ along the embedding ι (layerGalEquiv_mk). It is TauCeti.quotientFixingSubgroupFieldRangeEquiv K L ι read on the layer. Another embedding changes this identification by an inner automorphism (layerGalEquiv_comp).

@[simp]

theorem TauCeti.ClassFieldTheory.layerGalEquiv_mk {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (σ : ↥(NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).ground) : (layerGalEquiv ι) ↑σ = ι.restrictNormalHom ↑σ

layerGalEquiv ι sends the class of σ ∈ G_K to the restriction of σ along ι.

theorem TauCeti.ClassFieldTheory.layerGalEquiv_symm_restrictNormalHom {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (σ : AbsoluteGaloisGroup K) : (layerGalEquiv ι).symm (ι.restrictNormalHom σ) = (NormalLayer.galOfOpenNormalEquiv (fixingOpenNormalSubgroup K L)).symm ↑σ

(layerGalEquiv ι).symm sends the restriction of σ ∈ G_K along ι to the class of σ in G_K ⧸ V, read in the Galois group of the layer.

theorem TauCeti.ClassFieldTheory.coe_autCongr_layerGalEquiv_mk_apply {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (u : ↥(NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).ground) (x : ↥ι.fieldRange) : ↑((ι.equivFieldRange.autCongr ((layerGalEquiv ι) ↑u)) x) = ↑u ↑x

Read on the image of ι through ι.equivFieldRange, layerGalEquiv ι sends the class of u to the restriction of u to the image: its value at x is u x.

theorem TauCeti.ClassFieldTheory.layerGalEquiv_comp {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (τ : Gal(L/K)) (γ : (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).Gal) : (layerGalEquiv (ι.comp ↑τ)) γ = τ⁻¹ * (layerGalEquiv ι) γ * τ

Changing the embedding conjugates the identification of the Galois group: precomposing ι with τ ∈ Gal(L/K) changes layerGalEquiv by the inner automorphism of τ.

theorem TauCeti.ClassFieldTheory.abelianizationCongr_layerGalEquiv {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι ι' : L →ₐ[K] SeparableClosure K) : (layerGalEquiv ι).abelianizationCongr = (layerGalEquiv ι').abelianizationCongr

The abelianized Galois group of the layer is Gal(L/K)^ab independently of the embedding: the identifications layerGalEquiv ι for different ι differ by inner automorphisms, which become trivial on abelianizations.

The norm from the level of a finite extension

theorem TauCeti.ClassFieldTheory.levelNorm_unitsLevelEquiv {K : Type} [Field K] {E : Type u_1} [Field E] [Algebra K E] (ι : E →ₐ[K] SeparableClosure K) {W W₀ : OpenSubgroup (AbsoluteGaloisGroup K)} (h : W ≤ W₀) (hW : IntermediateField.fixedField ↑W = ι.fieldRange) (hW₀ : IntermediateField.fixedField ↑W₀ = (Algebra.ofId K (SeparableClosure K)).fieldRange) (y : Additive Eˣ) : ((unitsFormation K).levelNorm h) ((unitsLevelEquiv ι hW) y) = (unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) hW₀) (Additive.ofMul ((Algebra.normUnits K) (Additive.toMul y)))

The norm from the level of a finite extension is the field norm: if the fixed field of the open subgroup W is the image of a K-embedding ι : E →ₐ[K] Kˢ of an extension E/K (finite, as it is isomorphic to that fixed field), and that of W₀ ⊇ W is K, then under the identifications unitsLevelEquiv of the two levels with Eˣ and Kˣ, the norm Formation.levelNorm from ((Kˢ)ˣ)^W to ((Kˢ)ˣ)^{W₀} is N_{E/K}. The extension E/K need not be normal.

The norm quotient of the layer

@[simp]

theorem TauCeti.ClassFieldTheory.rep_ρ_unitsLevelEquiv {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (γ : (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).Gal) (y : Additive Lˣ) : ((((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).groundRep (unitsFormation K)).ofQuotient (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).relativeTop) γ) ((unitsLevelEquiv ι ⋯) y) = (unitsLevelEquiv ι ⋯) (Additive.ofMul ((layerGalEquiv ι) γ • Additive.toMul y))

The Galois action on the top level of the layer is the action of Gal(L/K) on Lˣ, through layerGalEquiv ι and unitsLevelEquiv ι.

theorem TauCeti.ClassFieldTheory.norm_unitsLevelEquiv {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (y : Additive Lˣ) : ((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).norm (unitsFormation K)) ((unitsLevelEquiv ι ⋯) y) = (unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul ((Algebra.normUnits K) (Additive.toMul y)))

The norm of the layer is the field norm: under the identifications of its top and ground levels with Lˣ and Kˣ, the norm N_{G_K/V} of the layer of L is N_{L/K}. This is the case E = L of levelNorm_unitsLevelEquiv, since the norm of a layer is Formation.levelNorm between its top and ground levels (NormalLayer.toAddMonoidHom_norm).

theorem TauCeti.ClassFieldTheory.unitsLevelEquiv_mem_normSubgroup_iff (K : Type) [Field K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (a : Kˣ) : (unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul a) ∈ (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).normSubgroup (unitsFormation K) ↔ a ∈ normGroup K L

The norm subgroup of the layer is the norm group N_{L/K}(Lˣ): an element of Kˣ lies in the norm subgroup of the layer of L exactly when it is the field norm of a unit of L.

noncomputable def TauCeti.ClassFieldTheory.layerNormQuotientEquiv (K : Type) [Field K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : Additive (Kˣ ⧸ normGroup K L) ≃+ (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).NormQuotient (unitsFormation K)

The norm quotient of the layer of L is Kˣ / N_{L/K}(Lˣ): the identification unitsLevelEquiv of the ground level of the layer with Kˣ descends to the quotients by N_{L/K}(Lˣ) and by the norm subgroup of the layer (unitsLevelEquiv_mem_normSubgroup_iff).

@[simp]

theorem TauCeti.ClassFieldTheory.layerNormQuotientEquiv_mk {K : Type} [Field K] {L : Type u_1} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (a : Kˣ) : (layerNormQuotientEquiv K L) (Additive.ofMul ↑a) = ((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).normQuotientMk (unitsFormation K)) ((unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul a))

layerNormQuotientEquiv K L sends the class of a ∈ Kˣ to the class of a in the norm quotient of the layer.

Cohomology

noncomputable def TauCeti.ClassFieldTheory.layerCoefficientEquiv {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : ↑((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).rep (unitsFormation K)) ≃ₗ[ℤ] ↑(Rep.ofMulDistribMulAction Gal(L/K) Lˣ)

The coefficient identification from the representation of the layer of L to the standard Galois representation on Lˣ.

@[simp]

theorem TauCeti.ClassFieldTheory.layerCoefficientEquiv_unitsLevelEquiv {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (y : Additive Lˣ) : (layerCoefficientEquiv ι) ((unitsLevelEquiv ι ⋯) y) = y

The coefficient identification inverts unitsLevelEquiv.

theorem TauCeti.ClassFieldTheory.layerCoefficientEquiv_apply_coe {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (x : ↑((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).rep (unitsFormation K))) : Additive.ofMul ((Units.map ↑ι) (Additive.toMul (Rep.toAdditive ((layerCoefficientEquiv ι) x)))) = (unitsCoeffEquivUnitsFormation K).symm ↑x

Reading the concrete coefficient of a layer element through ι recovers its value in the separable closure.

theorem TauCeti.ClassFieldTheory.layerCoefficientEquiv_ρ {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (γ : (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).Gal) (x : ↑((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).rep (unitsFormation K))) : (layerCoefficientEquiv ι) ((((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).rep (unitsFormation K)).ρ γ) x) = ((Rep.ofMulDistribMulAction Gal(L/K) Lˣ).ρ ((layerGalEquiv ι) γ)) ((layerCoefficientEquiv ι) x)

The coefficient identification intertwines the layer action with the concrete Galois action.

noncomputable def TauCeti.ClassFieldTheory.layerCoefficientHom {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : Rep.res (↑(layerGalEquiv ι).symm) ((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).rep (unitsFormation K)) ⟶ Rep.ofMulDistribMulAction Gal(L/K) Lˣ

The morphism of representations underlying layerCohomologyEquiv.

@[simp]

theorem TauCeti.ClassFieldTheory.layerCoefficientHom_apply {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (x : ↑((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).rep (unitsFormation K))) : (Rep.Hom.hom (layerCoefficientHom ι)) x = (layerCoefficientEquiv ι) x

The representation morphism underlying the layer comparison is the coefficient identification.

noncomputable def TauCeti.ClassFieldTheory.layerCohomologyEquiv {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (n : ℕ) : ↑((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).H (unitsFormation K) n) ≃+ ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) n)

The cohomology of the layer of L is the ordinary Galois cohomology of L/K: restriction along ι identifies the layer Galois group with Gal(L/K), while unitsLevelEquiv identifies the layer coefficients with Lˣ.

theorem TauCeti.ClassFieldTheory.layerCohomologyEquiv_apply {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (n : ℕ) (x : ↑((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).H (unitsFormation K) n)) : (layerCohomologyEquiv ι n) x = (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (↑(layerGalEquiv ι).symm) (layerCoefficientHom ι) n)) x

layerCohomologyEquiv is induced by the concrete group and coefficient identifications.

theorem TauCeti.ClassFieldTheory.layerCoefficientEquiv_groundLevel {K : Type} [Field K] {L : Type} [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (a : Kˣ) : Rep.toAdditive ((layerCoefficientEquiv ι) ↑(((NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L)).groundLevelEquiv (unitsFormation K)).symm ((unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul a)))) = Additive.ofMul ((Units.map ↑(algebraMap K L)) a)

A ground-field unit, viewed in the layer and then in Lˣ, is its image under the algebra map K → L.