Genus characters on the elementary-2 quotient of the narrow class group

A genus character on the narrow class group has values in the two-element group ℤˣ, so it is trivial on squares. It therefore factors canonically through the maximal elementary-2 quotient

Cl⁺(K) / Cl⁺(K)².

Writing the quotient and the sign group additively makes the factor a ZMod 2-linear functional. This file also collects the characters indexed by the individual prime discriminants into one linear map. A character indexed by a subset is the sum of the corresponding singleton coordinates. Thus the arithmetic characters are organized as the linear family used in the genus-theoretic computation of the narrow class group's two-rank.

The construction follows the genus-character treatment in Cox, Primes of the Form x² + ny², §3.B, and Lemmermeyer, Reciprocity Laws, §2.2. The quotient factorization uses Mathlib's ModN.liftEquiv', exposed through TauCeti.elementaryTwoQuotientLinearLiftEquiv.

Main results

• genusCharFunElementaryTwoQuotientLinearMap: the genus character as a linear functional on Cl⁺(K) / Cl⁺(K)².
• genusCharFunElementaryTwoQuotientFamilyLinearMap: the linear map collecting all singleton genus characters.
• genusCharFunElementaryTwoQuotientLinearMap_eq_sum_singleton: a subset character is the sum of its singleton linear functionals.

noncomputable def TauCeti.Multiquadratic.genusCharFunElementaryTwoQuotientLinearMap {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.ElementaryTwoQuotient K →ₗ[ZMod 2] Additive ℤˣ

The genus character as a ZMod 2-linear functional on the maximal elementary-2 quotient Cl⁺(K) / Cl⁺(K)² of the narrow class group.

The target is written as Additive ℤˣ: multiplication of signs is addition in this two-element ZMod 2-module.

Equations

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

@[simp]

theorem TauCeti.Multiquadratic.genusCharFunElementaryTwoQuotientLinearMap_mk {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) (A : NumberField.NarrowClassGroup K) : (genusCharFunElementaryTwoQuotientLinearMap hs heven hprod hmin hgen hsf hts) (elementaryTwoQuotientMk A) = Additive.ofMul ((genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf hts) A)

Evaluating the factored linear genus character on the class of a narrow ideal class recovers the original narrow-class-group character.

noncomputable def TauCeti.Multiquadratic.genusCharFunElementaryTwoQuotientFamilyLinearMap {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) : NumberField.NarrowClassGroup.ElementaryTwoQuotient K →ₗ[ZMod 2] ↥s → Additive ℤˣ

The linear family of singleton genus characters, with one coordinate for each prime discriminant in s.

Equations

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

@[simp]

theorem TauCeti.Multiquadratic.genusCharFunElementaryTwoQuotientFamilyLinearMap_apply {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) (x : NumberField.NarrowClassGroup.ElementaryTwoQuotient K) (P : ↥s) : (genusCharFunElementaryTwoQuotientFamilyLinearMap hs heven hprod hmin hgen hsf) x P = (genusCharFunElementaryTwoQuotientLinearMap hs heven hprod hmin hgen hsf ⋯) x

A coordinate of the family map is the linear genus character indexed by the corresponding singleton prime discriminant.

theorem TauCeti.Multiquadratic.genusCharFunElementaryTwoQuotientLinearMap_eq_sum_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) : genusCharFunElementaryTwoQuotientLinearMap hs heven hprod hmin hgen hsf hts = ∑ P : ↥t, genusCharFunElementaryTwoQuotientLinearMap hs heven hprod hmin hgen hsf ⋯

The linear functional of a subset-indexed genus character is the sum of the singleton functionals indexed by that subset.