The character group of a prime-discriminant family

Let s be a finite family of distinct prime discriminants which does not contain all three even prime discriminants, and put N = |∏ P ∈ s, P|. Each quadratic character belonging to a factor P lifts to level N (primeDiscriminantCharAtLevel), and the products of these lifted characters are indexed by the subsets t of s (genusCharAtLevel). The level stays N as t shrinks — only the subset varies — which is what puts all of these characters in a single group: multiplication corresponds to symmetric difference of subsets. When t has at most one even member, the conductor of its character is |∏ P ∈ t, P|.

Consequently the subgroup generated by the factor characters has exactly 2 ^ #s elements. This is the character-group counterpart of the degree-2 ^ #s prime-discriminant compositum. It is the input for combining the individual quadratic character fixed fields inside one cyclotomic field.

The whole-family character TauCeti.Multiquadratic.genusChar s hs is the case t = Finset.univ of genusCharAtLevel: that is how TauCeti/NumberTheory/Multiquadratic/Quadratic/GenusCharacter/Dirichlet.lean defines it, so the genusChar API (its values on integers, its primitivity) is the whole-family case of the API here, and conductor_genusCharAtLevel is the subset form of isPrimitive_genusChar.

The prime-discriminant description is classical; see K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 6, and D. A. Cox, Primes of the Form x² + ny², §§3.B and 6.A.

Main definitions and results

• primeDiscriminantCharAtLevel: the character of one factor, lifted to the common level.
• genusCharAtLevel: the product character indexed by a subset of the factors.
• genusCharAtLevel_apply_int: its value at an integer coprime to the level.
• genusCharAtLevel_symmDiff: multiplication corresponds to symmetric difference.
• conductor_genusCharAtLevel: the conductor is the product of the factor conductors.
• genusCharAtLevel_injective: distinct subsets give distinct characters.
• genusCharGroup: the subgroup consisting of all subset characters, identified by genusCharGroup_eq_closure with the subgroup generated by the factor characters.
• genusCharGroupEquiv: the subsets of s are in bijection with that subgroup.
• natCard_genusCharGroup: that subgroup has 2 ^ #s elements.
• dirichletConductor_genusCharGroup: the conductor of that subgroup is the least common multiple of the |P|.

