Prime discriminants

The genus-field layer of the multiquadratic roadmap uses the prime discriminants -4, 8, -8, and p* = (-1)^((p - 1) / 2) p for odd primes p. The files PrimeDiscriminant and EvenPrimeDiscriminant develop the odd and 2-adic pieces separately; this file packages them into one predicate and one radicand map for later genus-field constructions.

For an odd prime discriminant the radicand is the discriminant itself. For an even prime discriminant D ∈ {-4, 8, -8}, the radicand is D / 4, so the three even cases give -1, 2, and -2.

Main definitions and results

• TauCeti.Multiquadratic.IsPrimeDiscriminant: the union of the even prime discriminants and odd prime discriminants.
• TauCeti.Multiquadratic.primeDiscriminantRadicand: the associated squarefree integer radicand.
• TauCeti.Multiquadratic.dvd_primeDiscriminant_iff_dvd_radicand: away from 2, an integer and its associated radicand have the same prime divisors.
• TauCeti.Multiquadratic.squarefree_primeDiscriminantRadicand: the associated radicand is squarefree.
• TauCeti.Multiquadratic.not_isSquare_primeDiscriminantRadicand_rat: the associated rational radicand is not a square.
• TauCeti.Multiquadratic.primeDiscriminantPrime: the single rational prime lying under a prime discriminant, with TauCeti.Multiquadratic.natCast_dvd_primeDiscriminant_iff saying that it is the only prime divisor.
• TauCeti.Multiquadratic.isCoprime_primeDiscriminant_of_ne_of_not_both_even: distinct prime discriminants are coprime, unless both are even.
• TauCeti.Multiquadratic.lcm_natAbs_eq_natAbs_prod_of_forall_isPrimeDiscriminant_of_not_both_even: for prime discriminants with at most one even member, the least common multiple of their absolute values is that of their product.
• TauCeti.Multiquadratic.prod_ne_zero_of_forall_isPrimeDiscriminant and TauCeti.Multiquadratic.neZero_natAbs_prod_of_forall_isPrimeDiscriminant: a product of prime discriminants is nonzero, so its absolute value is a legitimate Dirichlet character level.

def TauCeti.Multiquadratic.IsPrimeDiscriminant (D : ℤ) : Prop

The prime discriminants: the even prime discriminants -4, 8, -8, together with the odd prime discriminants p* for odd natural primes p.

Equations

• TauCeti.Multiquadratic.IsPrimeDiscriminant D = (TauCeti.Multiquadratic.IsEvenPrimeDiscriminant D ∨ ∃ (p : ℕ), Nat.Prime p ∧ Odd p ∧ D = TauCeti.Multiquadratic.oddPrimeDiscriminant p)

theorem TauCeti.Multiquadratic.isPrimeDiscriminant_iff {D : ℤ} : IsPrimeDiscriminant D ↔ IsEvenPrimeDiscriminant D ∨ ∃ (p : ℕ), Nat.Prime p ∧ Odd p ∧ D = oddPrimeDiscriminant p

The defining disjunction for IsPrimeDiscriminant.

