Frobenius actions on multiquadratic generators #
Let K = ℚ(√d₁, …, √dₙ) be a number field generated over ℚ by square roots r i of
integers d i, and let p be an odd prime dividing none of the d i. The multiquadratic
roadmap's Layer 1 states the splitting law in two forms: p splits completely iff every d i
is a quadratic residue mod p (NumberField.ncard_primesOver_multiquadratic_iff),
and, more precisely, the Frobenius at p acts on the generators by the Legendre symbols. This
file supplies the second, finer form. An arithmetic Frobenius exists at every prime Q of
𝓞 K above p and acts on each generator by the corresponding symbol,
σ (r i) = legendreSym p (d i) • r i
(NumberField.exists_isArithFrobAt_multiquadratic), and the Frobenius is trivial iff
every symbol is 1 (isArithFrobAt_multiquadratic_eq_one_iff).
The roadmap's actual sign-vector statement — the Frobenius equals ((d₁/p), …, (dₙ/p)) under
the identification Gal ≅ (ℤ/2)ⁿ — is then proved for the multiquadratic field taken as the
intermediate field M = ℚ(√dᵢ : i) = adjoin ℚ (Set.range root) itself, where
TauCeti.Multiquadratic.galoisGroupEquiv lives (its automorphisms are of M, not of an
abstract K). For a Frobenius σ on M at a prime over p,
NumberField.signPattern_frobenius gives each coordinate
signPattern root σ i = if legendreSym p (d i) = 1 then 0 else 1, and
NumberField.galoisGroupEquiv_frobenius packages this as
galoisGroupEquiv σ = ((d₁/p), …, (dₙ/p)).
Main results #
NumberField.exists_isArithFrobAt_multiquadratic: at every primeQoverpthere is a Frobenius, and it sends each generatorr itolegendreSym p (d i) • r i.NumberField.isArithFrobAt_multiquadratic_eq_one_iff: a Frobenius atQis the identity iff everyd iis a quadratic residue modp.NumberField.signPattern_frobeniusandNumberField.galoisGroupEquiv_frobenius: the Frobenius sign pattern on the multiquadratic field is the Legendre vector((d₁/p), …, (dₙ/p))underGal ≅ (ℤ/2)ⁿ.TauCeti.Multiquadratic.isArithFrobAt_eq_one_iff_mod_eight: for radicands1modulo4, Frobenius at2is trivial exactly when all radicands are1modulo8.TauCeti.Multiquadratic.signPattern_frobenius_twoandTauCeti.Multiquadratic.galoisGroupEquiv_frobenius_two: its coordinates are0at radicands1modulo8and1at radicands5modulo8.
A multiquadratic Frobenius is trivial iff every radicand is a residue. Let
K = ℚ(√d₁, …, √dₙ) be generated over ℚ by the square roots r i of the integers d i,
let p be an odd prime with p ∤ d i for all i, and let σ be an arithmetic Frobenius at
an ideal Q of 𝓞 K above p. Then σ = 1 iff every d i is a quadratic residue mod p.
Combined with the splitting law, this is the Frobenius-theoretic reading of complete
splitting.
The Frobenius of a multiquadratic field acts on each generator by a Legendre symbol.
For a Galois number field K with elements r i satisfying r i ² = d i ∈ ℤ, an odd prime
p with p ∤ d i for all i, and any prime Q of 𝓞 K above p, there is an arithmetic
Frobenius σ ∈ Gal(K/ℚ) at Q, and it sends each generator to the corresponding Legendre
multiple: σ (r i) = legendreSym p (d i) • r i. This is the generator-wise Frobenius input of
the multiquadratic splitting law; the sign-vector description under galoisGroupEquiv is not
formed here (see the module docstring). The IsGalois ℚ K hypothesis holds in particular when
the r i generate K (TauCeti.Multiquadratic.isGalois transported along adjoin ℚ … = ⊤).
The Frobenius as a sign vector under Gal ≅ (ℤ/2)ⁿ #
The signPattern/galoisGroupEquiv API of TauCeti.NumberTheory.Multiquadratic.Galois.Group
is stated for automorphisms of the intermediate field M = adjoin ℚ (Set.range root). To match
the roadmap's Gal(K/ℚ) ≅ (ℤ/2)ⁿ Frobenius-vector statement we take that intermediate field
(a number field, NumberField.of_intermediateField) as the multiquadratic field itself, and
compute the Frobenius sign pattern there.
The rational algebra structure on the multiquadratic intermediate field.
Equations
Instances For
The Frobenius sign pattern of a multiquadratic field is the Legendre encoding. For the
multiquadratic field M = ℚ(√dᵢ : i) = adjoin ℚ (Set.range root), an odd prime p ∤ dᵢ, and an
arithmetic Frobenius σ on M at a prime Q above p, the i-th coordinate of the sign
pattern is 0 when dᵢ is a quadratic residue mod p and 1 otherwise.
The Frobenius of a multiquadratic field is the Legendre sign vector. Under square-class
independence of the dᵢ (so TauCeti.Multiquadratic.galoisGroupEquiv is the identification
Gal(M/ℚ) ≅ (ℤ/2)ⁿ), an arithmetic Frobenius σ at a prime Q above the odd prime p ∤ dᵢ
maps to the vector of Legendre symbols i ↦ (dᵢ/p). This is the roadmap's Layer 1 Frobenius
statement.
Dyadic Frobenius sign patterns in multiquadratic fields #
For square roots of integers dᵢ ≡ 1 (mod 4), Frobenius at a prime over 2 has sign
coordinate 0 if dᵢ ≡ 1 (mod 8) and 1 if dᵢ ≡ 5 (mod 8). Under square-class
independence these are its coordinates in the explicit Galois-group isomorphism with (ℤ/2)ⁿ.
In particular, Frobenius is the identity exactly when every radicand is 1 modulo 8.
The condition modulo 4 lets one use integral half-generators to separate the two conjugates
modulo 2. For prime-discriminant composita of odd discriminant, all generators satisfy this
condition. This complements the odd-prime Legendre-symbol calculation above.
Frobenius above 2 on a field generated by square roots of dᵢ ≡ 1 (mod 4) is trivial
exactly when all the radicands are 1 modulo 8. No independence assumption is needed.
The sign vector of a dyadic Frobenius has a 1 exactly at the radicands congruent to 5
modulo 8.
Under square-class independence, the Galois-group coordinates of Frobenius above 2 are
0 at radicands 1 modulo 8 and 1 at radicands 5 modulo 8.