noncomputable def TauCeti.Multiquadratic.primeDiscriminantCharAtLevel (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (P : ↥s) : DirichletCharacter ℤ (∏ Q ∈ s, Q).natAbs

The character of a prime-discriminant factor, lifted to the common level |∏ P ∈ s, P|.

theorem TauCeti.Multiquadratic.primeDiscriminantCharAtLevel_def (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (P : ↥s) : primeDiscriminantCharAtLevel s hs P = (DirichletCharacter.changeLevel ⋯) (primeDiscriminantChar ↑P ⋯)

The defining equation of primeDiscriminantCharAtLevel: the factor character lifted along |P| ∣ |∏ Q ∈ s, Q|.

theorem TauCeti.Multiquadratic.primeDiscriminantCharAtLevel_apply_int (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (P : ↥s) (n : ℤ) (hn : IsCoprime n ↑(∏ Q ∈ s, Q).natAbs) : (primeDiscriminantCharAtLevel s hs P) ↑n = (primeDiscriminantChar ↑P ⋯) ↑n

At an integer coprime to the common level, a lifted prime-discriminant character agrees with the character attached to its factor.

@[simp]

theorem TauCeti.Multiquadratic.conductor_primeDiscriminantCharAtLevel (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (P : ↥s) : (primeDiscriminantCharAtLevel s hs P).conductor = (↑P).natAbs

The conductor of a lifted prime-discriminant character is the absolute value of its factor.

theorem TauCeti.Multiquadratic.isQuadratic_primeDiscriminantCharAtLevel (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (P : ↥s) : MulChar.IsQuadratic (primeDiscriminantCharAtLevel s hs P)

A lifted prime-discriminant character is quadratic.

@[simp]

theorem TauCeti.Multiquadratic.primeDiscriminantCharAtLevel_sq (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (P : ↥s) : primeDiscriminantCharAtLevel s hs P ^ 2 = 1

A lifted prime-discriminant character squares to the trivial character.

noncomputable def TauCeti.Multiquadratic.genusCharAtLevel (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (t : Finset ↥s) : DirichletCharacter ℤ (∏ P ∈ s, P).natAbs

The common-level genus character indexed by a subset of the prime-discriminant factors.

theorem TauCeti.Multiquadratic.genusCharAtLevel_def (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (t : Finset ↥s) : genusCharAtLevel s hs t = ∏ P ∈ t, primeDiscriminantCharAtLevel s hs P

The defining equation of genusCharAtLevel: the product of the lifted characters of the factors in the subset.

@[simp]

theorem TauCeti.Multiquadratic.genusCharAtLevel_empty (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : genusCharAtLevel s hs ∅ = 1

@[simp]

theorem TauCeti.Multiquadratic.genusCharAtLevel_singleton (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (P : ↥s) : genusCharAtLevel s hs {P} = primeDiscriminantCharAtLevel s hs P

@[simp]

theorem TauCeti.Multiquadratic.genusCharAtLevel_insert (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) {P : ↥s} {t : Finset ↥s} (hP : P ∉ t) : genusCharAtLevel s hs (insert P t) = primeDiscriminantCharAtLevel s hs P * genusCharAtLevel s hs t

Inserting a new factor multiplies its character into the subset character.

theorem TauCeti.Multiquadratic.genusCharAtLevel_apply_int (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (t : Finset ↥s) (n : ℤ) (hn : IsCoprime n ↑(∏ Q ∈ s, Q).natAbs) : (genusCharAtLevel s hs t) ↑n = ∏ P ∈ t, primeDiscriminantCharFun (↑P) n

At an integer coprime to the common level, a subset character is the product of the prime-discriminant character functions of its factors.

@[simp]

theorem TauCeti.Multiquadratic.genusCharAtLevel_symmDiff (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (t u : Finset ↥s) : genusCharAtLevel s hs (symmDiff t u) = genusCharAtLevel s hs t * genusCharAtLevel s hs u

Multiplication of subset characters corresponds to symmetric difference of the subsets.

theorem TauCeti.Multiquadratic.isQuadratic_genusCharAtLevel (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (t : Finset ↥s) : MulChar.IsQuadratic (genusCharAtLevel s hs t)

Every subset character is quadratic.

theorem TauCeti.Multiquadratic.conductor_genusCharAtLevel (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (t : Finset ↥s) (heven : ∀ P ∈ t, ∀ Q ∈ t, IsEvenPrimeDiscriminant ↑P → IsEvenPrimeDiscriminant ↑Q → P = Q) : (genusCharAtLevel s hs t).conductor = ∏ P ∈ t, (↑P).natAbs

If the subset contains at most one even prime discriminant, its character's conductor is the product of the absolute values of its factors.

theorem TauCeti.Multiquadratic.genusCharAtLevel_injective (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hnoall : ¬(-4 ∈ s ∧ 8 ∈ s ∧ -8 ∈ s)) : Function.Injective (genusCharAtLevel s hs)

If s does not contain all three even prime discriminants, distinct subsets of s give distinct characters of level |∏ P ∈ s, P|.

noncomputable def TauCeti.Multiquadratic.genusCharGroup (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : Subgroup (DirichletCharacter ℤ (∏ P ∈ s, P).natAbs)

The subgroup of common-level Dirichlet characters obtained by taking products over subsets of the prime-discriminant factors.

@[simp]

theorem TauCeti.Multiquadratic.mem_genusCharGroup_iff (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) {chi : DirichletCharacter ℤ (∏ P ∈ s, P).natAbs} : chi ∈ genusCharGroup s hs ↔ ∃ (t : Finset ↥s), genusCharAtLevel s hs t = chi

Membership in the prime-discriminant character group means being the character of a subset.

theorem TauCeti.Multiquadratic.genusCharGroup_eq_closure (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : genusCharGroup s hs = Subgroup.closure (Set.range (primeDiscriminantCharAtLevel s hs))

The subset characters are exactly the subgroup generated by the individual prime-discriminant characters.

noncomputable def TauCeti.Multiquadratic.genusCharGroupEquiv (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hnoall : ¬(-4 ∈ s ∧ 8 ∈ s ∧ -8 ∈ s)) : Finset ↥s ≃ ↥(genusCharGroup s hs)

If the family does not contain all three even prime discriminants, its subsets are in bijection with its character group.

@[simp]

theorem TauCeti.Multiquadratic.coe_genusCharGroupEquiv_apply (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hnoall : ¬(-4 ∈ s ∧ 8 ∈ s ∧ -8 ∈ s)) (t : Finset ↥s) : ↑((genusCharGroupEquiv s hs hnoall) t) = genusCharAtLevel s hs t

The subset equivalence sends a subset to its corresponding common-level genus character.

theorem TauCeti.Multiquadratic.natCard_genusCharGroup (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hnoall : ¬(-4 ∈ s ∧ 8 ∈ s ∧ -8 ∈ s)) : Nat.card ↥(genusCharGroup s hs) = 2 ^ s.card

If s does not contain all three even prime discriminants, its character group has one element for each subset.

@[simp]

theorem TauCeti.Multiquadratic.dirichletConductor_genusCharGroup (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) : (genusCharGroup s hs).dirichletConductor = s.lcm Int.natAbs

The conductor of the prime-discriminant character group is the least common multiple of the absolute values of the prime discriminants.