Fundamental discriminants

A fundamental discriminant is an integer D which is either congruent to 1 modulo 4 and squarefree, or of the form 4 * m with m squarefree and congruent to 2 or 3 modulo 4. These are exactly the discriminants of quadratic fields (together with 1, the discriminant of ℚ itself, which arises as the empty product below).

The genus-field layer of the multiquadratic roadmap needs the passage between a fundamental discriminant and the prime discriminants dividing it: the genus field of ℚ(√d) is the compositum of the quadratic fields ℚ(√p*) attached to the prime discriminants dividing disc ℚ(√d), and it is those prime discriminants, not the squarefree radicands, that behave correctly at 2. This file supplies the synthesis half of that passage: a product of prime discriminants with pairwise distinct underlying primes is again a fundamental discriminant. The analysis half (every fundamental discriminant factors as such a product, uniquely) is left to a later file.

Since two distinct even prime discriminants are both divisible by 4, a product of prime discriminants can only be fundamental if at most one factor is even. The two component theorems below therefore split along exactly that line: a product of odd prime discriminants at pairwise distinct primes, and such a product multiplied by one even prime discriminant. Every product of pairwise coprime prime discriminants is of one of these two shapes, and the general theorem isFundamentalDiscriminant_prod assembles the two cases for distinct prime discriminants with at most one even value; isFundamentalDiscriminant_prod_of_pairwise_isCoprime gives the pairwise-coprime specialization.

The definition of a fundamental discriminant and the fact that products of prime discriminants are fundamental are classical; see Cox, Primes of the Form x² + ny², and Lemmermeyer, Reciprocity Laws, following the same prime-discriminant convention as the sibling files in this directory. The -20 and -84 worked examples of the Worked examples section of TauCetiRoadmap/Multiquadratic/README.md have their fundamental-discriminant component established in FundamentalDiscriminant/Examples.lean; their class-group and concrete genus-field identifications remain future work.

Main definitions and results

• TauCeti.Multiquadratic.IsFundamentalDiscriminant: the defining congruence-and-squarefreeness condition.
• TauCeti.Multiquadratic.IsPrimeDiscriminant.isFundamentalDiscriminant: every prime discriminant is a fundamental discriminant.
• TauCeti.Multiquadratic.isFundamentalDiscriminant_prod: a product of distinct prime discriminants with at most one even value is a fundamental discriminant.
• TauCeti.Multiquadratic.isFundamentalDiscriminant_prod_of_pairwise_isCoprime: the pairwise-coprime specialization.
• TauCeti.Multiquadratic.isFundamentalDiscriminant_prod_oddPrimeDiscriminant and its even-factor companion ..._of_isEvenPrimeDiscriminant: the two shape-specific component theorems that isFundamentalDiscriminant_prod assembles.
• TauCeti.Multiquadratic.IsFundamentalDiscriminant.not_isSquare_rat: a fundamental discriminant other than 1 is not a rational square, so ℚ(√D) is a genuine quadratic field.

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

A fundamental discriminant: either D ≡ 1 (mod 4) with D squarefree, or D = 4 * m with m squarefree and m ≡ 2 or 3 (mod 4). These are the discriminants of quadratic fields, together with 1.

Equations

• TauCeti.Multiquadratic.IsFundamentalDiscriminant D = (D % 4 = 1 ∧ Squarefree D ∨ ∃ (m : ℤ), D = 4 * m ∧ (m % 4 = 2 ∨ m % 4 = 3) ∧ Squarefree m)

theorem TauCeti.Multiquadratic.isFundamentalDiscriminant_iff {D : ℤ} : IsFundamentalDiscriminant D ↔ D % 4 = 1 ∧ Squarefree D ∨ ∃ (m : ℤ), D = 4 * m ∧ (m % 4 = 2 ∨ m % 4 = 3) ∧ Squarefree m

The defining disjunction for IsFundamentalDiscriminant.

@[simp]

theorem TauCeti.Multiquadratic.isFundamentalDiscriminant_one : IsFundamentalDiscriminant 1

The discriminant of ℚ itself. It is the empty product of prime discriminants, and the degenerate case of the first branch of the definition.

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

A fundamental discriminant is nonzero.

theorem TauCeti.Multiquadratic.IsFundamentalDiscriminant.mod_four_eq_zero_or_one {D : ℤ} (hD : IsFundamentalDiscriminant D) : D % 4 = 0 ∨ D % 4 = 1

A fundamental discriminant is 0 or 1 modulo 4.

theorem TauCeti.Multiquadratic.IsFundamentalDiscriminant.squarefree_of_mod_four_eq_one {D : ℤ} (hD : IsFundamentalDiscriminant D) (h : D % 4 = 1) : Squarefree D

The first branch accessor: a fundamental discriminant that is 1 modulo 4 is squarefree.

theorem TauCeti.Multiquadratic.IsFundamentalDiscriminant.squarefree_div_four {D : ℤ} (hD : IsFundamentalDiscriminant D) (h : D % 4 = 0) : Squarefree (D / 4)

