Finite local reciprocity

Let K be a nonarchimedean local field and L/K a finite Galois extension, embedded in the separable closure Kˢ by ι : L →ₐ[K] Kˢ. The local class formation TauCeti.ClassFieldTheory.localClassFormation K has an abstract Artin reciprocity isomorphism ClassFormation.artinEquiv on the layer V ◁ G_K of L, from the norm quotient of the layer to the abelianized Galois group of the layer. Reading its two ends through the identifications of TauCeti.ClassFieldTheory.UnitsLayer,

• the norm quotient of the layer with Kˣ / N_{L/K}(Lˣ) (layerNormQuotientEquiv), and
• the Galois group of the layer with Gal(L/K), by restriction along ι (layerGalEquiv ι),

gives finite local reciprocity localArtinEquiv K L ι : Kˣ / N_{L/K}(Lˣ) ≃ Gal(L/K)^ab, written additively, and the local Artin map localArtinMap K L ι : Kˣ → Gal(L/K)^ab. They are the abstract Artin equivalence and Artin map of the local class formation transported along these identifications, and nothing else (localArtinEquiv_mk); in particular the kernel of the local Artin map is the norm group N_{L/K}(Lˣ) (ker_localArtinMap) and it is surjective.

The layer of L does not depend on ι, and changing ι changes layerGalEquiv ι only by an inner automorphism of Gal(L/K), which is trivial on the abelianization. So finite local reciprocity does not depend on the embedding (localArtinEquiv_eq_of_iota), and its multiplicative form normResidue K L : Kˣ / N_{L/K}(Lˣ) ≃* Gal(L/K)^ab is canonical (toAdditive_normResidue).

Main definitions

• TauCeti.ClassFieldTheory.localArtinEquiv K L ι: finite local reciprocity Kˣ / N_{L/K}(Lˣ) ≃ Gal(L/K)^ab, written additively.
• TauCeti.ClassFieldTheory.localArtinMap K L ι: the local Artin map Kˣ → Gal(L/K)^ab.
• TauCeti.ClassFieldTheory.normResidue K L: the norm residue isomorphism, the multiplicative form of finite local reciprocity.

Main results

• TauCeti.ClassFieldTheory.localArtinEquiv_mk: finite local reciprocity is the Artin map of the local class formation, read through the identifications of the layer of L.
• TauCeti.ClassFieldTheory.localArtinEquiv_eq_of_iota: finite local reciprocity does not depend on the embedding of L into Kˢ.
• TauCeti.ClassFieldTheory.ker_localArtinMap, TauCeti.ClassFieldTheory.localArtinMap_eq_zero_iff: the kernel of the local Artin map is the norm group N_{L/K}(Lˣ).
• TauCeti.ClassFieldTheory.surjective_localArtinMap: the local Artin map is surjective.
• TauCeti.ClassFieldTheory.toAdditive_normResidue: normResidue is finite local reciprocity for every embedding.
• TauCeti.ClassFieldTheory.index_normGroup_of_isMulCommutative: the norm group of a finite abelian extension has index equal to the degree.
• TauCeti.ClassFieldTheory.comap_normUnits_normGroup: for a tower E/F/K with E/K abelian, N_{F/K}⁻¹(N_{E/K}(Eˣ)) = N_{E/F}(Eˣ).

References

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

Finite local reciprocity

