Finite global reciprocity

Let K be a number field and L/K a finite Galois extension, embedded in the separable closure Kˢ by ι : L →ₐ[K] Kˢ. The global class formation globalClassFormation K, whose invariant is the sum of the local invariants, 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 identification of the norm quotient of the layer with C_K / N_{L/K}(C_L) (globalLayerNormQuotientEquiv), and
• the identification of the Galois group of the layer with Gal(L/K), by restriction along ι (layerGalEquiv ι),

gives finite global reciprocity globalArtinEquiv K L ι : C_K / N_{L/K}(C_L) ≃ Gal(L/K)^ab, written additively, and the global Artin map globalArtinMap K L ι : C_K → Gal(L/K)^ab. They are the abstract Artin equivalence and Artin map of the global class formation transported along these identifications, and nothing else (globalArtinEquiv_mk). In particular the kernel of the global Artin map is the idele-class norm group N_{L/K}(C_L) (ker_globalArtinMap), the map is surjective, and, being defined on C_K = 𝕀_K / Kˣ, it kills the classes of principal ideles (globalArtinMap_principal), which is the reciprocity law in idelic form. For an abelian extension, the norm index [C_K : N_{L/K}(C_L)] is the degree [L : K] (card_ideleClassNormQuotient), and the global Artin map, read in Gal(L/K) itself, is ideleClassArtinMap K L : C_K →* Gal(L/K), surjective with kernel N_{L/K}(C_L).

As in the local case, 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 global reciprocity does not depend on the embedding (globalArtinEquiv_eq_of_iota).

The global Artin maps of the different finite Galois extensions are compatible in towers. The global class formation has an absolute Artin map C_K → G_K^ab whose finite restrictions are the Artin maps of its layers (ClassFormation.abelianizationRestrict_absoluteArtinMap). So if g ∈ G_K represents the absolute Artin symbol of c ∈ C_K, then the global Artin symbol of c in Gal(L/K)^ab is the class of the restriction of g to L, for every L (globalArtinMap_eq_of_mk_eq_absoluteArtinMap). In particular, for a K-embedding M → L of finite Galois extensions, restricting the global Artin symbol from L to M gives the global Artin symbol of M/K (globalArtinMap_comp).

Main definitions

• TauCeti.ClassFieldTheory.globalArtinEquiv K L ι: finite global reciprocity C_K / N_{L/K}(C_L) ≃ Gal(L/K)^ab, written additively.
• TauCeti.ClassFieldTheory.globalArtinMap K L ι: the global Artin map C_K → Gal(L/K)^ab.
• TauCeti.ClassFieldTheory.ideleClassArtinMap K L: the global Artin map C_K →* Gal(L/K) of a finite abelian extension.

Main results

• TauCeti.ClassFieldTheory.globalArtinEquiv_mk: finite global reciprocity is the Artin map of the global class formation, read through the identifications of the layer of L.
• TauCeti.ClassFieldTheory.globalArtinEquiv_eq_of_iota: finite global reciprocity does not depend on the embedding of L into Kˢ.
• TauCeti.ClassFieldTheory.ker_globalArtinMap, TauCeti.ClassFieldTheory.globalArtinMap_eq_zero_iff: the kernel of the global Artin map is the idele-class norm group N_{L/K}(C_L).
• TauCeti.ClassFieldTheory.surjective_globalArtinMap: the global Artin map is surjective.
• TauCeti.ClassFieldTheory.globalArtinMap_principal: the global Artin map kills principal ideles.
• TauCeti.ClassFieldTheory.globalArtinMap_eq_of_mk_eq_absoluteArtinMap: the global Artin symbol in Gal(L/K)^ab is the restriction of any representative of the absolute Artin symbol.
• TauCeti.ClassFieldTheory.globalArtinMap_comp: the global Artin map is compatible with restriction to a Galois subextension.
• TauCeti.ClassFieldTheory.card_ideleClassNormQuotient: the norm index theorem [C_K : N_{L/K}(C_L)] = [L : K] for a finite abelian extension.
• TauCeti.ClassFieldTheory.of_ideleClassArtinMap, TauCeti.ClassFieldTheory.ker_ideleClassArtinMap, TauCeti.ClassFieldTheory.ideleClassArtinMap_surjective: the global Artin map of an abelian extension is globalArtinMap, has kernel N_{L/K}(C_L), and is surjective.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §4.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §5 (including the compatibility of the norm residue symbol in towers).
• J. S. Milne, Class Field Theory, v4.03, Chapter VIII.

