Frobenius elements on n-th roots: the power residue criterion

Let S/R be an extension of commutative rings with S a domain, Q a prime of S, and φ an arithmetic Frobenius at Q, so that φ y ≡ y ^ q (mod Q) with q = #(R ⧸ Q ∩ R). Suppose R contains an element ζ that is a primitive n-th root of unity in S, with n ∉ Q. If x ∈ S is an n-th root of a ∈ R and a ∉ Q, then

φ x = x ↔ a is an n-th power modulo Q ∩ R

(AlgHom.IsArithFrobAt.apply_eq_self_iff). This is the Frobenius description of the n-th power residue symbol: φ x = ξ x for the n-th root of unity ξ ≡ a ^ ((q - 1) / n), and ξ is trivial exactly when a is an n-th power in the residue field.

For a family of Frobenius elements σ i at primes Q i, the subgroup they generate fixes x exactly when a is an n-th power modulo every Q i ∩ R (IsArithFrobAt.forall_mem_closure_smul_eq_self_iff). This is the form in which Kummer theory detects, through Frobenius elements, whether an n-th root of a lies in a given subfield.

At n = 2 over ℤ the value ξ = ±1 is the Legendre symbol, which is AlgHom.IsArithFrobAt.apply_sqrt.

Main results

• Ideal.exists_pow_eq_mk_iff_pow_sub_one_mem: Euler's criterion in a finite residue domain R ⧸ P with n ∣ #(R ⧸ P) - 1: the class of a ∉ P is an n-th power exactly when a ^ ((#(R ⧸ P) - 1) / n) ≡ 1 (mod P).
• AlgHom.IsArithFrobAt.dvd_card_sub_one: n ∣ q - 1 when R contains a primitive n-th root of unity of S and n ∉ Q.
• AlgHom.IsArithFrobAt.sub_pow_mul_mem: φ x ≡ a ^ ((q - 1) / n) * x (mod Q) for x ^ n = a.
• AlgHom.IsArithFrobAt.apply_eq_self_iff, IsArithFrobAt.smul_eq_self_iff: a Frobenius fixes an n-th root of a exactly when a is an n-th power modulo Q ∩ R.
• IsArithFrobAt.forall_mem_closure_smul_eq_self_iff: the same for the subgroup generated by a family of Frobenius elements.

References

• J. Neukirch, Algebraic Number Theory, Chapter V, §3 (the n-th power residue symbol).
• J. S. Milne, Class Field Theory, v4.03, Chapter VII, proof of Lemma 6.3.

theorem Ideal.exists_pow_eq_mk_iff_pow_sub_one_mem {R : Type u_1} [CommRing R] {P : Ideal R} [P.IsPrime] [Finite (R ⧸ P)] {n : ℕ} (hdvd : n ∣ Nat.card (R ⧸ P) - 1) {a : R} (ha : a ∉ P) : (∃ (b : R ⧸ P), b ^ n = (Quotient.mk P) a) ↔ a ^ ((Nat.card (R ⧸ P) - 1) / n) - 1 ∈ P

Euler's criterion in a finite residue domain. Let P be a prime of R with finite quotient and n ∣ #(R ⧸ P) - 1. For a ∉ P, the class of a is an n-th power in R ⧸ P exactly when a ^ ((#(R ⧸ P) - 1) / n) ≡ 1 (mod P).

theorem AlgHom.IsArithFrobAt.dvd_card_sub_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} [IsDomain S] (H : φ.IsArithFrobAt Q) {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ((algebraMap R S) ζ) n) (hn : ↑n ∉ Q) : n ∣ Nat.card (R ⧸ Ideal.under R Q) - 1

If R contains an element that is a primitive n-th root of unity in the domain S and n ∉ Q, then n divides q - 1, where q = #(R ⧸ Q ∩ R) is the exponent of a Frobenius at Q.

theorem AlgHom.IsArithFrobAt.sub_pow_mul_mem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} (H : φ.IsArithFrobAt Q) {n : ℕ} (hdvd : n ∣ Nat.card (R ⧸ Ideal.under R Q) - 1) {x : S} {a : R} (hx : x ^ n = (algebraMap R S) a) : φ x - (algebraMap R S) (a ^ ((Nat.card (R ⧸ Ideal.under R Q) - 1) / n)) * x ∈ Q

The power residue congruence. If x ^ n = a with a ∈ R and n ∣ q - 1, where q = #(R ⧸ Q ∩ R), then a Frobenius at Q multiplies x by a ^ ((q - 1) / n) modulo Q.

theorem AlgHom.IsArithFrobAt.apply_eq_self_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {φ : S →ₐ[R] S} {Q : Ideal S} [IsDomain S] [Q.IsPrime] (H : φ.IsArithFrobAt Q) {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ((algebraMap R S) ζ) n) (hn : ↑n ∉ Q) {x : S} {a : R} (hx : x ^ n = (algebraMap R S) a) (ha : (algebraMap R S) a ∉ Q) : φ x = x ↔ ∃ (b : R ⧸ Ideal.under R Q), b ^ n = (Ideal.Quotient.mk (Ideal.under R Q)) a

A Frobenius fixes an n-th root exactly at an n-th power residue. Let S be a domain, Q a prime of S, and φ an arithmetic Frobenius at Q. Suppose that ζ ∈ R is a primitive n-th root of unity in S and that n ∉ Q. If x ^ n = a with a ∈ R and a ∉ Q, then φ x = x exactly when the class of a is an n-th power in R ⧸ Q ∩ R.

theorem IsArithFrobAt.smul_eq_self_iff {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] {n : ℕ} {ζ : R} {x : S} {a : R} [Monoid G] [MulSemiringAction G S] [SMulCommClass G R S] {Q : Ideal S} [Q.IsPrime] {σ : G} (H : IsArithFrobAt R σ Q) (hζ : IsPrimitiveRoot ((algebraMap R S) ζ) n) (hn : ↑n ∉ Q) (hx : x ^ n = (algebraMap R S) a) (ha : (algebraMap R S) a ∉ Q) : σ • x = x ↔ ∃ (b : R ⧸ Ideal.under R Q), b ^ n = (Ideal.Quotient.mk (Ideal.under R Q)) a

A Frobenius element fixes an n-th root exactly at an n-th power residue, action form of AlgHom.IsArithFrobAt.apply_eq_self_iff.

theorem IsArithFrobAt.forall_mem_closure_smul_eq_self_iff {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] {n : ℕ} {ζ : R} {x : S} {a : R} [Group G] [MulSemiringAction G S] [SMulCommClass G R S] {ι : Type u_4} {σ : ι → G} {Q : ι → Ideal S} [∀ (i : ι), (Q i).IsPrime] (H : ∀ (i : ι), IsArithFrobAt R (σ i) (Q i)) (hζ : IsPrimitiveRoot ((algebraMap R S) ζ) n) (hn : ∀ (i : ι), ↑n ∉ Q i) (hx : x ^ n = (algebraMap R S) a) (ha : ∀ (i : ι), (algebraMap R S) a ∉ Q i) : (∀ g ∈ Subgroup.closure (Set.range σ), g • x = x) ↔ ∀ (i : ι), ∃ (b : R ⧸ Ideal.under R (Q i)), b ^ n = (Ideal.Quotient.mk (Ideal.under R (Q i))) a

The subgroup generated by Frobenius elements fixes an n-th root exactly at common n-th power residues. Let σ i be an arithmetic Frobenius at the prime Q i for every i. If x ^ n = a, with n and a outside every Q i and R containing a primitive n-th root of unity of S, then the subgroup generated by the σ i fixes x exactly when a is an n-th power modulo every Q i ∩ R.