The fundamental discriminant of a squarefree radicand

For a squarefree integer d, the quadratic field ℚ(√d) has discriminant d when d ≡ 1 (mod 4) and 4 * d otherwise. This file packages that assignment as a function TauCeti.Multiquadratic.fundamentalDiscriminant and proves the two facts the genus-field layer needs of it: for squarefree d the value is a fundamental discriminant (so FundamentalDiscriminant/Factorization splits it into prime discriminants), and it differs from d by a square, so it names the same quadratic field ℚ(√d).

The genus field of ℚ(√d) is the compositum of the ℚ(√(radicand D*)) over the prime discriminants D* dividing the discriminant of ℚ(√d); this function supplies that discriminant from the squarefree radicand d.

It also records which primes divide the fundamental discriminant, feeding the prime-ramification law in Quadratic/Ramification.lean: a prime coprime to 2 divides it exactly when it divides d, and 2 divides it exactly when d ≢ 1 (mod 4).

Main definitions and results

• TauCeti.Multiquadratic.fundamentalDiscriminant: d if d ≡ 1 (mod 4), else 4 * d, with its defining equation fundamentalDiscriminant_def.
• TauCeti.Multiquadratic.isFundamentalDiscriminant_fundamentalDiscriminant: for squarefree d, its fundamental discriminant is a fundamental discriminant.
• TauCeti.Multiquadratic.exists_sq_mul_eq_fundamentalDiscriminant: it equals c² * d for some c ∈ {1, 2}, so it lies in the square class of d.
• TauCeti.Multiquadratic.dvd_fundamentalDiscriminant_iff: for p coprime to 2, p ∣ fundamentalDiscriminant d ↔ p ∣ d (the ramified odd primes are the divisors of d).
• TauCeti.Multiquadratic.two_not_dvd_fundamentalDiscriminant_iff_mod_four_eq_one: 2 ∤ fundamentalDiscriminant d ↔ d ≡ 1 (mod 4) (2 is unramified exactly then).
• TauCeti.Multiquadratic.fundamentalDiscriminant_ne_zero: it is nonzero for nonzero d.
• TauCeti.Multiquadratic.fundamentalDiscriminant_primeDiscriminantRadicand: a prime discriminant is the fundamental discriminant of its own radicand.

def TauCeti.Multiquadratic.fundamentalDiscriminant (d : ℤ) : ℤ

The fundamental discriminant attached to an integer d: the discriminant of the quadratic field ℚ(√d) for squarefree d, namely d when d ≡ 1 (mod 4) and 4 * d otherwise.

Equations

• TauCeti.Multiquadratic.fundamentalDiscriminant d = if d % 4 = 1 then d else 4 * d

@[simp]

theorem TauCeti.Multiquadratic.fundamentalDiscriminant_of_mod_four_eq_one {d : ℤ} (hd : d % 4 = 1) : fundamentalDiscriminant d = d

@[simp]

theorem TauCeti.Multiquadratic.fundamentalDiscriminant_of_mod_four_ne_one {d : ℤ} (hd : d % 4 ≠ 1) : fundamentalDiscriminant d = 4 * d

theorem TauCeti.Multiquadratic.fundamentalDiscriminant_def (d : ℤ) : fundamentalDiscriminant d = if d % 4 = 1 then d else 4 * d

theorem TauCeti.Multiquadratic.exists_sq_mul_eq_fundamentalDiscriminant (d : ℤ) : ∃ (c : ℤ), (c = 1 ∨ c = 2) ∧ c ^ 2 * d = fundamentalDiscriminant d

c² * d = fundamentalDiscriminant d for some c ∈ {1, 2}: the fundamental discriminant differs from d by a nonzero square, so ℚ(√(fundamentalDiscriminant d)) = ℚ(√d). The c = 1 ∨ c = 2 restriction is part of the statement, so the multiplier is genuinely a unit-or-2 square (not the vacuous c = 0).

theorem TauCeti.Multiquadratic.fundamentalDiscriminant_ne_zero {d : ℤ} (hd : d ≠ 0) : fundamentalDiscriminant d ≠ 0

The fundamental discriminant of a nonzero integer is nonzero, being a nonzero square multiple of it.

theorem TauCeti.Multiquadratic.isFundamentalDiscriminant_fundamentalDiscriminant {d : ℤ} (hd : Squarefree d) : IsFundamentalDiscriminant (fundamentalDiscriminant d)

The fundamental discriminant of a squarefree integer is a fundamental discriminant. When d ≡ 1 (mod 4) the value is d itself (≡ 1 (mod 4), squarefree); otherwise d ≡ 2 or 3 (mod 4) (it cannot be 0 (mod 4), as 4 = 2² would break squarefreeness) and the value is 4 * d.

@[simp]

theorem TauCeti.Multiquadratic.dvd_fundamentalDiscriminant_iff {d p : ℤ} (hp : IsCoprime p 2) : p ∣ fundamentalDiscriminant d ↔ p ∣ d

For p coprime to 2, divisibility by fundamentalDiscriminant d is the same as divisibility by d: the only extra factor in the d ≢ 1 (mod 4) case is 4, which is coprime to p.

theorem TauCeti.Multiquadratic.two_not_dvd_fundamentalDiscriminant_iff_mod_four_eq_one (d : ℤ) : ¬2 ∣ fundamentalDiscriminant d ↔ d % 4 = 1

The fundamental discriminant is odd exactly when d ≡ 1 (mod 4) (otherwise it is 4d). Not @[simp]: Int.two_dvd_ne_zero already normalises ¬ 2 ∣ x to x % 2 = 1, so this ¬ ∣ left-hand side is not a simp normal form (it is applied explicitly instead).

theorem TauCeti.Multiquadratic.fundamentalDiscriminant_primeDiscriminantRadicand {D : ℤ} (hD : IsPrimeDiscriminant D) : fundamentalDiscriminant (primeDiscriminantRadicand D) = D

A prime discriminant is the fundamental discriminant of its own radicand. For an odd prime discriminant this is the congruence p* ≡ 1 (mod 4); for -4, 8, -8 it is the factor 4 removed by primeDiscriminantRadicand. So ℚ(√(radicand D)) is the quadratic field of discriminant D.