The ring of integers of a quadratic field

For a quadratic number field K = ℚ(√d) — presented by an algebraic integer θ : 𝓞 K with minpoly ℤ θ = X² - d and Algebra.adjoin ℚ {θ} = ⊤ — with d squarefree, the ring of integers depends on d mod 4:

• d ≢ 1 (mod 4): 𝓞 K = ℤ[θ] and NumberField.discr K = 4 * d;
• d ≡ 1 (mod 4): 𝓞 K = ℤ[ω] with ω = (1+θ)/2 = NumberField.halfGen, and NumberField.discr K = d.

The content is the "no more integers" step: an algebraic integer z with (z : K) = a + b·θ (a, b : ℚ) has 2a ∈ ℤ and a² - d·b² ∈ ℤ (its trace and norm), whence 2a, 2b ∈ ℤ (using that d is squarefree), and the residue a² ≡ d·b² (mod 4) fixes the coordinates: 2a, 2b are both even when d % 4 ≠ 1, and are equal mod 2 (so z ∈ ℤ + ℤ·ω) when d ≡ 1 (mod 4).

The same coordinates give the norm form of K: writing the trace as A and twice the second coordinate as B, the norm of z is (A² - d·B²)/4, and the factor 4 disappears when d ≢ 1 (mod 4) because the coordinates are then integers.

Main results

• NumberField.adjoin_gen_eq_top_of_mod_four_ne_one: 𝓞 K = ℤ[θ] for d % 4 ≠ 1.
• NumberField.discr_eq_four_mul_of_mod_four_ne_one: discr K = 4d for d % 4 ≠ 1.
• NumberField.adjoin_halfGen_eq_top_of_mod_four_eq_one: 𝓞 K = ℤ[(1+θ)/2] for d ≡ 1.
• NumberField.minpoly_halfGen: the minimal polynomial of (1+θ)/2 is X² - X + (1-d)/4.
• NumberField.adjoin_rat_halfGen_eq_top: (1+θ)/2 generates K over ℚ.
• NumberField.discr_eq_of_squarefree_of_mod_four_eq_one: discr K = d for d ≡ 1.
• NumberField.exists_sq_sub_mul_sq_eq_four_mul_norm: the norm form 4·N(z) = A² - d·B², and NumberField.exists_sq_sub_mul_sq_eq_norm_of_mod_four_ne_one: N(z) = A² - d·B² for d ≢ 1.

noncomputable def NumberField.halfGen {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hd4 : d % 4 = 1) : RingOfIntegers K

For d ≡ 1 (mod 4), the half-integer generator ω = (1 + θ)/2 ∈ 𝓞 K.

Equations

• NumberField.halfGen hmin hd4 = ⟨(1 + ↑θ) / 2, ⋯⟩

@[simp]

theorem NumberField.coe_halfGen {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hd4 : d % 4 = 1) : ↑(halfGen hmin hd4) = (1 + ↑θ) / 2

The half-integer generator coerces to (1 + θ)/2 in K.

theorem NumberField.adjoin_rat_halfGen_eq_top {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hd4 : d % 4 = 1) : ℚ[↑(halfGen hmin hd4)] = ⊤

The half-integer generator (1+θ)/2 generates K over ℚ whenever θ does.

theorem NumberField.minpoly_halfGen {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hd4 : d % 4 = 1) : minpoly ℤ (halfGen hmin hd4) = Polynomial.X ^ 2 - Polynomial.X + Polynomial.C ((1 - d) / 4)

The minimal polynomial of the half-integer generator (1+θ)/2 over ℤ is X² - X + (1 - d)/4.

theorem NumberField.adjoin_halfGen_eq_top_of_mod_four_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd4 : d % 4 = 1) : ℤ[halfGen hmin hd4] = ⊤

The ring of integers is ℤ[(1+θ)/2] when d ≡ 1 (mod 4). For squarefree d with d % 4 = 1, the ring of integers of ℚ(√d) is generated over ℤ by ω = (1+θ)/2.

theorem NumberField.discr_eq_of_squarefree_of_mod_four_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd4 : d % 4 = 1) : discr K = d

The discriminant of ℚ(√d) when d ≡ 1 (mod 4). For squarefree d with d % 4 = 1, the field discriminant is disc K = d (the ring of integers is ℤ[(1+θ)/2], whose {1, ω} basis has discriminant d).

theorem NumberField.exists_sq_sub_mul_sq_eq_four_mul_norm {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (z : RingOfIntegers K) : ∃ (A : ℤ) (B : ℤ), A ^ 2 - d * B ^ 2 = 4 * (Algebra.norm ℤ) z

The norm form of a quadratic field. For squarefree d, every algebraic integer z of K = ℚ(√d) has 4·N(z) = A² - d·B² for integers A (its trace) and B: the {1, θ}-coordinates of z are the half-integers A/2 and B/2 (exists_half_int_coords), and the norm of a + c·θ is a² - d·c².

This is the shape in which the norm of a quadratic integer is used arithmetically; when d ≢ 1 (mod 4) the factor 4 can be removed, see exists_sq_sub_mul_sq_eq_norm_of_mod_four_ne_one.

theorem NumberField.exists_sq_sub_mul_sq_eq_norm_of_mod_four_ne_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd4 : d % 4 ≠ 1) (z : RingOfIntegers K) : ∃ (A : ℤ) (B : ℤ), A ^ 2 - d * B ^ 2 = (Algebra.norm ℤ) z

The norm form of a quadratic field when d ≢ 1 (mod 4). There the ring of integers is ℤ[θ], so every algebraic integer is A + B·θ and its norm is exactly A² - d·B².

theorem NumberField.adjoin_gen_eq_top_of_mod_four_ne_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd4 : d % 4 ≠ 1) : ℤ[θ] = ⊤

The ring of integers is ℤ[θ] when d ≢ 1 (mod 4). For squarefree d with d % 4 ≠ 1, the ring of integers of ℚ(√d) is generated over ℤ by θ.

theorem NumberField.discr_eq_four_mul_of_mod_four_ne_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hd4 : d % 4 ≠ 1) : discr K = 4 * d

The discriminant of ℚ(√d) when d ≢ 1 (mod 4). For squarefree d with d % 4 ≠ 1 (equivalently d ≡ 2, 3 (mod 4)), the field discriminant is disc K = 4d. The ring of integers is ℤ[θ] — see adjoin_gen_eq_top_of_mod_four_ne_one.