Multiquadratic fields and genus theory

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremDegree of a multiquadratic field over a finite index#

If no nonempty subset product of the radicands d i is a square in K, then [K(rootᵢ : i) : K] = 2^|ι|.

TauCeti.Multiquadratic.finrank_adjoin_range.{u_1, u_2, u_3} {K : Type u_1} {L : Type u_2} [Field K]
  [Field L] [Algebra K L] {ι : Type u_3} [Finite ι] {d : ι → K} {root : ι → L}
  (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) [NeZero 2]
  (hindep : ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)) :
  Module.finrank K ↥(IntermediateField.adjoin K (Set.range root)) = 2 ^ Nat.card ι
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.finrank_adjoin_range.

Sources
LeanTauCeti.Multiquadratic.finrank_adjoin_range
Used by 5
Used byThe genus-field isomorphism Gal(K_gen/K) ≅ Cl⁺(K)/Cl⁺(K)² · The number of primes above 2 · The prime-discriminant compositum is the genus field in the imaginary quadratic case · The converse of the multiquadratic degree theorem · The multiquadratic degree theorem, restated via linear independence

TheoremResidue degree one exactly at the residues#

Let K be generated over ℚ by square roots r i of integers d i, and let Q be a prime of 𝓞 K above an odd prime p dividing none of the d i. Then Q has residue degree 1 iff every d i is a quadratic residue mod p.

TauCeti.Multiquadratic.inertiaDeg_eq_one_iff_forall_legendreSym_eq_one.{u_1, u_2} {K : Type u_1}
  [Field K] [NumberField K] {ι : Type u_2} {d : ι → ℤ} {r : ι → K} {p : ℕ} [Fact (Nat.Prime p)]
  [Finite ι] (hr : ∀ (i : ι), r i ^ 2 = (algebraMap ℤ K) (d i))
  (htop : IntermediateField.adjoin ℚ (Set.range r) = ⊤) (hodd : p ≠ 2) (hcop : ∀ (i : ι), ¬↑p ∣ d i)
  (Q : Ideal (NumberField.RingOfIntegers K)) [Q.IsPrime] [Q.LiesOver (Ideal.span {↑p})] :
  Q.inertiaDeg ℤ = 1 ↔ ∀ (i : ι), legendreSym p (d i) = 1
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.inertiaDeg_eq_one_iff_forall_legendreSym_eq_one.

Sources
LeanTauCeti.Multiquadratic.inertiaDeg_eq_one_iff_forall_legendreSym_eq_one

TheoremThe number of primes above 2#

Let K be generated over ℚ by square roots of n square-class independent integers d i (no nonempty subset product is a square) not divisible by 4. Then there are exactly 2 ^ (n - a - b) primes of 𝓞 K above 2, where the ramification index is e = 2 ^ a and the residue degree is f = 2 ^ b:

  • a = 2 when some d i is 3 modulo 4 and some d j is even, or some d i is 2 and some d j is 6 modulo 8; otherwise a = 0 when every d i is 1 modulo 4, and a = 1 when not;
  • b = 1 when some subset product ∏_{i ∈ T} dᵢ lies in the rational square class of an integer that is 5 modulo 8, and b = 0 otherwise.
TauCeti.Multiquadratic.ncard_primesOver_two_eq_two_pow_sub.{u_1, u_2} {K : Type u_1} [Field K]
  [NumberField K] {ι : Type u_2} [Finite ι] {d : ι → ℤ} {r : ι → K}
  (hr : ∀ (i : ι), r i ^ 2 = (algebraMap ℤ K) (d i))
  (htop : IntermediateField.adjoin ℚ (Set.range r) = ⊤) (hd : ∀ (i : ι), ¬4 ∣ d i)
  (hindep : ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, ↑(d i))) :
  ((Ideal.span {2}).primesOver (NumberField.RingOfIntegers K)).ncard =
    2 ^
      (Nat.card ι -
        ((if (∃ i j, d i % 4 = 3 ∧ 2 ∣ d j) ∨ ∃ i j, d i % 8 = 2 ∧ d j % 8 = 6 then 2
          else if ∀ (i : ι), d i % 4 = 1 then 0 else 1) +
          if ∃ T c q, c % 8 = 5 ∧ q ≠ 0 ∧ ∏ i ∈ T, ↑(d i) = ↑c * q ^ 2 then 1 else 0))
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.ncard_primesOver_two_eq_two_pow_sub.

Sources
LeanTauCeti.Multiquadratic.ncard_primesOver_two_eq_two_pow_sub
Uses 1
Proof usesDegree of a multiquadratic field over a finite index

