NYLL
Module

MultiquadraticAdjoin.lean

Nyll.SawinTotallyRealTowers.MultiquadraticAdjoin
2 declarations indexed from sourceView source ↗

Module documentation

Degree and square classes of multiquadratic extensions

A finite family of independent square classes gives an actual extension of degree two to the power of the family size. Degree and square-class classification are proved simultaneously: classification in the previous layer guarantees that the next square root gives a quadratic extension. The reverse square-class implication constructs the product of the roots.

Imports12
Imported by2

Declarations

theorem

isSquare_adjoin_of_product

L34 ↗
ClassFieldTower.Sawin.isSquare_adjoin_of_product
Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators
universe u v w
namespace ClassFieldTower.Sawin
Lean source · statement
theorem isSquare_adjoin_of_product
    (F : Type u) (Ω : Type v) [Field F] [Field Ω] [Algebra F Ω]
    {ι : Type w} (d : ι → F) (α : ι → Ω)
    (s t : Finset ι) (ht : t ⊆ s)
    (hRoot : ∀ i ∈ s, α i ^ 2 = algebraMap F Ω (d i))
    (b q : F) (hClass : b = (∏ i ∈ t, d i) * q ^ 2) :
    IsSquare (algebraMap F (IntermediateField.adjoin F (α '' (s : Set ι))) b)
theorem

finrank_and_squareClasses_adjoin_independent_squareRoots

L62 ↗
ClassFieldTower.Sawin.finrank_and_squareClasses_adjoin_independent_squareRoots
Documentation

Independent square classes generate a multiquadratic extension of the expected degree, and precisely their subproduct classes become squares.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators
universe u v w
namespace ClassFieldTower.Sawin
Lean source · statement
theorem finrank_and_squareClasses_adjoin_independent_squareRoots
    (F : Type u) (Ω : Type v) [Field F] [Field Ω] [Algebra F Ω]
    {ι : Type w} (d : ι → F) (α : ι → Ω)
    (hTwo : (2 : F) ≠ 0) (s : Finset ι)
    (hRoot : ∀ i ∈ s, α i ^ 2 = algebraMap F Ω (d i))
    (hIndependent : ∀ t : Finset ι, t ⊆ s → t.Nonempty → ¬ IsSquare (∏ i ∈ t, d i)) :
    Module.finrank F (IntermediateField.adjoin F (α '' (s : Set ι))) = 2 ^ s.card ∧
      ∀ b : F,
        IsSquare (algebraMap F (IntermediateField.adjoin F (α '' (s : Set ι))) b) ↔
          ∃ t : Finset ι, t ⊆ s ∧ ∃ q : F, b = (∏ i ∈ t, d i) * q ^ 2

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.