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.

Multiquadratic fields and genus theory

TheoremDegree of a multiquadratic field over a finite index#

Lean

Sources

TheoremResidue degree one exactly at the residues#

Lean

Sources

TheoremThe number of primes above 2#

Lean

Sources

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

Lean

Sources

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

Lean

Sources

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

Lean

Sources

DefinitionThe genus character on the narrow class group#

Lean

Sources

DefinitionNumberField.NarrowClassGroup#

Lean

Sources

TheoremUnique prime-discriminant factorization of a fundamental discriminant#

Lean

Sources

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

Lean

Sources

DefinitionTauCeti.Multiquadratic.genusCharGroup#

Lean

Sources

TheoremDegree of a multiquadratic field over a finite index #

TheoremResidue degree one exactly at the residues #

TheoremThe number of primes above `2`#

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

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

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

DefinitionThe genus character on the narrow class group #

DefinitionNumberField.NarrowClassGroup #

TheoremUnique prime-discriminant factorization of a fundamental discriminant #

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

DefinitionTauCeti.Multiquadratic.genusCharGroup #