TheoremThe prime-discriminant compositum is the genus field in the imaginary quadratic case#

For a squarefree negative integer d, candidateGenusField hd is abelian over ℚ, is unramified at every place over its embedded copy of ℚ(√d), and admits a root-preserving embedding from every other abelian extension with those properties.

TauCeti.Multiquadratic.isGenusField_candidateGenusField.{v} {d : ℤ} (hd : Squarefree d)
  (hneg : d < 0) :
  TauCeti.Multiquadratic.IsGenusField d (↥(TauCeti.Multiquadratic.candidateGenusField hd))
    (TauCeti.Multiquadratic.candidateGenusFieldBaseRoot hd)
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.isGenusField_candidateGenusField.

Sources
LeanTauCeti.Multiquadratic.isGenusField_candidateGenusField
Uses 2
Proof usesThe converse of the multiquadratic degree theorem · Degree of a multiquadratic field over a finite index

DefinitionThe genus-field isomorphism Gal(K_gen/K) ≅ Cl⁺(K)/Cl⁺(K)²#

For a squarefree integer d that is not a rational square, the Galois group of the candidate genus field over its embedded quadratic base K = ℚ(√d) is isomorphic to the maximal elementary-2 quotient of the narrow class group of K. Both are the space of even-parity sign patterns on the prime discriminants dividing disc K: the Galois group by its sign patterns, the class group by its genus characters.

The map is pinned down coordinate for coordinate on those prime discriminants: it sends an automorphism σ to the unique narrow class modulo squares whose genus characters are the signs that σ puts on the chosen square roots (autCandidateGenusFieldEquivNarrowElementaryTwoQuotient_apply together with narrowElementaryTwoQuotientEquivRelativeSign_apply_coe). Its identification with the inverse Artin map of K_gen / K is not proved here; see the module docstring.

TauCeti.Multiquadratic.autCandidateGenusFieldEquivNarrowElementaryTwoQuotient {d : ℤ}
  (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) :
  Gal(↥(TauCeti.Multiquadratic.candidateGenusField
          hd)/↥(TauCeti.Multiquadratic.candidateGenusFieldBase hd)) ≃*
    Multiplicative
      (NumberField.NarrowClassGroup.ElementaryTwoQuotient
        ↥(TauCeti.Multiquadratic.candidateGenusFieldBase hd))
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.autCandidateGenusFieldEquivNarrowElementaryTwoQuotient.

Sources
LeanTauCeti.Multiquadratic.autCandidateGenusFieldEquivNarrowElementaryTwoQuotient
Uses 5
Statement usesThe genus character on the narrow class group · NumberField.NarrowClassGroup
Proof usesThe 2-rank formula for the narrow class group of a quadratic field · Degree of a multiquadratic field over a finite index · Dirichlet's theorem for prime-discriminant characters

TheoremThe 2-rank formula for the narrow class group of a quadratic field#

For K = ℚ(√d) with d squarefree, of either signature, the 2-rank of Cl⁺(K) is exactly t - 1, where t is the number of rational primes ramifying in K. For an imaginary K the narrow and ordinary class groups coincide, and this recovers twoRank_eq_ncard_ramifiedPrimes_sub_one; that identity is also how the Gaussian field d = -1, which the ambiguous class number bound excludes, is covered.

TauCeti.Multiquadratic.narrowTwoRank_eq_ncard_ramifiedPrimes_sub_one.{u_1} {K : Type u_1} [Field K]
  [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ}
  (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) :
  NumberField.NarrowClassGroup.twoRank K = (NumberField.ramifiedPrimes K).ncard - 1
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.narrowTwoRank_eq_ncard_ramifiedPrimes_sub_one.

Sources
LeanTauCeti.Multiquadratic.narrowTwoRank_eq_ncard_ramifiedPrimes_sub_one
Uses 5 · Used by 2
Statement usesNumberField.NarrowClassGroup
Proof usesDirichlet's theorem for prime-discriminant characters · Dirichlet's unit theorem (NumberField.fg_units_integralClosure) · The genus character on the narrow class group · Hilbert's Theorem 90 for quadratic conjugation
Used byThe genus-field isomorphism Gal(K_gen/K) ≅ Cl⁺(K)/Cl⁺(K)² · The principal genus theorem

DefinitionThe 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.

