Frobenius elements of number fields and their action on square roots

For an extension L/K of number fields and a prime Q of 𝓞 L, an arithmetic Frobenius at Q is an automorphism σ : L ≃ₐ[K] L satisfying σ x ≡ x ^ #(𝓞 K ⧸ Q ∩ 𝓞 K) (mod Q) for every x : 𝓞 L. The exponent is the cardinality of the base residue ring, not the absolute norm of Q.

This file specializes Mathlib's Frobenius API to number fields:

• Frobenius elements exist at every nonzero prime in a Galois extension. The rational-prime form uses the base ring ℤ, with exponent p, whereas the relative form at K = ℚ uses the carrier 𝓞 ℚ.
• At an unramified prime, two Frobenius automorphisms coincide. This conditional uniqueness requires no Galois hypothesis on the extension.
• An isomorphism of extensions transports the Frobenius condition to the matching ideal.

The square-root formulas work in any characteristic-zero field. At an ideal above an odd prime p, a Frobenius sends a square root of an integer d with p ∤ d to legendreSym p d times that root. At an ideal above 2, for d ≡ 1 (mod 4), it fixes the root exactly when d ≡ 1 (mod 8) and negates it otherwise. These formulas describe Frobenius on every generator of a multiquadratic field.

Main results

• NumberField.exists_isArithFrobAt: a relative Frobenius exists at every nonzero prime in a Galois extension of number fields.
• NumberField.exists_isArithFrobAt_int_of_liesOver: a ℤ-carrier Frobenius exists at every prime above a rational prime.
• AlgEquiv.isArithFrobAt_autCongr: an isomorphism of extensions transports Frobenius.
• NumberField.isArithFrobAt_eq_of_isUnramifiedAt and NumberField.subsingleton_isArithFrobAt: uniqueness at an unramified prime.
• NumberField.isArithFrobAt_apply_sqrt and NumberField.isArithFrobAt_apply_sqrt_eq_self_iff: the odd-prime square-root action and its fixing criterion.
• TauCeti.isArithFrobAt_apply_sqrt_eq_self_iff_mod_eight and TauCeti.isArithFrobAt_apply_sqrt_two: the square-root action at 2.

theorem NumberField.exists_isArithFrobAt (K : Type u_1) [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (Q : Ideal (RingOfIntegers L)) [Q.IsPrime] (hQ : Q ≠ ⊥) : ∃ (σ : Gal(L/K)), IsArithFrobAt (RingOfIntegers K) σ Q

Relative Frobenius elements exist. For a finite Galois extension L/K of number fields and a nonzero prime Q of 𝓞 L, some σ ∈ Gal(L/K) is an arithmetic Frobenius at Q.

theorem NumberField.exists_isArithFrobAt_int_of_liesOver {K : Type u_1} [Field K] [NumberField K] [IsGalois ℚ K] {p : ℕ} [Fact (Nat.Prime p)] (Q : Ideal (RingOfIntegers K)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})] : ∃ (σ : Gal(K/ℚ)), IsArithFrobAt ℤ σ Q

A Frobenius relative to the base ring ℤ exists at every prime of 𝓞 K lying over the rational prime (p); its exponent is therefore p. This is distinct from exists_isArithFrobAt ℚ, whose base-ring carrier is 𝓞 ℚ rather than ℤ.

