Multiquadratic

Results named in Tau Ceti's TauCeti.NumberTheory.Multiquadratic modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe converse of the multiquadratic degree theorem#

Let 2 ≠ 0 in K and let L / K be a finite Galois extension whose Galois group has exponent dividing two. Then L = K(√d₁, …, √dₙ) for radicands d₁, …, dₙ ∈ K that are square-class independent — no nonempty subset product is a square — and consequently [L : K] = 2ⁿ.

TauCeti.Multiquadratic.exists_root_adjoin_range_eq_top.{u_1, u_2} {K : Type u_1} {L : Type u_2}
  [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [NeZero 2]
  (hexp : Monoid.exponent Gal(L/K) ∣ 2) :
  ∃ n d root,
    (∀ (i : Fin n), root i ^ 2 = (algebraMap K L) (d i)) ∧
      (∀ (S : Finset (Fin n)), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)) ∧
        IntermediateField.adjoin K (Set.range root) = ⊤ ∧ Module.finrank K L = 2 ^ n
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.exists_root_adjoin_range_eq_top.

Sources
LeanTauCeti.Multiquadratic.exists_root_adjoin_range_eq_top
Uses 1 · Used by 1
Proof usesDegree of a multiquadratic field over a finite index
Used byThe prime-discriminant compositum is the genus field in the imaginary quadratic case

TheoremDirichlet's theorem for prime-discriminant characters#

Let s be a finite set of prime discriminants, at most one of them even, let ε assign a sign to each, and let N be any bound. Then some odd prime q > N has χ_P(q) = ε P for every P ∈ s. In particular there are infinitely many such primes.

TauCeti.Multiquadratic.exists_prime_gt_forall_primeDiscriminantCharFun_eq {s : Finset ℤ}
  (hs : ∀ P ∈ s, TauCeti.Multiquadratic.IsPrimeDiscriminant P)
  (heven :
    ∀ P ∈ s,
      ∀ Q ∈ s,
        TauCeti.Multiquadratic.IsEvenPrimeDiscriminant P →
          TauCeti.Multiquadratic.IsEvenPrimeDiscriminant Q → P = Q)
  (ε : ℤ → ℤˣ) (N : ℕ) :
  ∃ q,
    N < q ∧
      Nat.Prime q ∧ q ≠ 2 ∧ ∀ P ∈ s, TauCeti.Multiquadratic.primeDiscriminantCharFun P ↑q = ↑(ε P)
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.exists_prime_gt_forall_primeDiscriminantCharFun_eq.

Sources
LeanTauCeti.Multiquadratic.exists_prime_gt_forall_primeDiscriminantCharFun_eq
Used by 3
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

TheoremThe multiquadratic degree theorem, restated via linear independence#

If the square classes of the radicands d : ι → Kˣ are ZMod 2-linearly independent, then the field generated over K by their square roots root i has degree 2^|ι|. This is finrank_adjoin_range consuming the structural form of square-class independence.

TauCeti.Multiquadratic.finrank_adjoin_range_of_linearIndependent.{u_1, u_2, u_3} {K : Type u_1}
  [Field K] {L : Type u_2} [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]
  (hli : LinearIndependent (ZMod 2) fun i => TauCeti.squareClass (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_of_linearIndependent.

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

TheoremThe principal genus theorem#

Let K = ℚ(√d) with d squarefree and let ∏ P ∈ s, P = fundamentalDiscriminant d be the prime-discriminant factorization of its discriminant. A narrow ideal class of K is a square exactly when every genus character is trivial on it; that is, the principal genus is the group of squares.

This is the classical statement that the genus characters cut out Cl⁺(K)² inside Cl⁺(K).

TauCeti.Multiquadratic.isSquare_iff_forall_genusCharFunNarrowClassGroupHom_eq_one.{u_1}
  {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s : 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)
  (A : NumberField.NarrowClassGroup K) :
  IsSquare A ↔
    ∀ (P : ℤ) (hP : P ∈ s),
      (TauCeti.Multiquadratic.genusCharFunNarrowClassGroupHom hs heven hprod hmin hgen hsf ⋯) A = 1
Lean

Formalized in Tau Ceti as TauCeti.Multiquadratic.isSquare_iff_forall_genusCharFunNarrowClassGroupHom_eq_one.

Sources
LeanTauCeti.Multiquadratic.isSquare_iff_forall_genusCharFunNarrowClassGroupHom_eq_one
Uses 4
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 · Dirichlet's theorem for prime-discriminant characters

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.