noncomputable def TauCeti.ClassFieldTheory.localArtinEquiv (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : Additive (Kˣ ⧸ normGroup K L) ≃+ Additive (Abelianization Gal(L/K))

Finite local reciprocity Kˣ / N_{L/K}(Lˣ) ≃ Gal(L/K)^ab for a finite Galois extension L/K of a nonarchimedean local field, embedded in the separable closure by ι: the abstract Artin reciprocity isomorphism ClassFormation.artinEquiv of the local class formation on the layer of L, read through layerNormQuotientEquiv K L and layerGalEquiv ι. It does not depend on ι (localArtinEquiv_eq_of_iota).

@[simp]

theorem TauCeti.ClassFieldTheory.localArtinEquiv_mk (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (a : Kˣ) : (localArtinEquiv K L ι) (Additive.ofMul ↑a) = (MulEquiv.toAdditive (layerGalEquiv ι).abelianizationCongr) (((localClassFormation K).artinMap (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L))) ((unitsLevelEquiv (Algebra.ofId K (SeparableClosure K)) ⋯) (Additive.ofMul a)))

Finite local reciprocity is the abstract Artin map: the image of the class of a ∈ Kˣ is the Artin symbol, for the local class formation, of a regarded as an element of the ground level of the layer of L, carried to Gal(L/K)^ab by restriction along ι.

theorem TauCeti.ClassFieldTheory.localArtinEquiv_eq_of_iota (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι ι' : L →ₐ[K] SeparableClosure K) : localArtinEquiv K L ι = localArtinEquiv K L ι'

Finite local reciprocity does not depend on the embedding of L into the separable closure: the layer of L is the same for every embedding, and two embeddings change the identification of its Galois group with Gal(L/K) by an inner automorphism, which is trivial on Gal(L/K)^ab.

The local Artin map

noncomputable def TauCeti.ClassFieldTheory.localArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : Additive Kˣ →+ Additive (Abelianization Gal(L/K))

The local Artin map Kˣ → Gal(L/K)^ab of a finite Galois extension L/K of a nonarchimedean local field: the class modulo N_{L/K}(Lˣ) followed by finite local reciprocity localArtinEquiv K L ι.

theorem TauCeti.ClassFieldTheory.localArtinMap_apply (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (a : Kˣ) : (localArtinMap K L ι) (Additive.ofMul a) = (localArtinEquiv K L ι) (Additive.ofMul ↑a)

The local Artin map is finite local reciprocity applied to the class modulo norms.

theorem TauCeti.ClassFieldTheory.localArtinMap_eq_of_iota (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι ι' : L →ₐ[K] SeparableClosure K) : localArtinMap K L ι = localArtinMap K L ι'

The local Artin map does not depend on the embedding of L into the separable closure.

@[simp]

theorem TauCeti.ClassFieldTheory.localArtinMap_eq_zero_iff (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (a : Kˣ) : (localArtinMap K L ι) (Additive.ofMul a) = 0 ↔ a ∈ normGroup K L

The kernel of the local Artin map is the norm group: the Artin symbol of a ∈ Kˣ is trivial exactly when a is a norm from L.

theorem TauCeti.ClassFieldTheory.ker_localArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : (localArtinMap K L ι).ker = Subgroup.toAddSubgroup (normGroup K L)

The kernel of the local Artin map is the norm group N_{L/K}(Lˣ), written additively.

theorem TauCeti.ClassFieldTheory.surjective_localArtinMap (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : Function.Surjective ⇑(localArtinMap K L ι)

The local Artin map is surjective.

The norm residue isomorphism

noncomputable def TauCeti.ClassFieldTheory.normResidue (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] : Kˣ ⧸ normGroup K L ≃* Abelianization Gal(L/K)

The norm residue isomorphism Kˣ / N_{L/K}(Lˣ) ≃* Gal(L/K)^ab: the multiplicative form of finite local reciprocity localArtinEquiv, for the embedding of L into the separable closure supplied by IsSepClosed.lift. Since finite local reciprocity does not depend on the embedding, it is the multiplicative form of localArtinEquiv K L ι for every ι (toAdditive_normResidue).

theorem TauCeti.ClassFieldTheory.toAdditive_normResidue (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : MulEquiv.toAdditive (normResidue K L) = localArtinEquiv K L ι

The norm residue isomorphism is finite local reciprocity for every embedding ι of L into the separable closure.

theorem TauCeti.ClassFieldTheory.normResidue_mk (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (a : Kˣ) : (normResidue K L) ↑a = Additive.toMul ((localArtinMap K L ι) (Additive.ofMul a))

The norm residue symbol of the class of a ∈ Kˣ is its local Artin symbol, for any embedding ι of L into the separable closure.

theorem TauCeti.ClassFieldTheory.normResidue_mk_eq_one_iff (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (a : Kˣ) : (normResidue K L) ↑a = 1 ↔ a ∈ normGroup K L

The norm residue symbol of the class of a ∈ Kˣ is trivial exactly when a is a norm from L.

theorem TauCeti.ClassFieldTheory.pow_natCard_abelianization_mem_normGroup (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (a : Kˣ) : a ^ Nat.card (Abelianization Gal(L/K)) ∈ normGroup K L

Powers to the order of Gal(L/K)^ab are norms: the norm residue isomorphism identifies Kˣ / N_{L/K}(Lˣ) with Gal(L/K)^ab, so a ^ #Gal(L/K)^ab ∈ N_{L/K}(Lˣ) for every a ∈ Kˣ.

theorem TauCeti.ClassFieldTheory.index_normGroup_of_isMulCommutative (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [IsMulCommutative Gal(L/K)] : (normGroup K L).index = Module.finrank K L

The norm index of a finite abelian extension: if Gal(L/K) is commutative, then [Kˣ : N_{L/K}(Lˣ)] = [L : K], since the norm residue isomorphism identifies the norm quotient with Gal(L/K)^ab, which is Gal(L/K) itself.

theorem TauCeti.ClassFieldTheory.powerSubgroup_le_normGroup_of_exponent_dvd (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {n : ℕ} (hn : Monoid.exponent Gal(L/K) ∣ n) : powerSubgroup Kˣ n ≤ normGroup K L

n-th powers are norms when n kills the Galois group. If σ ^ n = 1 for every σ ∈ Gal(L/K), then (Kˣ)ⁿ ≤ N_{L/K}(Lˣ): the norm residue isomorphism identifies Kˣ / N_{L/K}(Lˣ) with Gal(L/K)^ab, a quotient of Gal(L/K), so n kills it.

Norm groups in a tower

theorem TauCeti.ClassFieldTheory.comap_normUnits_normGroup {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [Algebra K F] (E : Type u_2) [Field E] [Algebra K E] [Algebra F E] [IsScalarTower K F E] [FiniteDimensional K E] [FiniteDimensional F E] [IsAbelianGalois K E] : Subgroup.comap (Algebra.normUnits K) (normGroup K E) = normGroup F E

Norm groups in a tower of abelian extensions. For finite extensions E/F/K of a nonarchimedean local field K with E/K abelian, an element of Fˣ is a norm from E exactly when its norm to K is a norm from E: N_{F/K}⁻¹(N_{E/K}(Eˣ)) = N_{E/F}(Eˣ).