theorem Hex.SquareClass.isIntegral_of_sq {d : ℤ} {r : ℂ} (hr : r ^ 2 = ↑d) : IsIntegral ℚ r

A complex square root of an integer is integral over ℚ.

theorem Hex.SquareClass.rootSet_X_pow_two_sub_C (d : ℤ) : (Polynomial.X ^ 2 - Polynomial.C ↑d).rootSet ℂ = {x : ℂ | x ^ 2 = ↑d}

The complex roots of X ^ 2 - d are the complex square roots of d.

theorem Hex.SquareClass.normal_adjoin_sqrt {d : ℤ} {r : ℂ} (hr : r ^ 2 = ↑d) : Normal ℚ ↥ℚ⟮r⟯

A quadratic subfield of the tower is normal: it splits X ^ 2 - d.

instance Hex.SquareClass.finiteDimensional_adjoinSqrt (ds : List ℤ) : FiniteDimensional ℚ ↥(adjoinSqrt ds)

instance Hex.SquareClass.normal_adjoinSqrt (ds : List ℤ) : Normal ℚ ↥(adjoinSqrt ds)

instance Hex.SquareClass.isGalois_adjoinSqrt (ds : List ℤ) : IsGalois ℚ ↥(adjoinSqrt ds)

def Hex.SquareClass.signSum {R : Type u_1} [Ring R] {n : ℕ} (c : ℤ) (r : Fin n → R) (ε : Fin n → Bool) : R

The sign-pattern sum c + ∑ᵢ ± rᵢ, where ε i selects the sign of the i-th root. Stated over an arbitrary ring so that the tower and the ambient ℂ share one definition.

Equations

• Hex.SquareClass.signSum c r ε = ↑c + ∑ i : Fin n, if ε i = true then r i else -r i

theorem Hex.SquareClass.signSum_const_true {R : Type u_1} [Ring R] {n : ℕ} (c : ℤ) (r : Fin n → R) : (signSum c r fun (x : Fin n) => true) = ↑c + ∑ i : Fin n, r i

The all-plus pattern gives the untwisted sum c + ∑ᵢ rᵢ.

