Genus characters on the narrow class group

The genus character of a quadratic field is initially defined only on ideals whose absolute norm is coprime to a chosen product of prime discriminants. This file uses coprime representatives to descend that arithmetic character to the whole narrow class group. The resulting homomorphism is the character package needed for the lower bound in the real quadratic genus-theory formula.

The construction follows Cox, Primes of the Form x² + ny², §3.B, and Lemmermeyer, Reciprocity Laws, §2.2. The coprime-ideal character and the strong-approximation representative theorem used here are developed in the preceding Tau Ceti modules.

Main results

• genusCharFunCoprimeIdealHom_eq_of_mk0_eq: the coprime-ideal character is constant on fibres of the map to the narrow class group.
• genusCharFunNarrowClassGroupHom: the descended genus character on Cl⁺(K).
• genusCharFunNarrowClassGroupHom_mk0: its computation on a coprime integral ideal.
• genusCharFunNarrowClassGroupHom_mk0_eq_primeDiscriminantCharFun_absNorm: the singleton character evaluated at an ideal whose norm is coprime to the selected prime discriminant.
• genusCharFunNarrowClassGroupHom_eq_prod_singleton: a subset-indexed narrow genus character is the product of its singleton characters.

theorem TauCeti.Multiquadratic.genusCharFunCoprimeIdealHom_eq_of_mk0_eq {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) {I J : ↥(genusCharFunCoprimeIdealSubmonoid t)} (hIJ : NumberField.NarrowClassGroup.mk0 ↑I = NumberField.NarrowClassGroup.mk0 ↑J) : (genusCharFunCoprimeIdealHom ⋯) I = (genusCharFunCoprimeIdealHom ⋯) J

Coprime genus characters are constant on narrow-class fibres.

The character has the same value on any two coprime integral ideals with the same narrow ideal class. This fibre invariance is what allows the character to descend from coprime ideals to the full narrow class group.

noncomputable def TauCeti.Multiquadratic.genusCharFunNarrowClassGroupHom {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) : NumberField.NarrowClassGroup K →* ℤˣ

The genus character on the narrow class group.

For a factor t of a prime-discriminant factorization, this is the homomorphism Cl⁺(K) → ℤˣ obtained by evaluating a coprime integral representative. Its definition is independent of the representative by genusCharFunCoprimeIdealHom_eq_of_mk0_eq.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Multiquadratic.genusCharFunNarrowClassGroupHom_mk0 {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) (I : ↥(genusCharFunCoprimeIdealSubmonoid t)) : (genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf hts) (NumberField.NarrowClassGroup.mk0 ↑I) = (genusCharFunCoprimeIdealHom ⋯) I

The descended genus character evaluates on a coprime ideal as the original ideal character.

@[simp]

theorem TauCeti.Multiquadratic.genusCharFunNarrowClassGroupHom_mk0_eq_primeDiscriminantCharFun_absNorm {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) (I : Ideal (NumberField.RingOfIntegers K)) (hI : I ∈ nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) (P : ℤ) (hP : P ∈ s) (hcop : IsCoprime (↑(Ideal.absNorm I)) P) : ↑((genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf ⋯) (NumberField.NarrowClassGroup.mk0 ⟨I, hI⟩)) = primeDiscriminantCharFun P ↑(Ideal.absNorm I)

The genus character of an ideal is its character at the absolute norm. Let D = ∏ P ∈ s, P be the prime-discriminant factorization for K = ℚ(√d). If a nonzero integral ideal I has absolute norm coprime to P, then the singleton genus character of its narrow class at P ∈ s is primeDiscriminantCharFun P (absNorm I).

theorem TauCeti.Multiquadratic.genusCharFunNarrowClassGroupHom_eq_prod_singleton {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) : genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf hts = ∏ P : ↥t, genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf ⋯

A genus character indexed by a set t of prime discriminants is the product of the characters indexed by the singletons in t.

Although this is immediate for the arithmetic function genusCharFun, the narrow-class-group characters are defined using coprime representatives. The statement records that their descent preserves the same product decomposition.