The second branch accessor: for a fundamental discriminant divisible by 4, the quotient D / 4 is squarefree.

theorem TauCeti.Multiquadratic.IsFundamentalDiscriminant.div_four_mod_four_eq_two_or_three {D : ℤ} (hD : IsFundamentalDiscriminant D) (h : D % 4 = 0) : D / 4 % 4 = 2 ∨ D / 4 % 4 = 3

The second branch accessor: for a fundamental discriminant divisible by 4, the quotient D / 4 is 2 or 3 modulo 4.

theorem TauCeti.Multiquadratic.IsPrimeDiscriminant.isFundamentalDiscriminant {D : ℤ} (hD : IsPrimeDiscriminant D) : IsFundamentalDiscriminant D

Every prime discriminant is a fundamental discriminant: the odd ones land in the first branch of the definition, the even ones -4, 8, -8 in the second, with radicands -1, 2, -2.

theorem TauCeti.Multiquadratic.prod_oddPrimeDiscriminant_mod_four_eq_one {ι : Type u_1} {s : Finset ι} {p : ι → ℕ} (hodd : ∀ i ∈ s, Odd (p i)) : (∏ i ∈ s, oddPrimeDiscriminant (p i)) % 4 = 1

A product of odd prime discriminants is congruent to 1 modulo 4. No distinctness of the underlying primes is needed.

theorem TauCeti.Multiquadratic.odd_prod_oddPrimeDiscriminant {ι : Type u_1} {s : Finset ι} {p : ι → ℕ} (hodd : ∀ i ∈ s, Odd (p i)) : Odd (∏ i ∈ s, oddPrimeDiscriminant (p i))

A product of odd prime discriminants is odd.

theorem TauCeti.Multiquadratic.squarefree_prod_oddPrimeDiscriminant {ι : Type u_1} {s : Finset ι} {p : ι → ℕ} (hp : ∀ i ∈ s, Nat.Prime (p i)) (hinj : Set.InjOn p ↑s) : Squarefree (∏ i ∈ s, oddPrimeDiscriminant (p i))

A product of odd prime discriminants at pairwise distinct primes is squarefree.

theorem TauCeti.Multiquadratic.isFundamentalDiscriminant_prod_oddPrimeDiscriminant {ι : Type u_1} {s : Finset ι} {p : ι → ℕ} (hp : ∀ i ∈ s, Nat.Prime (p i)) (hodd : ∀ i ∈ s, Odd (p i)) (hinj : Set.InjOn p ↑s) : IsFundamentalDiscriminant (∏ i ∈ s, oddPrimeDiscriminant (p i))

A product of odd prime discriminants is a fundamental discriminant, provided the underlying odd primes are pairwise distinct. The empty product recovers isFundamentalDiscriminant_one.

theorem TauCeti.Multiquadratic.isFundamentalDiscriminant_mul_prod_oddPrimeDiscriminant_of_isEvenPrimeDiscriminant {ι : Type u_1} {s : Finset ι} {p : ι → ℕ} {e : ℤ} (he : IsEvenPrimeDiscriminant e) (hp : ∀ i ∈ s, Nat.Prime (p i)) (hodd : ∀ i ∈ s, Odd (p i)) (hinj : Set.InjOn p ↑s) : IsFundamentalDiscriminant (e * ∏ i ∈ s, oddPrimeDiscriminant (p i))

An even prime discriminant times a product of odd prime discriminants is a fundamental discriminant, provided the underlying odd primes are pairwise distinct. Together with isFundamentalDiscriminant_prod_oddPrimeDiscriminant this covers every product of pairwise coprime prime discriminants, since two even prime discriminants are never coprime; see isFundamentalDiscriminant_prod for the assembled statement.

theorem TauCeti.Multiquadratic.isFundamentalDiscriminant_prod {ι : Type u_1} {s : Finset ι} {D : ι → ℤ} (hD : ∀ i ∈ s, IsPrimeDiscriminant (D i)) (hDinj : Set.InjOn D ↑s) (heven : ∀ i ∈ s, ∀ j ∈ s, IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) : IsFundamentalDiscriminant (∏ i ∈ s, D i)

A product of distinct prime discriminants with at most one even value is a fundamental discriminant.

theorem TauCeti.Multiquadratic.isFundamentalDiscriminant_prod_of_pairwise_isCoprime {ι : Type u_1} {s : Finset ι} {D : ι → ℤ} (hD : ∀ i ∈ s, IsPrimeDiscriminant (D i)) (hcop : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (D i) (D j)) : IsFundamentalDiscriminant (∏ i ∈ s, D i)

A product of pairwise coprime prime discriminants is a fundamental discriminant.

theorem TauCeti.Multiquadratic.IsFundamentalDiscriminant.not_isSquare_rat {D : ℤ} (hD : IsFundamentalDiscriminant D) (h1 : D ≠ 1) : ¬IsSquare ↑D

A fundamental discriminant other than 1 is not a rational square. Consequently ℚ(√D) is a genuine quadratic field: this is what keeps the genus-field constructions non-degenerate.