Genus characters of a quadratic discriminant

Genus theory attaches to a fundamental discriminant D a family of real quadratic characters, one for each prime discriminant occurring in a factorization D = P₁ ⋯ P_t (IsFundamentalDiscriminant.exists_finset_primeDiscriminant); the products of these over subsets are the genus characters of D. The character primeDiscriminantCharFun P of a single prime discriminant is built in TauCeti.NumberTheory.Multiquadratic.Legendre.PrimeDiscriminant.Character. This file defines the genus characters and proves the arithmetic fact that makes them characters of the class group: an integer coprime to D and represented by the principal form of discriminant D has all its genus characters equal to 1.

The proof splits along the cases of the definition and is elementary. Write D = P * Q. If P = p* is odd and 4n = x² - D y², then x² ≡ 4n (mod p), so n is a nonzero quadratic residue modulo p. If P is even, then Q ≡ 1 (mod 4) — that congruence is exactly what singles out the correct even prime discriminant, 24 = (-8) * (-3) rather than 8 * 3 — and n is odd; dividing x by 2 turns the hypothesis into n = u² - (P / 4) * Q * y², and a congruence modulo 8 pins n down to 1 (mod 4), to ±1 (mod 8), or to 1, 3 (mod 8) respectively, which is precisely the triviality of χ₄, χ₈ or χ₈' at n.

Because 4 * N(z) = A² - D * B² for every algebraic integer z of the quadratic field K = ℚ(√d) with D = fundamentalDiscriminant d (exists_sq_sub_fundamentalDiscriminant_mul_sq_eq_four_mul_norm), the relation says that a genus character of D is trivial at the norm of any algebraic integer of K coprime to the product of the prime discriminants indexing it. That is the first step towards reading the genus characters as characters of the narrow class group of K, whose independence is the lower bound t - 1 in the genus-theoretic 2-rank formula. Contrapositively, norm_ne_of_genusCharFun_eq_neg_one is the classical obstruction: an integer with a nontrivial genus character is not a norm.

The genus characters and this relation are classical; see D. A. Cox, Primes of the Form x² + ny², §3.B, and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.

Main definitions

• TauCeti.Multiquadratic.genusCharFun: the genus character indexed by a finite set of prime discriminants, the product of the characters it contains.

Main results

• TauCeti.Multiquadratic.primeDiscriminantCharFun_eq_one_of_four_mul_eq_sq_sub_mul_sq: the genus-character relation for a single prime discriminant P in a factorization D = P * Q.
• TauCeti.Multiquadratic.primeDiscriminantCharFun_eq_one_of_mem_of_four_mul_eq_sq_sub_mul_sq and TauCeti.Multiquadratic.genusCharFun_eq_one_of_four_mul_eq_sq_sub_mul_sq: the same relation for a prime discriminant, and for a genus character, of a prime-discriminant factorization of D.
• TauCeti.Multiquadratic.genusCharFun_mod_right': a genus character is a character modulo the absolute value of the product of its indices.
• TauCeti.Multiquadratic.genusCharFun_natCast_eq_legendreSym_prod and TauCeti.Multiquadratic.genusCharFun_natCast_eq_legendreSym: at an odd prime a genus character is the Legendre symbol of the product of its indices, and for a prime-discriminant factorization of fundamentalDiscriminant d it is the splitting symbol legendreSym q d.
• TauCeti.Multiquadratic.genusCharFun_norm_eq_one: a genus character of D is trivial at the norm of an algebraic integer of ℚ(√d) coprime to the product of its indices, and TauCeti.Multiquadratic.norm_ne_of_genusCharFun_eq_neg_one is the resulting obstruction; TauCeti.Multiquadratic.primeDiscriminantCharFun_norm_eq_one and TauCeti.Multiquadratic.norm_ne_of_primeDiscriminantCharFun_eq_neg_one are the single-index cases.

Values of the character on the principal form

theorem TauCeti.Multiquadratic.jacobiSym_eq_one_of_dvd_of_four_mul_eq_sq_sub_mul_sq {p : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) {D n x y : ℤ} (hpD : ↑p ∣ D) (hpn : ¬↑p ∣ n) (h : 4 * n = x ^ 2 - D * y ^ 2) : jacobiSym n p = 1

The odd half of the genus-character relation. If an odd prime p divides D but not n, and 4n = x² - D y², then n is a nonzero quadratic residue modulo p: reducing the hypothesis modulo p kills the D y² term and leaves 4n ≡ x², so n is the square of x / 2.

theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_eq_one_of_isEvenPrimeDiscriminant_of_four_mul_eq_sq_sub_mul_sq {P Q n x y : ℤ} (hP : IsEvenPrimeDiscriminant P) (hQ : Q % 4 = 1) (hn : ¬2 ∣ n) (h : 4 * n = x ^ 2 - P * Q * y ^ 2) : primeDiscriminantCharFun P n = 1

