Genus characters on coprime ideals

For a factor t of a prime-discriminant factorization, the genus character genusCharFun t is multiplicative but can vanish on integers sharing a prime factor with t. This file packages its nonvanishing restriction as a genuine homomorphism on the monoid of nonzero integral ideals whose absolute norm is coprime to the modulus ∏ P ∈ t, P.

The homomorphism is the arithmetic input for descending genus characters to the narrow class group. The descent theorem genusCharFun_absNorm_eq_of_span_mul_eq_span_mul proves invariance under a narrow-principal comparison when its two principal factors are also coprime to the modulus; the coprime representative API supplies representatives satisfying the ideal-level condition.

The construction follows the genus-character packaging in D. A. Cox, Primes of the Form x² + ny², §3.B, and F. Lemmermeyer, Reciprocity Laws, §2.2. No external implementation is vendored here.

Main definitions and results

• genusCharFunCoprimeIdealSubmonoid: nonzero integral ideals coprime to the genus modulus.
• genusCharFunCoprimeIdealHom: the genus character as a homomorphism from that submonoid to ℤˣ, whose values are the units 1 and -1.
• genusCharFunCoprimeIdealHom_apply: the underlying integer value is the genus character of the ideal's absolute norm.

def TauCeti.Multiquadratic.genusCharFunCoprimeIdealSubmonoid {K : Type u_1} [Field K] [NumberField K] (t : Finset ℤ) : Submonoid ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))

The monoid of nonzero integral ideals whose absolute norm is coprime to the modulus formed by the prime discriminants in t. The prime-discriminant hypotheses needed for nonvanishing are separate arguments to genusCharFunCoprimeIdealHom.

Equations

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

@[simp]

theorem TauCeti.Multiquadratic.mem_genusCharFunCoprimeIdealSubmonoid_iff {K : Type u_1} [Field K] [NumberField K] {t : Finset ℤ} (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : I ∈ genusCharFunCoprimeIdealSubmonoid t ↔ IsCoprime (↑(Ideal.absNorm ↑I)) (∏ P ∈ t, P)

Membership in the coprime-ideal submonoid is coprimality of the absolute norm with the genus modulus.

noncomputable def TauCeti.Multiquadratic.genusCharFunCoprimeIdealHom {K : Type u_1} [Field K] [NumberField K] {t : Finset ℤ} (ht : ∀ P ∈ t, IsPrimeDiscriminant P) : ↥(genusCharFunCoprimeIdealSubmonoid t) →* ℤˣ

The genus character on ideals coprime to its modulus, with values in the units of ℤ. Its value on an ideal is genusCharFun t (N I), viewed as the unit 1 or -1; the prime-discriminant hypotheses ensure that this integer is nonzero.

Equations

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

@[simp]

theorem TauCeti.Multiquadratic.genusCharFunCoprimeIdealHom_apply {K : Type u_1} [Field K] [NumberField K] {t : Finset ℤ} (ht : ∀ P ∈ t, IsPrimeDiscriminant P) (I : ↥(genusCharFunCoprimeIdealSubmonoid t)) : ↑((genusCharFunCoprimeIdealHom ht) I) = genusCharFun t ↑(Ideal.absNorm ↑↑I)

The underlying integer of the coprime-ideal genus character is the genus character of the ideal's absolute norm.

theorem TauCeti.Multiquadratic.genusCharFunCoprimeIdealHom_eq_one_or_eq_neg_one {K : Type u_1} [Field K] [NumberField K] {t : Finset ℤ} (ht : ∀ P ∈ t, IsPrimeDiscriminant P) (I : ↥(genusCharFunCoprimeIdealSubmonoid t)) : (genusCharFunCoprimeIdealHom ht) I = 1 ∨ (genusCharFunCoprimeIdealHom ht) I = -1

The coprime-ideal genus character has value 1 or -1.