theorem Hex.SquareClass.map_signSum {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {n : ℕ} (f : R →+* S) (c : ℤ) (r : Fin n → R) (ε : Fin n → Bool) : f (signSum c r ε) = signSum c (fun (i : Fin n) => f (r i)) ε

A ring map carries a sign-pattern sum to the sign-pattern sum of the images.

noncomputable def Hex.SquareClass.signPoly {R : Type u_1} [CommRing R] {n : ℕ} (c : ℤ) (r : Fin n → R) : Polynomial R

The sign-pattern product ∏_ε (X - (c + ∑ᵢ ± rᵢ)), the candidate minimal polynomial.

Equations

• Hex.SquareClass.signPoly c r = ∏ ε : Fin n → Bool, (Polynomial.X - Polynomial.C (Hex.SquareClass.signSum c r ε))

theorem Hex.SquareClass.signPoly_monic {R : Type u_1} [CommRing R] {n : ℕ} (c : ℤ) (r : Fin n → R) : (signPoly c r).Monic

The sign-pattern product is monic, being a product of monic linear factors.

theorem Hex.SquareClass.natDegree_signPoly {R : Type u_1} [CommRing R] [Nontrivial R] {n : ℕ} (c : ℤ) (r : Fin n → R) : (signPoly c r).natDegree = 2 ^ n

The sign-pattern product has degree 2 ^ n, one factor per sign pattern.

theorem Hex.SquareClass.map_signPoly {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : ℕ} (f : R →+* S) (c : ℤ) (r : Fin n → R) : Polynomial.map f (signPoly c r) = signPoly c fun (i : Fin n) => f (r i)

A ring map carries the sign-pattern product to the sign-pattern product of the images.

theorem Hex.SquareClass.signPoly_eval {R : Type u_1} [CommRing R] {n : ℕ} (c : ℤ) (r : Fin n → R) : Polynomial.eval (signSum c r fun (x : Fin n) => true) (signPoly c r) = 0

The all-plus pattern is a root of the sign-pattern product.

theorem Hex.SquareClass.getElem_mem_eraseIdx {α : Type u_1} {l : List α} {i j : Fin l.length} (hij : i ≠ j) : l[i] ∈ l.eraseIdx ↑j

Every entry except the j-th survives erasing position j.

theorem Hex.SquareClass.perm_eraseIdx {α : Type u_1} [DecidableEq α] (l : List α) (j : Fin l.length) : l.Perm (l[j] :: l.eraseIdx ↑j)

Erasing position j and putting the j-th entry back in front recovers the list.

theorem Hex.SquareClass.eq_zero_of_sum_eq_zero {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) {a : Fin ds.length → ℤ} (ha : ∑ i : Fin ds.length, ↑(a i) * r i = 0) (j : Fin ds.length) : a j = 0

No integer linear relation holds among square roots of independent radicands.

theorem Hex.SquareClass.adjoinSqrt_le {M : IntermediateField ℚ ℂ} (ds : List ℤ) : (∀ (x : ℂ), ∀ d ∈ ds, x ^ 2 = ↑d → x ∈ M) → adjoinSqrt ds ≤ M

An intermediate field containing every square root of every radicand contains the tower.

theorem Hex.SquareClass.eq_top_of_sqrt_mem {ds : List ℤ} (N : IntermediateField ℚ ↥(adjoinSqrt ds)) (hN : ∀ (x : ℂ), ∀ d ∈ ds, x ^ 2 = ↑d → x ∈ IntermediateField.map (adjoinSqrt ds).val N) : N = ⊤

An intermediate field of the tower whose image in ℂ contains every square root of every radicand is the whole tower.

theorem Hex.SquareClass.eq_or_neg_of_sq {K : Type u_1} [Field K] [Algebra ℚ K] (σ : Gal(K/ℚ)) {x : K} {d : ℤ} (hx : x ^ 2 = ↑d) : σ x = x ∨ σ x = -x

An automorphism sends a square root of an integer to plus or minus itself.

def Hex.SquareClass.root {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (i : Fin ds.length) : ↥(adjoinSqrt ds)

The chosen square roots, as elements of the tower.

Equations

• Hex.SquareClass.root hr i = ⟨r i, ⋯⟩

@[simp]

theorem Hex.SquareClass.root_val {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (i : Fin ds.length) : ↑(root hr i) = r i

The chosen root's underlying complex value.

theorem Hex.SquareClass.root_sq {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (i : Fin ds.length) : root hr i ^ 2 = ↑ds[i]

The chosen root squares to its radicand inside the tower.

noncomputable def Hex.SquareClass.signOf {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (σ : Gal(↥(adjoinSqrt ds)/ℚ)) (i : Fin ds.length) : Bool

The sign pattern by which σ acts on the chosen roots.

Equations

• Hex.SquareClass.signOf hr σ i = decide (σ (Hex.SquareClass.root hr i) = Hex.SquareClass.root hr i)

theorem Hex.SquareClass.getElem_ne_zero {ds : List ℤ} (h : Independent ds) (i : Fin ds.length) : ds[i] ≠ 0

A radicand of independent square classes is nonzero: 0 is a square.

theorem Hex.SquareClass.root_ne_neg_self {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (i : Fin ds.length) : root hr i ≠ -root hr i

A chosen root of an independent radicand is not its own negative.

theorem Hex.SquareClass.apply_root {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (σ : Gal(↥(adjoinSqrt ds)/ℚ)) (i : Fin ds.length) : σ (root hr i) = if signOf hr σ i = true then root hr i else -root hr i

Every automorphism of the tower acts on the chosen roots by its sign pattern.

theorem Hex.SquareClass.signOf_eq_of_apply {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) {σ : Gal(↥(adjoinSqrt ds)/ℚ)} {i : Fin ds.length} {b : Bool} (hb : σ (root hr i) = if b = true then root hr i else -root hr i) : signOf hr σ i = b

Reading a sign off an action recovers the sign pattern, the roots being nonzero.

noncomputable def Hex.SquareClass.gen {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : ↥(adjoinSqrt ds)

α = c + ∑ᵢ √dᵢ, as an element of the tower.

Equations

• Hex.SquareClass.gen hr c = Hex.SquareClass.signSum c (Hex.SquareClass.root hr) fun (x : Fin ds.length) => true

@[simp]

theorem Hex.SquareClass.gen_val {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : ↑(gen hr c) = signSum c r fun (x : Fin ds.length) => true

The generator's underlying complex value is the all-plus sign sum.

theorem Hex.SquareClass.eq_one_of_root_fixed {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) {σ : Gal(↥(adjoinSqrt ds)/ℚ)} (hσ : ∀ (i : Fin ds.length), σ (root hr i) = root hr i) : σ = 1

Only the identity fixes every chosen root.

theorem Hex.SquareClass.eq_one_of_gen_fixed {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) {σ : Gal(↥(adjoinSqrt ds)/ℚ)} (hσ : σ (gen hr c) = gen hr c) : σ = 1

Trivial stabilizer. Only the identity fixes the primitive element.

theorem Hex.SquareClass.fixingSubgroup_adjoin_gen {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : ℚ⟮gen hr c⟯.fixingSubgroup = ⊥

Nothing but the identity fixes ℚ(α) pointwise.

theorem Hex.SquareClass.adjoin_gen_eq_top {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : ℚ⟮gen hr c⟯ = ⊤

The tower theorem, part (2), read inside the tower.

theorem Hex.SquareClass.signOf_injective {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) : Function.Injective (signOf hr)

An automorphism is determined by its sign pattern, the roots generating the tower.

@[simp]

theorem Hex.SquareClass.signOf_one {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) : signOf hr 1 = fun (x : Fin ds.length) => true

The identity acts by the all-plus pattern.

theorem Hex.SquareClass.signOf_mul {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (σ τ : Gal(↥(adjoinSqrt ds)/ℚ)) : signOf hr (σ * τ) = fun (i : Fin ds.length) => signOf hr σ i == signOf hr τ i

Composing automorphisms multiplies sign patterns pointwise. Bool under == with true as identity is ℤ/2, so this is the homomorphism law that turns signOf_bijective into the isomorphism Gal(K/ℚ) ≅ (ℤ/2)ⁿ.

theorem Hex.SquareClass.signOf_bijective {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) : Function.Bijective (signOf hr)

The Galois group is (ℤ/2)ⁿ. Reading σ off as the sign pattern by which it acts on the chosen roots is a bijection onto the 2ⁿ sign patterns: injective because the roots generate the tower, surjective by the degree theorem. It is a group homomorphism by signOf_mul.

theorem Hex.SquareClass.signSum_congr {R : Type u_1} [Ring R] {n : ℕ} (c : ℤ) {r r' : Fin n → R} {ε ε' : Fin n → Bool} (h : ∀ (i : Fin n), (if ε i = true then r i else -r i) = if ε' i = true then r' i else -r' i) : signSum c r ε = signSum c r' ε'

Sign-pattern sums agree when their signed summands do.

theorem Hex.SquareClass.signPoly_comp_algEquiv {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) (σ : Gal(↥(adjoinSqrt ds)/ℚ)) : (signPoly c fun (i : Fin ds.length) => σ (root hr i)) = signPoly c (root hr)

An automorphism permutes the sign patterns by exclusive-or with its own.

theorem Hex.SquareClass.exists_monic_map_eq_signPoly {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : ∃ (Q : Polynomial ℚ), Q.Monic ∧ Polynomial.map (algebraMap ℚ ↥(adjoinSqrt ds)) Q = signPoly c (root hr)

The sign-pattern product has coefficients in ℚ.

theorem Hex.SquareClass.natDegree_minpoly_gen {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : (minpoly ℚ (gen hr c)).natDegree = 2 ^ ds.length

α has degree 2 ^ n over ℚ, by the Galois correspondence and the degree theorem.

theorem Hex.SquareClass.minpoly_gen_map {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : Polynomial.map (algebraMap ℚ ↥(adjoinSqrt ds)) (minpoly ℚ (gen hr c)) = signPoly c (root hr)

The tower theorem, part (3), read inside the tower.

theorem Hex.SquareClass.minpoly_signSum {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : minpoly ℚ (signSum c r fun (x : Fin ds.length) => true) = minpoly ℚ (gen hr c)

The minimal polynomial of α is computed inside the tower.

theorem Hex.SquareClass.minpoly_map_eq_signPoly {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ (signSum c r fun (x : Fin ds.length) => true)) = signPoly c r

The tower theorem, part (3). The minimal polynomial is the sign-pattern product.

theorem Hex.SquareClass.isIntegral_signSum {ds : List ℤ} {r : Fin ds.length → ℂ} (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : IsIntegral ℚ (signSum c r fun (x : Fin ds.length) => true)

α is integral over ℚ, lying in a finite extension.

theorem Hex.SquareClass.natDegree_minpoly_signSum {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : (minpoly ℚ (signSum c r fun (x : Fin ds.length) => true)).natDegree = 2 ^ ds.length

α has degree 2 ^ n over ℚ.

theorem Hex.SquareClass.adjoin_signSum_eq {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) : ℚ⟮signSum c r fun (x : Fin ds.length) => true⟯ = adjoinSqrt ds

The tower theorem, part (2). α = c + ∑ᵢ √dᵢ generates the whole tower.

theorem Hex.SquareClass.irreducible_of_map_eq_signPoly {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) {f : Polynomial ℚ} (hf : Polynomial.map (algebraMap ℚ ℂ) f = signPoly c r) : Irreducible f

The consequence the certificate needs. A rational polynomial that is the sign-pattern product of independent square classes is irreducible: it is the minimal polynomial of α.

theorem Hex.SquareClass.irreducible_int_of_map_eq_signPoly {ds : List ℤ} {r : Fin ds.length → ℂ} (h : Independent ds) (hr : ∀ (i : Fin ds.length), r i ^ 2 = ↑ds[i]) (c : ℤ) {f : Polynomial ℤ} (hfm : f.Monic) (hf : Polynomial.map (Int.castRingHom ℂ) f = signPoly c r) : Irreducible f

The same over ℤ, by Gauss's lemma: a monic integer sign-pattern product is irreducible.