The global Artin symbol of a prime idele is arithmetic Frobenius

Let L/K be a finite Galois extension of number fields and v a finite place of K. The prime idele class primeIdeleClass K v ∈ C_K is the class of the idele with a uniformizer of K_v at v and 1 at every other place. It is the idelic counterpart of the prime ideal v.

If v is unramified in L and σ ∈ Gal(L/K) is an arithmetic Frobenius at a prime Q of L above v, then the global Artin symbol of the class of the idele concentrated at v with component x ∈ K_vˣ is the class of σ raised to the normalized valuation of x (globalArtinMap_ofAdicCompletion_eq_of_isArithFrobAt). This combines the local–global compatibility globalArtinMap_local with the unramified local computation localArtinAt_eq_of_isArithFrobAt. In particular the Artin symbol of the prime idele class is the class of Frobenius, whichever uniformizer represents it (globalArtinMap_primeIdeleClass_eq_of_isArithFrobAt).

For L/K abelian, Gal(L/K) is its own abelianization, so this pins the Artin symbol down as an automorphism: an automorphism whose class is the Artin symbol of the class of the idele with any uniformizer of K_v at v and 1 at every other place is an arithmetic Frobenius at every prime of L above v (isArithFrobAt_of_globalArtinMap_ofAdicCompletion_eq), in particular for the prime idele class (globalArtinMap_isArithFrobAt). This is the arithmetic, rather than geometric, normalization of the global Artin map. Since a Frobenius at an unramified prime has order the residue degree, so does the Artin symbol of the prime idele class (addOrderOf_globalArtinMap_primeIdeleClass); in particular the symbol is trivial exactly when v splits completely. In a quadratic extension the symbol is the nontrivial automorphism exactly when v is inert (globalArtinMap_quadratic_prime).

Consequently the global Artin map agrees with the ideal-theoretic Artin map TauCeti.NumberFieldArithmetic.artinHomAway on the primes outside a finite set S containing the ramified ones: for an abelian L/K and v ∉ S, the Artin symbol of the prime idele class at v is the class of the value of artinHomAway at the prime v (globalArtinMap_ideal). Since a homomorphism on the ideals prime to S is determined by its values on primes, every such homomorphism whose prime values are the global Artin symbols of the prime idele classes is artinHomAway itself (eq_artinHomAway_of_globalArtinMap).

Main definitions

• TauCeti.ClassFieldTheory.primeIdeleClass K v: the idele class of a uniformizer at v.

Main results

• TauCeti.ClassFieldTheory.globalArtinMap_ofAdicCompletion_eq_of_isArithFrobAt: at an unramified place, the global Artin symbol of x ∈ K_vˣ is Frobenius to the power v(x).
• TauCeti.ClassFieldTheory.globalArtinMap_primeIdeleClass_eq_of_isArithFrobAt: the global Artin symbol of the prime idele class at an unramified place is the class of Frobenius.
• TauCeti.ClassFieldTheory.isArithFrobAt_of_globalArtinMap_ofAdicCompletion_eq: for L/K abelian, an automorphism representing the Artin symbol of the class of the idele with any uniformizer at an unramified v and 1 elsewhere is an arithmetic Frobenius at every prime of L above v.
• TauCeti.ClassFieldTheory.globalArtinMap_isArithFrobAt: the same for the prime idele class.
• TauCeti.ClassFieldTheory.addOrderOf_globalArtinMap_primeIdeleClass and globalArtinMap_primeIdeleClass_eq_zero_iff_inertiaDeg_eq_one: for L/K abelian and v unramified, the Artin symbol of the prime idele class has order the residue degree, and is trivial exactly when the residue degree is 1.
• TauCeti.ClassFieldTheory.globalArtinMap_quadratic_prime: in a quadratic extension, the Artin symbol of an unramified prime is the nontrivial automorphism exactly when the prime is inert.
• TauCeti.ClassFieldTheory.globalArtinMap_ideal: for L/K abelian, the global Artin symbol of the prime idele class at v ∉ S is the class of the ideal-theoretic Artin symbol of v.
• TauCeti.ClassFieldTheory.eq_artinHomAway_of_globalArtinMap: a homomorphism on the ideals prime to S taking the global Artin symbols of the prime idele classes at the primes outside S is the ideal-theoretic Artin map.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §5 and §7 (the idelic and the ideal-theoretic Artin symbols).
• J. S. Milne, Class Field Theory, v4.03, Chapter V, §3 and Chapter VII.