TauCeti.Multiquadratic.genusCharFunNarrowClassGroupHom.{u_1} {K : Type u_1} [Field K]
  [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s t : Finset ℤ}
  (hs : ∀ P ∈ s, TauCeti.Multiquadratic.IsPrimeDiscriminant P)
  (heven :
    ∀ P ∈ s,
      ∀ P' ∈ s,
        TauCeti.Multiquadratic.IsEvenPrimeDiscriminant P →
          TauCeti.Multiquadratic.IsEvenPrimeDiscriminant P' → P = P')
  (hprod : ∏ P ∈ s, P = TauCeti.Multiquadratic.fundamentalDiscriminant d)
  (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d)
  (hts : t ⊆ s) : NumberField.NarrowClassGroup K →* ℤˣ
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.genusCharFunNarrowClassGroupHom.

Sources
LeanTauCeti.Multiquadratic.genusCharFunNarrowClassGroupHom
Uses 1 · Used by 3
Statement usesNumberField.NarrowClassGroup
Used byThe 2-rank formula for the narrow class group of a quadratic field · The genus-field isomorphism Gal(K_gen/K) ≅ Cl⁺(K)/Cl⁺(K)² · The principal genus theorem

DefinitionNumberField.NarrowClassGroup#

The narrow class group Cl⁺(K): invertible fractional ideals of 𝓞 K modulo the principal ones with a totally positive generator.

NumberField.NarrowClassGroup.{u_1} (K : Type u_1) [Field K] [NumberField K] : Type u_1
Lean

Formalized in Tau Ceti as NumberField.NarrowClassGroup.

Sources
LeanNumberField.NarrowClassGroup
Used by 4
Used byThe 2-rank formula for the narrow class group of a quadratic field · The genus character on the narrow class group · The genus-field isomorphism Gal(K_gen/K) ≅ Cl⁺(K)/Cl⁺(K)² · The principal genus theorem

TheoremUnique prime-discriminant factorization of a fundamental discriminant#

Every fundamental discriminant is the product of a unique finite set of prime discriminants.

Int.IsFundamentalDiscr.existsUnique_finset_primeDiscriminant {D : ℤ} (hD : D.IsFundamentalDiscr) :
  ∃! s, (∀ P ∈ s, TauCeti.Multiquadratic.IsPrimeDiscriminant P) ∧ ∏ P ∈ s, P = D
Lean

Formalized in Tau Ceti as Int.IsFundamentalDiscr.existsUnique_finset_primeDiscriminant.

Sources
LeanInt.IsFundamentalDiscr.existsUnique_finset_primeDiscriminant

TheoremThe candidate genus field is cut out of the cyclotomic field by the genus characters#

For squarefree d with fundamental discriminant D and a cyclotomic subfield K ⊆ ℂ of level |D|, the candidate genus field of ℚ(√d) is the image in ℂ of the intermediate field of K that the character correspondence attaches to the genus character group of D. The correspondence is taken for the abelian Galois structure of the cyclotomic extension.

TauCeti.Multiquadratic.candidateGenusField_eq_map_characterSubfield_genusCharGroup.{u_1} {d : ℤ}
  (hd : Squarefree d) (K : IntermediateField ℚ ℂ) [NumberField ↥K]
  [IsCyclotomicExtension {(∏ P ∈ TauCeti.Multiquadratic.genusPrimeDiscriminants hd, P).natAbs} ℚ ↥K]
  (R : Type u_1) [CommRing R] [CharZero R]
  [HasEnoughRootsOfUnity R
      (Monoid.exponent
        (ZMod (∏ P ∈ TauCeti.Multiquadratic.genusPrimeDiscriminants hd, P).natAbs)ˣ)] :
  TauCeti.Multiquadratic.candidateGenusField hd =
    IntermediateField.map K.val
      ((IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar
            (∏ P ∈ TauCeti.Multiquadratic.genusPrimeDiscriminants hd, P).natAbs (↥K) R).symm
        (Subgroup.map (MulChar.ringHomCompHom (Int.castRingHom R))
          (TauCeti.Multiquadratic.genusCharGroup (TauCeti.Multiquadratic.genusPrimeDiscriminants hd)
            ⋯)))
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.candidateGenusField_eq_map_characterSubfield_genusCharGroup.

Sources
LeanTauCeti.Multiquadratic.candidateGenusField_eq_map_characterSubfield_genusCharGroup
Uses 1
Statement usesTauCeti.Multiquadratic.genusCharGroup

DefinitionTauCeti.Multiquadratic.genusCharGroup#

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

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

Formalized in Tau Ceti as TauCeti.Multiquadratic.genusCharGroup.

Sources
LeanTauCeti.Multiquadratic.genusCharGroup
Used by 1
Used byThe candidate genus field is cut out of the cyclotomic field by the genus characters

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.