theorem AlgEquiv.isArithFrobAt_autCongr {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Algebra K L] [Field L'] [Algebra K L'] (e : L ≃ₐ[K] L') {Q : Ideal (NumberField.RingOfIntegers L)} {σ : Gal(L/K)} (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) : IsArithFrobAt (NumberField.RingOfIntegers K) (e.autCongr σ) (Ideal.comap (NumberField.RingOfIntegers.mapAlgEquiv e).symm Q)

A Frobenius travels along an isomorphism of extensions. If σ is an arithmetic Frobenius at Q, then AlgEquiv.autCongr e σ is one at the prime of 𝓞 L' matching Q.

Uniqueness at unramified primes

theorem NumberField.isArithFrobAt_eq_of_isUnramifiedAt {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField L] [Algebra K L] {σ τ : Gal(L/K)} {Q : Ideal (RingOfIntegers L)} [Q.IsPrime] [Algebra.IsUnramifiedAt (RingOfIntegers K) Q] (hσ : IsArithFrobAt (RingOfIntegers K) σ Q) (hτ : IsArithFrobAt (RingOfIntegers K) τ Q) : σ = τ

At an unramified prime of 𝓞 L, two arithmetic Frobenius automorphisms of an extension L/K of number fields coincide. No normality hypothesis is needed.

This is a conditional uniqueness statement and makes no existence assertion, so Q need not be assumed nonzero.

instance NumberField.subsingleton_isArithFrobAt {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField L] [Algebra K L] {Q : Ideal (RingOfIntegers L)} [Q.IsPrime] [Algebra.IsUnramifiedAt (RingOfIntegers K) Q] : Subsingleton { σ : Gal(L/K) // IsArithFrobAt (RingOfIntegers K) σ Q }

The Frobenius elements at an unramified prime form a subsingleton.

theorem NumberField.isArithFrobAt_apply_sqrt {K : Type u_1} [Field K] [CharZero K] {p : ℕ} [Fact (Nat.Prime p)] (hodd : p ≠ 2) {d : ℤ} (hd : ¬↑p ∣ d) {x : K} (hx : x ^ 2 = (algebraMap ℤ K) d) (Q : Ideal (RingOfIntegers K)) [Q.LiesOver (Ideal.span {↑p})] {σ : Gal(K/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : σ x = legendreSym p d • x

A Frobenius acts on square roots by the Legendre symbol. Let K be a characteristic-zero field, p an odd prime, and σ : K ≃ₐ[ℚ] K an arithmetic Frobenius at an ideal Q of 𝓞 K above p. If x ∈ K satisfies x² = d for an integer d with p ∤ d, then

σ x = legendreSym p d • x:

the Frobenius fixes √d when d is a quadratic residue mod p and negates it otherwise.

theorem NumberField.isArithFrobAt_apply_sqrt_eq_self_iff {K : Type u_1} [Field K] [CharZero K] {p : ℕ} [Fact (Nat.Prime p)] (hodd : p ≠ 2) {d : ℤ} (hd : ¬↑p ∣ d) {x : K} (hx : x ^ 2 = (algebraMap ℤ K) d) (Q : Ideal (RingOfIntegers K)) [Q.LiesOver (Ideal.span {↑p})] {σ : Gal(K/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : σ x = x ↔ legendreSym p d = 1

A Frobenius fixes √d iff d is a quadratic residue mod p. Under the hypotheses of NumberField.isArithFrobAt_apply_sqrt, σ x = x exactly when legendreSym p d = 1 (the other case being σ x = -x, legendreSym p d = -1). The ambient field only needs characteristic zero.

Frobenius on square roots at 2

For d ≡ 1 (mod 4), an arithmetic Frobenius at a prime above 2 fixes a square root of d exactly when d ≡ 1 (mod 8), and negates it when d ≡ 5 (mod 8). The ambient field need not be quadratic, so the result applies to each generator of a multiquadratic field.

The two roots have identical reductions in characteristic two. Instead one uses the algebraic integer (1 + √d) / 2, whose conjugate is 1 - (1 + √d) / 2; their difference has odd square and hence is nonzero modulo the prime. This is the dyadic counterpart of the Legendre-symbol formula for Frobenius at odd primes, and supplies its missing local input at an odd discriminant.

The classical quadratic splitting criterion is described in D. A. Cox, Primes of the Form x² + ny², §5.A.

theorem TauCeti.isArithFrobAt_apply_sqrt_eq_self_iff_mod_eight {K : Type u_1} [Field K] [CharZero K] {d : ℤ} {x : K} (hx : x ^ 2 = (algebraMap ℤ K) d) (hd : d % 4 = 1) (Q : Ideal (NumberField.RingOfIntegers K)) [Q.LiesOver (Ideal.span {2})] {σ : Gal(K/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : σ x = x ↔ d % 8 = 1

At a prime above 2, Frobenius fixes √d exactly when d ≡ 1 (mod 8), provided d ≡ 1 (mod 4). This works in any characteristic-zero field containing the chosen square root.

theorem TauCeti.isArithFrobAt_apply_sqrt_two {K : Type u_1} [Field K] [CharZero K] {d : ℤ} {x : K} (hx : x ^ 2 = (algebraMap ℤ K) d) (hd : d % 4 = 1) (Q : Ideal (NumberField.RingOfIntegers K)) [Q.LiesOver (Ideal.span {2})] {σ : Gal(K/ℚ)} (hσ : IsArithFrobAt ℤ σ Q) : σ x = if d % 8 = 1 then x else -x

At a prime above 2, Frobenius fixes square roots of integers congruent to 1 modulo 8 and negates square roots of integers congruent to 5 modulo 8.