noncomputable def TauCeti.ClassFieldTheory.primeIdeleClass (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K

The prime idele class at a finite place v of a number field K: the class in the idele class group of the idele whose component at v is a chosen uniformizer of K_v and whose other components are 1. At a place unramified in a finite Galois extension its global Artin symbol does not depend on the choice (globalArtinMap_primeIdeleClass_eq_of_isArithFrobAt).

theorem TauCeti.ClassFieldTheory.exists_isUniformizer_primeIdeleClass_eq (K : Type) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ∃ (π : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ), IsUniformizer (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) π ∧ primeIdeleClass K v = (NumberField.IdeleClassGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) π

The prime idele class at v is the class of the idele concentrated at v with a uniformizer of K_v as component.

theorem TauCeti.ClassFieldTheory.globalArtinMap_ofAdicCompletion_eq_of_isArithFrobAt {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] {σ : Gal(L/K)} (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) (x : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : (globalArtinMap K L ι) (Additive.ofMul ((NumberField.IdeleClassGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) x)) = Additive.ofMul (Abelianization.of σ ^ Multiplicative.toAdd ((normalizedValuation (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x))

The global Artin symbol at an unramified place. If v is unramified at a prime Q of L above it and σ ∈ Gal(L/K) is an arithmetic Frobenius at Q, then the global Artin symbol of the class of the idele concentrated at v with component x ∈ K_vˣ is the class of σ raised to the normalized valuation of x.

theorem TauCeti.ClassFieldTheory.globalArtinMap_primeIdeleClass_eq_of_isArithFrobAt {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] {σ : Gal(L/K)} (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) : (globalArtinMap K L ι) (Additive.ofMul (primeIdeleClass K v)) = Additive.ofMul (Abelianization.of σ)

The global Artin symbol of a prime idele class is Frobenius. If v is unramified at a prime Q of L above it and σ ∈ Gal(L/K) is an arithmetic Frobenius at Q, then the global Artin symbol of the prime idele class at v is the class of σ in Gal(L/K)^ab.

theorem TauCeti.ClassFieldTheory.isArithFrobAt_of_globalArtinMap_ofAdicCompletion_eq {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] [IsMulCommutative Gal(L/K)] {π : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ} (hπ : IsUniformizer (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) π) {σ : Gal(L/K)} (hσ : (globalArtinMap K L ι) (Additive.ofMul ((NumberField.IdeleClassGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) π)) = Additive.ofMul (Abelianization.of σ)) : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q

Arithmetic Frobenius normalization of the global Artin map. For a finite abelian extension L/K of number fields and a finite place v of K unramified at a prime Q of L above it, an automorphism σ ∈ Gal(L/K) whose class is the global Artin symbol of the class of the idele with a uniformizer π of K_v at v and 1 at every other place is an arithmetic Frobenius at Q.

theorem TauCeti.ClassFieldTheory.globalArtinMap_isArithFrobAt {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] [IsMulCommutative Gal(L/K)] {σ : Gal(L/K)} (hσ : (globalArtinMap K L ι) (Additive.ofMul (primeIdeleClass K v)) = Additive.ofMul (Abelianization.of σ)) : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q

Arithmetic Frobenius normalization at the prime idele class. For a finite abelian extension L/K of number fields and a finite place v of K unramified at a prime Q of L above it, an automorphism σ ∈ Gal(L/K) whose class is the global Artin symbol of the prime idele class at v is an arithmetic Frobenius at Q.

theorem TauCeti.ClassFieldTheory.addOrderOf_globalArtinMap_primeIdeleClass {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] [IsMulCommutative Gal(L/K)] : addOrderOf ((globalArtinMap K L ι) (Additive.ofMul (primeIdeleClass K v))) = Q.inertiaDeg (NumberField.RingOfIntegers K)

The order of the Artin symbol of a prime is its residue degree. For a finite abelian extension L/K of number fields and a finite place v of K unramified at a prime Q of L above it, the global Artin symbol of the prime idele class at v has order the residue degree f(Q | v).

theorem TauCeti.ClassFieldTheory.globalArtinMap_primeIdeleClass_eq_zero_iff_inertiaDeg_eq_one {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] [IsMulCommutative Gal(L/K)] : (globalArtinMap K L ι) (Additive.ofMul (primeIdeleClass K v)) = 0 ↔ Q.inertiaDeg (NumberField.RingOfIntegers K) = 1

Splitting criterion through the Artin symbol. For a finite abelian extension L/K of number fields and a finite place v of K unramified at a prime Q of L above it, the global Artin symbol of the prime idele class at v is trivial exactly when Q has residue degree 1, that is, when v splits completely in L.

theorem TauCeti.ClassFieldTheory.globalArtinMap_quadratic_prime {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (ι : L →ₐ[K] SeparableClosure K) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Q.LiesOver v.asIdeal] [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q] (hL : Module.finrank K L = 2) {τ : Gal(L/K)} (hτ : τ ≠ 1) : (globalArtinMap K L ι) (Additive.ofMul (primeIdeleClass K v)) = Additive.ofMul (Abelianization.of τ) ↔ Q.inertiaDeg (NumberField.RingOfIntegers K) = 2

Artin symbols in a quadratic extension. Let L/K be a quadratic extension of number fields with nontrivial automorphism τ, and let v be a finite place of K unramified at a prime Q of L above it. The global Artin symbol of the prime idele class at v is the class of τ exactly when Q has residue degree 2, that is, when v is inert in L. Otherwise it is trivial (globalArtinMap_primeIdeleClass_eq_zero_iff_inertiaDeg_eq_one).

theorem TauCeti.ClassFieldTheory.globalArtinMap_ideal {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] (ι : L →ₐ[K] SeparableClosure K) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hur : ∀ v ∉ S, ∀ (Q : Ideal (NumberField.RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver v.asIdeal], Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (I : ↥(NumberFieldArithmetic.idealsAway K S)) (hI : ↑↑I = ↑v.asIdeal) : (globalArtinMap K L ι) (Additive.ofMul (primeIdeleClass K v)) = Additive.ofMul (Abelianization.of ((NumberFieldArithmetic.artinHomAway ⋯ S hur) I))

Comparison with the ideal-theoretic Artin map. For a finite abelian extension L/K of number fields, unramified outside a finite set S of finite places of K, and a finite place v whose prime ideal I is prime to S (so v ∉ S), the global Artin symbol of the prime idele class at v is the class of the value of NumberFieldArithmetic.artinHomAway at I, that is, of the arithmetic Frobenius at v.

theorem TauCeti.ClassFieldTheory.eq_artinHomAway_of_globalArtinMap {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsAbelianGalois K L] (ι : L →ₐ[K] SeparableClosure K) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hur : ∀ v ∉ S, ∀ (Q : Ideal (NumberField.RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver v.asIdeal], Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q) (φ : ↥(NumberFieldArithmetic.idealsAway K S) →* Gal(L/K)) (hφ : ∀ (I : ↥(NumberFieldArithmetic.idealsAway K S)), ∀ v ∉ S, ↑↑I = ↑v.asIdeal → (globalArtinMap K L ι) (Additive.ofMul (primeIdeleClass K v)) = Additive.ofMul (Abelianization.of (φ I))) : φ = NumberFieldArithmetic.artinHomAway ⋯ S hur

The global Artin symbols of the prime idele classes determine the ideal-theoretic Artin map. For a finite abelian extension L/K of number fields, unramified outside a finite set S of finite places of K, a homomorphism φ on the ideals prime to S whose value at each prime v ∉ S represents the global Artin symbol of the prime idele class at v is NumberFieldArithmetic.artinHomAway.