theorem TauCeti.Multiquadratic.IsEvenPrimeDiscriminant.isPrimeDiscriminant {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : IsPrimeDiscriminant D

Every even prime discriminant is a prime discriminant.

@[simp]

theorem TauCeti.Multiquadratic.isPrimeDiscriminant_neg_four : IsPrimeDiscriminant (-4)

The discriminant -4 is a prime discriminant.

@[simp]

theorem TauCeti.Multiquadratic.isPrimeDiscriminant_eight : IsPrimeDiscriminant 8

The discriminant 8 is a prime discriminant.

@[simp]

theorem TauCeti.Multiquadratic.isPrimeDiscriminant_neg_eight : IsPrimeDiscriminant (-8)

The discriminant -8 is a prime discriminant.

theorem TauCeti.Multiquadratic.isPrimeDiscriminant_oddPrimeDiscriminant {p : ℕ} (hp : Nat.Prime p) (hodd : Odd p) : IsPrimeDiscriminant (oddPrimeDiscriminant p)

The odd prime discriminant attached to an odd natural prime is a prime discriminant.

theorem TauCeti.Multiquadratic.IsPrimeDiscriminant.one_lt_natAbs {D : ℤ} (hD : IsPrimeDiscriminant D) : 1 < D.natAbs

The absolute value of a prime discriminant is greater than one.

theorem TauCeti.Multiquadratic.not_isEvenPrimeDiscriminant_oddPrimeDiscriminant {p : ℕ} (hodd : Odd p) : ¬IsEvenPrimeDiscriminant (oddPrimeDiscriminant p)

An odd prime discriminant is not one of the even prime discriminants.

def TauCeti.Multiquadratic.primeDiscriminantRadicand (D : ℤ) : ℤ

The squarefree radicand attached to a prime discriminant. In the even cases this divides by 4; in the odd cases the discriminant is already squarefree and is used as its own radicand.

Equations

• TauCeti.Multiquadratic.primeDiscriminantRadicand D = if D = -4 ∨ D = 8 ∨ D = -8 then TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand D else D

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_def (D : ℤ) : primeDiscriminantRadicand D = if D = -4 ∨ D = 8 ∨ D = -8 then evenPrimeDiscriminantRadicand D else D

The defining equation for the prime-discriminant radicand.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_neg_four : primeDiscriminantRadicand (-4) = -1

The prime-discriminant radicand of -4 is -1.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_eight : primeDiscriminantRadicand 8 = 2

The prime-discriminant radicand of 8 is 2.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_neg_eight : primeDiscriminantRadicand (-8) = -2

The prime-discriminant radicand of -8 is -2.

@[simp]

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_of_isEvenPrimeDiscriminant {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : primeDiscriminantRadicand D = evenPrimeDiscriminantRadicand D

The radicand attached to an even prime discriminant is its even-prime radicand.

@[simp]

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_oddPrimeDiscriminant {p : ℕ} (hodd : Odd p) : primeDiscriminantRadicand (oddPrimeDiscriminant p) = oddPrimeDiscriminant p

The radicand attached to an odd prime discriminant is the discriminant itself.

theorem TauCeti.Multiquadratic.primeDiscriminant_eq_radicand_or_eq_four_mul_radicand {D : ℤ} (hD : IsPrimeDiscriminant D) : D = primeDiscriminantRadicand D ∨ D = 4 * primeDiscriminantRadicand D

A prime discriminant is either its own radicand, or four times its radicand in the even cases.

@[simp]

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_neg_iff {D : ℤ} (hD : IsPrimeDiscriminant D) : primeDiscriminantRadicand D < 0 ↔ D < 0

A prime discriminant and its squarefree radicand have the same sign.

theorem TauCeti.Multiquadratic.dvd_primeDiscriminant_iff_dvd_radicand {q : ℕ} [Fact (Nat.Prime q)] (D : ℤ) (hq : q ≠ 2) : ↑q ∣ D ↔ ↑q ∣ primeDiscriminantRadicand D

Away from 2, divisibility of an integer is the same as divisibility of its associated prime-discriminant radicand. In the even-prime cases the two differ by the square factor 4; in all other cases they are equal. Not a simp lemma: the right-hand side is again of the form (q : ℤ) ∣ _, so as a rewrite rule it matches its own output and loops.

theorem TauCeti.Multiquadratic.forall_not_dvd_primeDiscriminant_iff_radicand {q : ℕ} [Fact (Nat.Prime q)] {ι : Type u_1} (D : ι → ℤ) (hq : q ≠ 2) : (∀ (i : ι), ¬↑q ∣ D i) ↔ ∀ (i : ι), ¬↑q ∣ primeDiscriminantRadicand (D i)

Away from 2, an indexed family of integers and its associated prime-discriminant radicands have the same unramifiedness condition at q.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_ne_zero {D : ℤ} (hD : IsPrimeDiscriminant D) : primeDiscriminantRadicand D ≠ 0

The radicand attached to a prime discriminant is nonzero.

theorem TauCeti.Multiquadratic.squarefree_primeDiscriminantRadicand {D : ℤ} (hD : IsPrimeDiscriminant D) : Squarefree (primeDiscriminantRadicand D)

The radicand attached to a prime discriminant is squarefree.

theorem TauCeti.Multiquadratic.not_isSquare_primeDiscriminantRadicand_rat {D : ℤ} (hD : IsPrimeDiscriminant D) : ¬IsSquare ↑(primeDiscriminantRadicand D)

The radicand attached to a prime discriminant is not a rational square.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_mod_four_eq_one_of_odd {p : ℕ} (hodd : Odd p) : primeDiscriminantRadicand (oddPrimeDiscriminant p) % 4 = 1

An odd prime discriminant has odd radicand congruent to 1 modulo 4.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_mod_four_eq_three_or_two_of_even {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : primeDiscriminantRadicand D % 4 = 3 ∨ primeDiscriminantRadicand D % 4 = 2

An even prime discriminant has radicand congruent to 3 or 2 modulo 4.

theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_or_primeDiscriminantRadicand_mod_four_eq_one {D : ℤ} (hD : IsPrimeDiscriminant D) : IsEvenPrimeDiscriminant D ∨ primeDiscriminantRadicand D % 4 = 1

A prime discriminant is either even, or its associated radicand is congruent to 1 modulo 4.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_natAbs_eq_one_iff {D : ℤ} (hD : IsPrimeDiscriminant D) : (primeDiscriminantRadicand D).natAbs = 1 ↔ D = -4

The only prime discriminant whose radicand has absolute value 1 is -4. This is the small exceptional case in the radicand map: the odd prime-discriminant radicands have prime absolute value, and the other even prime-discriminant radicands have absolute value 2.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_eq_neg_one_iff {D : ℤ} (hD : IsPrimeDiscriminant D) : primeDiscriminantRadicand D = -1 ↔ D = -4

Among prime discriminants, radicand -1 comes only from the even prime discriminant -4.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_eq_two_iff {D : ℤ} (hD : IsPrimeDiscriminant D) : primeDiscriminantRadicand D = 2 ↔ D = 8

Among prime discriminants, radicand 2 comes only from the even prime discriminant 8.

theorem TauCeti.Multiquadratic.primeDiscriminantRadicand_eq_neg_two_iff {D : ℤ} (hD : IsPrimeDiscriminant D) : primeDiscriminantRadicand D = -2 ↔ D = -8

Among prime discriminants, radicand -2 comes only from the even prime discriminant -8.

theorem TauCeti.Multiquadratic.eq_of_primeDiscriminantRadicand_eq {D E : ℤ} (hD : IsPrimeDiscriminant D) (hE : IsPrimeDiscriminant E) (h : primeDiscriminantRadicand D = primeDiscriminantRadicand E) : D = E

The radicand map is injective on prime discriminants. This is the bookkeeping that lets later genus-field code pass between a list of prime discriminants and the corresponding multiquadratic radicands without identifying two different quadratic factors.

theorem TauCeti.Multiquadratic.injOn_primeDiscriminantRadicand : Set.InjOn primeDiscriminantRadicand {D : ℤ | IsPrimeDiscriminant D}

primeDiscriminantRadicand is injective on the set of prime discriminants.

theorem TauCeti.Multiquadratic.injective_primeDiscriminantRadicand_comp_iff {ι : Type u_1} {D : ι → ℤ} (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) : (Function.Injective fun (i : ι) => primeDiscriminantRadicand (D i)) ↔ Function.Injective D

For a family of prime discriminants, injectivity is unchanged after replacing each discriminant by its multiquadratic radicand.

The prime under a prime discriminant

A prime discriminant is, up to sign, a power of a single rational prime: p for the odd prime discriminant p*, and 2 for each of -4, 8, -8. That prime is the one ramifying in the quadratic field the discriminant belongs to, so the map below is what turns a prime-discriminant factorization of a fundamental discriminant into the list of ramified primes.

def TauCeti.Multiquadratic.primeDiscriminantPrime (D : ℤ) : ℕ

The rational prime lying under a prime discriminant D, when IsPrimeDiscriminant D: p for the odd prime discriminant p*, and 2 for the even prime discriminants -4, 8, -8. That the value really is prime under that hypothesis is prime_primeDiscriminantPrime.

The definition is total: on an integer that is not a prime discriminant it returns the junk value D.natAbs (unless D is one of -4, 8, -8), which need not be prime — for instance primeDiscriminantPrime 9 = 9.

Equations

• TauCeti.Multiquadratic.primeDiscriminantPrime D = if D = -4 ∨ D = 8 ∨ D = -8 then 2 else D.natAbs

theorem TauCeti.Multiquadratic.primeDiscriminantPrime_def (D : ℤ) : primeDiscriminantPrime D = if D = -4 ∨ D = 8 ∨ D = -8 then 2 else D.natAbs

The defining if expression for primeDiscriminantPrime. The body of primeDiscriminantPrime is not @[expose]d, so downstream files rewrite with this lemma — or with the evaluation lemmas below — rather than unfolding the definition.

@[simp]

theorem TauCeti.Multiquadratic.primeDiscriminantPrime_of_isEvenPrimeDiscriminant {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : primeDiscriminantPrime D = 2

The prime under an even prime discriminant is 2.

@[simp]

theorem TauCeti.Multiquadratic.primeDiscriminantPrime_oddPrimeDiscriminant {p : ℕ} (hodd : Odd p) : primeDiscriminantPrime (oddPrimeDiscriminant p) = p

The prime under the odd prime discriminant p* is p.

theorem TauCeti.Multiquadratic.prime_primeDiscriminantPrime {D : ℤ} (hD : IsPrimeDiscriminant D) : Nat.Prime (primeDiscriminantPrime D)

The prime under a prime discriminant is a natural prime.

theorem TauCeti.Multiquadratic.primeDiscriminantPrime_dvd {D : ℤ} (hD : IsPrimeDiscriminant D) : ↑(primeDiscriminantPrime D) ∣ D

The prime under a prime discriminant divides it.

theorem TauCeti.Multiquadratic.natCast_dvd_primeDiscriminant_iff {D : ℤ} (hD : IsPrimeDiscriminant D) {p : ℕ} (hp : Nat.Prime p) : ↑p ∣ D ↔ p = primeDiscriminantPrime D

A prime discriminant has exactly one prime divisor. A natural prime divides a prime discriminant precisely when it is the prime under it. This is what makes the prime-discriminant factorization of a fundamental discriminant a list of ramified primes without repetition.

theorem TauCeti.Multiquadratic.eq_of_primeDiscriminantPrime_eq {D E : ℤ} (hD : IsPrimeDiscriminant D) (hE : IsPrimeDiscriminant E) (heven : IsEvenPrimeDiscriminant D → IsEvenPrimeDiscriminant E → D = E) (h : primeDiscriminantPrime D = primeDiscriminantPrime E) : D = E

The prime under a prime discriminant determines it, provided the two discriminants are not two distinct even prime discriminants (all three of which lie over 2).

theorem TauCeti.Multiquadratic.injOn_primeDiscriminantPrime {s : Set ℤ} (hs : ∀ D ∈ s, IsPrimeDiscriminant D) (heven : ∀ D ∈ s, ∀ E ∈ s, IsEvenPrimeDiscriminant D → IsEvenPrimeDiscriminant E → D = E) : Set.InjOn primeDiscriminantPrime s

primeDiscriminantPrime is injective on a set of prime discriminants containing at most one even prime discriminant.

theorem TauCeti.Multiquadratic.IsPrimeDiscriminant.ne_zero {D : ℤ} (hD : IsPrimeDiscriminant D) : D ≠ 0

A prime discriminant is nonzero.

theorem TauCeti.Multiquadratic.prod_ne_zero_of_forall_isPrimeDiscriminant {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : ∏ P ∈ s, P ≠ 0

A product of prime discriminants is nonzero.

theorem TauCeti.Multiquadratic.prod_natAbs_ne_zero_of_forall_isPrimeDiscriminant {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : ∏ P ∈ s, P.natAbs ≠ 0

A product of the absolute values of prime discriminants is nonzero.

theorem TauCeti.Multiquadratic.neZero_natAbs_prod_of_forall_isPrimeDiscriminant {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : NeZero (∏ P ∈ s, P).natAbs

The absolute value of a product of prime discriminants is a nonzero level.

theorem TauCeti.Multiquadratic.isCoprime_evenPrimeDiscriminant_oddPrimeDiscriminant {D : ℤ} {p : ℕ} (hD : IsEvenPrimeDiscriminant D) (hp : Odd p) : IsCoprime D (oddPrimeDiscriminant p)

An even prime discriminant is coprime to every odd prime discriminant.

theorem TauCeti.Multiquadratic.isCoprime_primeDiscriminant_of_ne_of_not_both_even {D E : ℤ} (hD : IsPrimeDiscriminant D) (hE : IsPrimeDiscriminant E) (hne : D ≠ E) (heven : ¬(IsEvenPrimeDiscriminant D ∧ IsEvenPrimeDiscriminant E)) : IsCoprime D E

Distinct prime discriminants are coprime, provided they are not two distinct even prime discriminants; the proviso is necessary, since -4, 8 and -8 all lie over 2.

theorem TauCeti.Multiquadratic.lcm_natAbs_eq_natAbs_prod_of_forall_isPrimeDiscriminant_of_not_both_even {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ Q ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) : s.lcm Int.natAbs = (∏ P ∈ s, P).natAbs

For a family of prime discriminants with at most one even member, the least common multiple of their absolute values is the absolute value of their product.