The Frobenius acts on square roots by the Legendre symbol

Let S be a commutative domain, Q an ideal of S lying over the rational prime p ≠ 2, and φ an arithmetic Frobenius at Q (AlgHom.IsArithFrobAt, so φ y ≡ y ^ p (mod Q) for all y). If x ∈ S is a square root of an integer d with p ∤ d, then

φ x = legendreSym p d • x.

Indeed φ x ≡ x ^ p = (x²)^((p-1)/2) · x = d^((p-1)/2) · x ≡ (d/p) · x (mod Q) by Euler's criterion, while (φ x)² = x² forces φ x = ± x on the nose; the two signs are separated modulo Q because 2x ∈ Q would force p ∣ 4d. This is the local input for the Frobenius form of the multiquadratic splitting law (Layer 1 of the multiquadratic roadmap): the Frobenius of ℚ(√d₁, …, √dₙ) at p acts on each generator by the sign (dᵢ/p). TauCeti.NumberTheory.NumberField.Frobenius transports this computation to the Galois group of a number field, and TauCeti.NumberTheory.Multiquadratic.Frobenius applies it to the multiquadratic generators.

Main results

• AlgHom.IsArithFrobAt.apply_sqrt: φ x = legendreSym p d • x for an arithmetic Frobenius φ : S →ₐ[ℤ] S at Q and x² = d.
• IsArithFrobAt.smul_sqrt: the same for a Frobenius element σ of a monoid acting on S.

theorem AlgHom.IsArithFrobAt.apply_sqrt {S : Type u_1} [CommRing S] {p : ℕ} [Fact (Nat.Prime p)] {d : ℤ} [IsDomain S] {Q : Ideal S} {x : S} {φ : S →ₐ[ℤ] S} (H : φ.IsArithFrobAt Q) [Q.LiesOver (Ideal.span {↑p})] (hodd : p ≠ 2) (hd : ¬↑p ∣ d) (hx : x ^ 2 = (algebraMap ℤ S) d) : φ x = legendreSym p d • x

An arithmetic Frobenius acts on square roots by the Legendre symbol. Let S be a domain, Q an ideal of S over the odd rational prime p, and φ : S →ₐ[ℤ] S an arithmetic Frobenius at Q. If x² = d for an integer d not divisible by p, then φ x = legendreSym p d • x: the Frobenius fixes √d when d is a quadratic residue mod p and negates it otherwise. (Primality of Q is not needed: the sign separation comes from S being a domain and Q ∩ ℤ = (p).)

theorem IsArithFrobAt.smul_sqrt {S : Type u_1} [CommRing S] {p : ℕ} [Fact (Nat.Prime p)] {d : ℤ} [IsDomain S] {Q : Ideal S} {x : S} {M : Type u_2} [Monoid M] [MulSemiringAction M S] [SMulCommClass M ℤ S] {σ : M} (H : IsArithFrobAt ℤ σ Q) [Q.LiesOver (Ideal.span {↑p})] (hodd : p ≠ 2) (hd : ¬↑p ∣ d) (hx : x ^ 2 = (algebraMap ℤ S) d) : σ • x = legendreSym p d • x

A Frobenius element acts on square roots by the Legendre symbol, action form: if σ : M is an arithmetic Frobenius at an ideal Q over the odd prime p and x² = d with p ∤ d, then σ • x = legendreSym p d • x. Only a monoid action is needed.