The even half of the genus-character relation. Let P be an even prime discriminant and Q ≡ 1 (mod 4). If an odd integer n satisfies 4n = x² - P * Q * y², then the character of P is trivial at n.

Halving x — which is even, because 4 ∣ P — rewrites the hypothesis as n = u² - (P / 4) * Q * y², and the value of n modulo 8 is then forced into the kernel of the corresponding character.

theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_eq_one_of_four_mul_eq_sq_sub_mul_sq {P Q n x y : ℤ} (hP : IsPrimeDiscriminant P) (hQ : IsEvenPrimeDiscriminant P → Q % 4 = 1) (hcop : IsCoprime n P) (h : 4 * n = x ^ 2 - P * Q * y ^ 2) : primeDiscriminantCharFun P n = 1

The genus-character relation for a single prime discriminant. Let P be a prime discriminant and Q an integer, congruent to 1 modulo 4 when P is even. An integer n coprime to P and satisfying 4n = x² - P * Q * y² has trivial character at P. When P * Q is supplied as an actual discriminant factorization, this equation says that n is represented by the principal form of discriminant P * Q.

The genus characters of a fundamental discriminant

theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_eq_one_of_mem_of_four_mul_eq_sq_sub_mul_sq {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ P' ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant P' → P = P') {P : ℤ} (hP : P ∈ s) {n x y : ℤ} (hcop : IsCoprime n P) (h : 4 * n = x ^ 2 - (∏ P ∈ s, P) * y ^ 2) : primeDiscriminantCharFun P n = 1

The genus-character relation. Let D = ∏ P ∈ s, P be a factorization of a discriminant into prime discriminants, at most one of them even, as produced by IsFundamentalDiscriminant.exists_finset_primeDiscriminant. For each P ∈ s, every integer n coprime to P and represented by the principal form of discriminant D, 4n = x² - D y², has trivial character at P.

The hypothesis that at most one member of s is even is what makes the complementary factor ∏ P' ∈ s.erase P, P' congruent to 1 modulo 4 when P is the even one.

def TauCeti.Multiquadratic.genusCharFun (s : Finset ℤ) (n : ℤ) : ℤ

The genus character indexed by a finite set s of prime discriminants: the product of the characters they carry. The genus characters of a fundamental discriminant D are those indexed by the subsets of a prime-discriminant factorization of D.

Equations

• TauCeti.Multiquadratic.genusCharFun s n = ∏ P ∈ s, TauCeti.Multiquadratic.primeDiscriminantCharFun P n

theorem TauCeti.Multiquadratic.genusCharFun_def (s : Finset ℤ) (n : ℤ) : genusCharFun s n = ∏ P ∈ s, primeDiscriminantCharFun P n

A genus character is the product of its prime-discriminant characters.

@[simp]

theorem TauCeti.Multiquadratic.genusCharFun_empty (n : ℤ) : genusCharFun ∅ n = 1

The genus character indexed by the empty set is trivial.

@[simp]

theorem TauCeti.Multiquadratic.genusCharFun_singleton (P n : ℤ) : genusCharFun {P} n = primeDiscriminantCharFun P n

A singleton genus character is its prime-discriminant character.

@[simp]

theorem TauCeti.Multiquadratic.genusCharFun_insert {s : Finset ℤ} {P : ℤ} (hP : P ∉ s) (n : ℤ) : genusCharFun (insert P s) n = primeDiscriminantCharFun P n * genusCharFun s n

Inserting a fresh prime discriminant multiplies its character into the genus character.

@[simp]

theorem TauCeti.Multiquadratic.genusCharFun_mul_right (s : Finset ℤ) (m n : ℤ) : genusCharFun s (m * n) = genusCharFun s m * genusCharFun s n

A genus character is completely multiplicative.

@[simp]

theorem TauCeti.Multiquadratic.genusCharFun_one (s : Finset ℤ) : genusCharFun s 1 = 1

A genus character takes the value 1 at 1.

theorem TauCeti.Multiquadratic.genusCharFun_mod_right' {s : Finset ℤ} {m n : ℤ} (h : m % ↑(∏ P ∈ s, P).natAbs = n % ↑(∏ P ∈ s, P).natAbs) : genusCharFun s m = genusCharFun s n

A genus character depends only on the residue class modulo the absolute value of the product of its prime-discriminant indices: each factor is a character modulo |P| (primeDiscriminantCharFun_mod_right'), and P divides that product.

@[simp]

theorem TauCeti.Multiquadratic.genusCharFun_eq_zero_iff {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) {n : ℤ} : genusCharFun s n = 0 ↔ ¬IsCoprime n (∏ P ∈ s, P)

A genus character vanishes exactly when its argument is not coprime to the product of its prime-discriminant indices.

theorem TauCeti.Multiquadratic.genusCharFun_eq_one_or_eq_neg_one {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) {n : ℤ} (hcop : IsCoprime n (∏ P ∈ s, P)) : genusCharFun s n = 1 ∨ genusCharFun s n = -1

A genus character takes the values ±1 on integers coprime to the product of its prime-discriminant indices.

theorem TauCeti.Multiquadratic.genusCharFun_eq_one_of_four_mul_eq_sq_sub_mul_sq {s t : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ P' ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant P' → P = P') (hts : t ⊆ s) {n x y : ℤ} (hcop : IsCoprime n (∏ P ∈ t, P)) (h : 4 * n = x ^ 2 - (∏ P ∈ s, P) * y ^ 2) : genusCharFun t n = 1

The genus characters are trivial on the values of the principal form. For a prime-discriminant factorization D = ∏ P ∈ s, P and any subset t ⊆ s, the genus character indexed by t is trivial at every integer coprime to the product of the factors in t that the principal form of discriminant D represents. This is the arithmetic input for a future proof that the genus characters descend to the class group.

Values at an odd prime

theorem TauCeti.Multiquadratic.genusCharFun_natCast_eq_legendreSym_prod {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) : genusCharFun s ↑q = legendreSym q (∏ P ∈ s, P)

A genus character evaluates at an odd prime as a Legendre symbol. For a set s of prime discriminants, genusCharFun s q = legendreSym q (∏ P ∈ s, P) at every odd prime q, since each prime-discriminant character is the Legendre symbol of its prime discriminant.

theorem TauCeti.Multiquadratic.genusCharFun_natCast_eq_legendreSym {s : Finset ℤ} {d : ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) : genusCharFun s ↑q = legendreSym q d

The genus character of a quadratic discriminant is its splitting symbol. For K = ℚ(√d) with discriminant D = ∏ P ∈ s, P, the genus character indexed by the whole factorization agrees at an odd prime q with legendreSym q d: the fundamental discriminant differs from d by the square of 1 or 2, which the symbol does not see.

Genus characters on the norms of a quadratic field

theorem TauCeti.Multiquadratic.genusCharFun_norm_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s t : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ P' ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant P' → P = P') (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hts : t ⊆ s) (z : NumberField.RingOfIntegers K) (hcop : IsCoprime ((Algebra.norm ℤ) z) (∏ P ∈ t, P)) : genusCharFun t ((Algebra.norm ℤ) z) = 1

The genus characters of a quadratic field are trivial on the norms of its integers. Let K = ℚ(√d) with d squarefree and let D = fundamentalDiscriminant d factor as ∏ P ∈ s, P into prime discriminants, at most one even. For a subset t ⊆ s, if the norm of an algebraic integer z of K is coprime to ∏ P ∈ t, P, then the genus character indexed by t is trivial at it.

This theorem handles element norms. Applying genus characters to ideal-class representatives will require a further argument comparing representatives through principal ideals.

theorem TauCeti.Multiquadratic.primeDiscriminantCharFun_norm_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ P' ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant P' → P = P') (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) {P : ℤ} (hP : P ∈ s) (z : NumberField.RingOfIntegers K) (hcop : IsCoprime ((Algebra.norm ℤ) z) P) : primeDiscriminantCharFun P ((Algebra.norm ℤ) z) = 1

The single-index case of genusCharFun_norm_eq_one: the character at a prime discriminant P ∈ s is trivial at the norms of the algebraic integers of ℚ(√d) that are coprime to P.

theorem TauCeti.Multiquadratic.norm_ne_of_genusCharFun_eq_neg_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s t : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ P' ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant P' → P = P') (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hts : t ⊆ s) {n : ℤ} (hchar : genusCharFun t n = -1) (z : NumberField.RingOfIntegers K) : (Algebra.norm ℤ) z ≠ n

Genus characters obstruct norms. If a genus character of the quadratic field K = ℚ(√d), indexed by a subset t of a prime-discriminant factorization of its fundamental discriminant, takes the value -1 at an integer n, then n is not the norm of any algebraic integer of K. This is the form in which genus theory rules out representations.

theorem TauCeti.Multiquadratic.norm_ne_of_primeDiscriminantCharFun_eq_neg_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ P' ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant P' → P = P') (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) {P n : ℤ} (hP : P ∈ s) (hchar : primeDiscriminantCharFun P n = -1) (z : NumberField.RingOfIntegers K) : (Algebra.norm ℤ) z ≠ n

The single-index case of norm_ne_of_genusCharFun_eq_neg_one: an integer at which the character of a prime discriminant P ∈ s takes the value -1 is not the norm of an algebraic integer of ℚ(√d).