Square roots of integers as algebraic integers

An element x of a field K with x² = d for an integer d is integral over ℤ (its square is an integer, which is integral); this file packages such an x as an element NumberField.integralSqrt hx of the ring of integers 𝓞 K, together with its two defining identities: its image in K is x, and it squares to d in 𝓞 K.

This is the shared square-root packaging used by the multiquadratic Layer 1 files: the splitting law (TauCeti.NumberTheory.Multiquadratic.MultiquadraticSplitting) moves the generators √dᵢ into 𝓞 K to compare residues, and the Frobenius computation (TauCeti.NumberTheory.NumberField.Frobenius) applies the arithmetic-Frobenius congruence, which lives on 𝓞 K, to a square root.

When d is not a rational square, X² - d is irreducible over ℚ, so it is the minimal polynomial of x over ℚ; since ℤ is integrally closed in ℚ and x is integral, it is also the minimal polynomial over ℤ. That last identity is the standing hypothesis hmin of the quadratic-field API in TauCeti.NumberTheory.NumberField.Quadratic and of the multiquadratic files built on it, so it is recorded here once.

For d ≡ 1 (mod 4), the half-generator (1 + x) / 2 is integral as well. This is the integral generator that separates conjugates at primes above 2.

Main definitions and results

• TauCeti.sq_one_add_div_two_sub_self: the quadratic relation for the half-generator.
• TauCeti.isIntegral_one_add_div_two_of_sq_eq: the half-generator is integral when d ≡ 1 (mod 4).
• NumberField.integralSqrt: the packaging in 𝓞 K, with NumberField.algebraMap_integralSqrt and NumberField.integralSqrt_sq.
• NumberField.minpoly_integralSqrt: its minimal polynomial over ℤ is X² - d, provided d is not a rational square.

noncomputable def NumberField.integralSqrt {K : Type u_1} [Field K] {x : K} {d : ℤ} (hx : x ^ 2 = (algebraMap ℤ K) d) : RingOfIntegers K

A square root x of an integer d, packaged as an element of the ring of integers: since x ^ 2 = d is the image of an integer, it is integral over ℤ (IsIntegral.of_pow).

Equations

• NumberField.integralSqrt hx = ⟨x, ⋯⟩

@[simp]

theorem NumberField.algebraMap_integralSqrt {K : Type u_1} [Field K] {x : K} {d : ℤ} (hx : x ^ 2 = (algebraMap ℤ K) d) : (algebraMap (RingOfIntegers K) K) (integralSqrt hx) = x

Under 𝓞 K ↪ K, NumberField.integralSqrt hx maps back to x.

@[simp]

theorem NumberField.integralSqrt_sq {K : Type u_1} [Field K] {x : K} {d : ℤ} (hx : x ^ 2 = (algebraMap ℤ K) d) : integralSqrt hx ^ 2 = (algebraMap ℤ (RingOfIntegers K)) d

NumberField.integralSqrt hx squares to the radicand d in 𝓞 K.

theorem NumberField.minpoly_integralSqrt {K : Type u_1} [Field K] {x : K} {d : ℤ} [NumberField K] (hx : x ^ 2 = (algebraMap ℤ K) d) (hnsq : ¬IsSquare ↑d) : minpoly ℤ (integralSqrt hx) = Polynomial.X ^ 2 - Polynomial.C d

The minimal polynomial of a square root of a nonsquare integer. If x ^ 2 = d for an integer d that is not a square in ℚ, then X ^ 2 - d is the minimal polynomial over ℤ of NumberField.integralSqrt hx. Over ℚ this is Kummer irreducibility (X_pow_sub_C_irreducible_of_prime); the descent to ℤ is minpoly.isIntegrallyClosed_eq_field_fractions.

theorem TauCeti.sq_one_add_div_two_sub_self {K : Type u_1} [Field K] [CharZero K] {x : K} {d : ℤ} (hx : x ^ 2 = (algebraMap ℤ K) d) (hd : d % 4 = 1) : ((1 + x) / 2) ^ 2 - (1 + x) / 2 = (algebraMap ℤ K) (d / 4)

If x² = d and d ≡ 1 (mod 4), the half-generator satisfies ((1 + x) / 2)² - (1 + x) / 2 = ⌊d / 4⌋.

theorem TauCeti.isIntegral_one_add_div_two_of_sq_eq {K : Type u_1} [Field K] [CharZero K] {x : K} {d : ℤ} (hx : x ^ 2 = (algebraMap ℤ K) d) (hd : d % 4 = 1) : IsIntegral ℤ ((1 + x) / 2)

If x² = d and d ≡ 1 (mod 4), then (1 + x) / 2 is an algebraic integer. No nonsquareness or squarefreeness assumption on d is needed.