Finite global reciprocity

noncomputable def TauCeti.ClassFieldTheory.globalArtinEquiv (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : Additive (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K ⧸ (↑(GlobalNumberFields.ideleClassNormMap K L)).range) ≃+ Additive (Abelianization Gal(L/K))

Finite global reciprocity C_K / N_{L/K}(C_L) ≃ Gal(L/K)^ab for a finite Galois extension L/K of number fields, embedded in the separable closure of K by ι: the abstract Artin reciprocity isomorphism ClassFormation.artinEquiv of the global class formation on the layer of L, read through globalLayerNormQuotientEquiv K L and layerGalEquiv ι. It does not depend on ι (globalArtinEquiv_eq_of_iota).

@[simp]

theorem TauCeti.ClassFieldTheory.globalArtinEquiv_mk (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (globalArtinEquiv K L ι) (Additive.ofMul ↑c) = (MulEquiv.toAdditive (layerGalEquiv ι).abelianizationCongr) (((globalClassFormation K).artinMap (NormalLayer.ofOpenNormal (fixingOpenNormalSubgroup K L))) ((NormalLayer.groundEquivOfOpenNormal (globalFormation K) (fixingOpenNormalSubgroup K L)) ((globalGroundEquiv K) (Additive.ofMul c))))

Finite global reciprocity is the abstract Artin map: the image of the class of c ∈ C_K is the Artin symbol, for the global class formation, of c 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.globalArtinEquiv_eq_of_iota (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι ι' : L →ₐ[K] SeparableClosure K) : globalArtinEquiv K L ι = globalArtinEquiv K L ι'

Finite global 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 global Artin map

noncomputable def TauCeti.ClassFieldTheory.globalArtinMap (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : Additive (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) →+ Additive (Abelianization Gal(L/K))

The global Artin map C_K → Gal(L/K)^ab of a finite Galois extension L/K of number fields: the class modulo N_{L/K}(C_L) followed by finite global reciprocity globalArtinEquiv K L ι.

theorem TauCeti.ClassFieldTheory.globalArtinMap_apply (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (globalArtinMap K L ι) (Additive.ofMul c) = (globalArtinEquiv K L ι) (Additive.ofMul ↑c)

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

theorem TauCeti.ClassFieldTheory.globalArtinMap_eq_of_iota (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι ι' : L →ₐ[K] SeparableClosure K) : globalArtinMap K L ι = globalArtinMap K L ι'

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

@[simp]

theorem TauCeti.ClassFieldTheory.globalArtinMap_eq_zero_iff (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (globalArtinMap K L ι) (Additive.ofMul c) = 0 ↔ c ∈ (↑(GlobalNumberFields.ideleClassNormMap K L)).range

The kernel of the global Artin map is the idele-class norm group: the Artin symbol of c ∈ C_K is trivial exactly when c is the norm of an idele class of L.

theorem TauCeti.ClassFieldTheory.ker_globalArtinMap (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : (globalArtinMap K L ι).ker = Subgroup.toAddSubgroup (↑(GlobalNumberFields.ideleClassNormMap K L)).range

The kernel of the global Artin map is the idele-class norm group N_{L/K}(C_L), written additively.

theorem TauCeti.ClassFieldTheory.surjective_globalArtinMap (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) : Function.Surjective ⇑(globalArtinMap K L ι)

The global Artin map is surjective.

@[simp]

theorem TauCeti.ClassFieldTheory.globalArtinMap_principal (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (x : Kˣ) : (globalArtinMap K L ι) (Additive.ofMul ↑((NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) x)) = 0

The global Artin map kills principal ideles: the class in C_K of the principal idele of x ∈ Kˣ is trivial, so its Artin symbol vanishes. This is the reciprocity law in idelic form.

Compatibility in towers

theorem TauCeti.ClassFieldTheory.globalArtinMap_eq_of_mk_eq_absoluteArtinMap (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) {c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K} (g : AbsoluteGaloisGroup K) (hg : Additive.ofMul ↑g = (globalClassFormation K).absoluteArtinMap ((globalGroundEquiv K) (Additive.ofMul c))) : (globalArtinMap K L ι) (Additive.ofMul c) = Additive.ofMul (Abelianization.of (ι.restrictNormalHom g))

The global Artin map through a representative of the absolute Artin symbol. If g ∈ G_K represents the absolute Artin symbol of c ∈ C_K for the global class formation, then for every finite Galois extension L/K, embedded in the separable closure by ι, the Artin symbol of c in Gal(L/K)^ab is the class of the restriction of g along ι.

theorem TauCeti.ClassFieldTheory.globalArtinMap_comp (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {M : Type u_2} [Field M] [NumberField M] [Algebra K M] [IsGalois K M] (f : M →ₐ[K] L) (ι : L →ₐ[K] SeparableClosure K) : (MonoidHom.toAdditive (Abelianization.map f.restrictNormalHom)).comp (globalArtinMap K L ι) = globalArtinMap K M (ι.comp f)

The global Artin map is compatible in towers: for a K-embedding f : M → L of a finite Galois extension M/K into L, restricting the global Artin symbol in Gal(L/K)^ab to M along f gives the global Artin symbol in Gal(M/K)^ab.

The norm index of an abelian extension

theorem TauCeti.ClassFieldTheory.card_ideleClassNormQuotient (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] : Nat.card (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K ⧸ (↑(GlobalNumberFields.ideleClassNormMap K L)).range) = Module.finrank K L

The norm index theorem: for a finite abelian extension L/K of number fields, [C_K : N_{L/K}(C_L)] = [L : K], since finite global reciprocity identifies the norm quotient with Gal(L/K)^ab, which is Gal(L/K) itself.

The global Artin map of an abelian extension

noncomputable def TauCeti.ClassFieldTheory.ideleClassArtinMap (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K →* Gal(L/K)

The global Artin map C_K →* Gal(L/K) of a finite abelian extension L/K of number fields: the global Artin map globalArtinMap, read in Gal(L/K) itself, which is its own abelianization. It is characterized by of_ideleClassArtinMap, for every embedding of L into the separable closure.

theorem TauCeti.ClassFieldTheory.of_ideleClassArtinMap (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] (ι : L →ₐ[K] SeparableClosure K) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : Abelianization.of ((ideleClassArtinMap K L) c) = Additive.toMul ((globalArtinMap K L ι) (Additive.ofMul c))

The global Artin map of an abelian extension is globalArtinMap: the class in Gal(L/K)^ab of the Artin symbol of c ∈ C_K is the global Artin symbol of c, for every embedding ι of L into the separable closure.

theorem TauCeti.ClassFieldTheory.ker_ideleClassArtinMap (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] : (ideleClassArtinMap K L).ker = (↑(GlobalNumberFields.ideleClassNormMap K L)).range

The kernel of the global Artin map of an abelian extension is the idele-class norm group N_{L/K}(C_L).

theorem TauCeti.ClassFieldTheory.ideleClassArtinMap_surjective (K : Type) [Field K] [NumberField K] (L : Type u_1) [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] : Function.Surjective ⇑(ideleClassArtinMap K L)

The global Artin map of an abelian extension is surjective.