def Hex.SquareClass.Independent (ds : List ℤ) : Prop

ds are independent square classes: no nonempty sublist of ds has a product that is a square in ℚ.

Sublists rather than subsets of Fin ds.length: a sublist selects a subset of positions, so repeated radicands are handled correctly ([d, d] is not independent, its own product being d ^ 2), and the formulation inducts directly on the list. independent_iff_sublists converts to the ℤ-valued perfect-square test that an executable check performs.

Equations

• Hex.SquareClass.Independent ds = ∀ (t : List ℤ), t.Sublist ds → t ≠ [] → ¬IsSquare ↑t.prod

theorem Hex.SquareClass.independent_iff_sublists {ds : List ℤ} : Independent ds ↔ ∀ t ∈ ds.sublists, t ≠ [] → ¬IsSquare t.prod

Independence tested over ℤ, quantified over the finite list ds.sublists. This is the shape a Bool-valued executable check decides: 2 ^ ds.length - 1 integer perfect-square tests, the empty sublist being skipped.

@[instance_reducible]

instance Hex.SquareClass.decidableIndependent (ds : List ℤ) : Decidable (Independent ds)

Equations

• Hex.SquareClass.decidableIndependent ds = decidable_of_iff (∀ t ∈ ds.sublists, t ≠ [] → ¬IsSquare t.prod) ⋯

theorem Hex.SquareClass.Independent.sublist {ds t : List ℤ} (h : Independent ds) (ht : t.Sublist ds) : Independent t

A sublist of independent square classes is independent.

theorem Hex.SquareClass.Independent.of_perm {ds ds' : List ℤ} (h : Independent ds) (hp : ds.Perm ds') : Independent ds'

Independence is symmetric in the radicands.

def Hex.SquareClass.IsSquareIn (K : IntermediateField ℚ ℂ) (x : ℂ) : Prop

x is a square in the intermediate field K of ℂ / ℚ: some element of K squares to x. Phrasing this in the ambient field keeps the tower induction free of subtype coercions.

Equations

• Hex.SquareClass.IsSquareIn K x = ∃ z ∈ K, z ^ 2 = x

theorem Hex.SquareClass.intCast_mem (K : IntermediateField ℚ ℂ) (d : ℤ) : ↑d ∈ K

Every integer lies in every intermediate field of ℂ / ℚ.

theorem Hex.SquareClass.isSquareIn_iff_isSquare {K : IntermediateField ℚ ℂ} {x : ℂ} (hx : x ∈ K) : IsSquareIn K x ↔ IsSquare ⟨x, hx⟩

IsSquareIn is IsSquare read through the subtype.

theorem Hex.SquareClass.isSquareIn_sq_mul_iff {K : IntermediateField ℚ ℂ} {x y : ℂ} (hy : y ∈ K) (hy0 : y ≠ 0) : IsSquareIn K (y ^ 2 * x) ↔ IsSquareIn K x

A nonzero square factor from K is invisible to IsSquareIn K.

theorem Hex.SquareClass.ne_zero_of_not_isSquareIn {K : IntermediateField ℚ ℂ} {x : ℂ} (h : ¬IsSquareIn K x) : x ≠ 0

Zero is a square, so a non-square is nonzero.

theorem Hex.SquareClass.isSquare_ratCast_of_isSquareIn_bot {d : ℤ} (h : IsSquareIn ⊥ ↑d) : IsSquare ↑d

An integer that is a square in ℚ ⊆ ℂ is a square in ℚ.

theorem Hex.SquareClass.exists_repr_of_mem_adjoin {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {a : F} {r : E} (hr : r ^ 2 = (algebraMap F E) a) {z : E} (hz : z ∈ F⟮r⟯) : ∃ (x : F) (y : F), z = (algebraMap F E) x + (algebraMap F E) y * r

When r ^ 2 lies in F, every element of F(r) is x + y * r with x, y ∈ F: the {1, r} basis, obtained by reducing a polynomial expression modulo X ^ 2 - C a.

theorem Hex.SquareClass.isSquare_or_isSquare_mul {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (h2 : 2 ≠ 0) {a : F} (ha : ¬IsSquare a) {r : E} (hr : r ^ 2 = (algebraMap F E) a) {b : F} {z : E} (hz : z ∈ F⟮r⟯) (hzb : z ^ 2 = (algebraMap F E) b) : IsSquare b ∨ IsSquare (a * b)

Lemma A. Let F have characteristic ≠ 2, let a ∈ F not be a square in F, and let r ^ 2 = a in an extension E. If b ∈ F is a square in F(r), then b or a * b is a square in F.

Writing the witness as x + y * r, the {1, r} basis forces 2 * x * y = 0, hence x = 0 or y = 0: the two cases give b = y ^ 2 * a and b = x ^ 2.

theorem Hex.SquareClass.minpoly_eq_X_pow_two_sub_C {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {a : F} (ha : ¬IsSquare a) {r : E} (hr : r ^ 2 = (algebraMap F E) a) : minpoly F r = Polynomial.X ^ 2 - Polynomial.C a

The minimal polynomial of a square root of a non-square.

def Hex.SquareClass.sqrtSet (ds : List ℤ) : Set ℂ

The complex square roots of the entries of ds.

Equations

• Hex.SquareClass.sqrtSet ds = {x : ℂ | ∃ d ∈ ds, x ^ 2 = ↑d}

noncomputable def Hex.SquareClass.adjoinSqrt (ds : List ℤ) : IntermediateField ℚ ℂ

ℚ(√d₁, …, √dₙ) realised inside ℂ: the intermediate field generated by every complex square root of every entry of ds. Radicands may be negative, so ℝ is not enough.

Equations

• Hex.SquareClass.adjoinSqrt ds = IntermediateField.adjoin ℚ (Hex.SquareClass.sqrtSet ds)

theorem Hex.SquareClass.exists_sqrt (d : ℤ) : ∃ (r : ℂ), r ^ 2 = ↑d

Every integer has a complex square root.

@[simp]

theorem Hex.SquareClass.sqrtSet_nil : sqrtSet [] = ∅

No radicands, no square roots.

theorem Hex.SquareClass.sqrtSet_cons (d : ℤ) (ds : List ℤ) : sqrtSet (d :: ds) = {x : ℂ | x ^ 2 = ↑d} ∪ sqrtSet ds

The square-root set of a cons splits off the head radicand's roots.

theorem Hex.SquareClass.adjoin_sqrtSet_singleton {c r : ℂ} (hr : r ^ 2 = c) : IntermediateField.adjoin ℚ {x : ℂ | x ^ 2 = c} = ℚ⟮r⟯

Adjoining all square roots of c is adjoining one of them.

@[simp]

theorem Hex.SquareClass.adjoinSqrt_nil : adjoinSqrt [] = ⊥

Adjoining no square roots leaves the base field.

theorem Hex.SquareClass.adjoinSqrt_cons_sup {d : ℤ} {r : ℂ} (hr : r ^ 2 = ↑d) (ds : List ℤ) : adjoinSqrt (d :: ds) = adjoinSqrt ds ⊔ ℚ⟮r⟯

Consing a radicand adjoins one square root to the field built so far.

theorem Hex.SquareClass.adjoinSqrt_mono {ds ds' : List ℤ} (h : ∀ d ∈ ds, d ∈ ds') : adjoinSqrt ds ≤ adjoinSqrt ds'

The tower grows monotonically in the radicands.

theorem Hex.SquareClass.adjoinSqrt_le_cons (d : ℤ) (ds : List ℤ) : adjoinSqrt ds ≤ adjoinSqrt (d :: ds)

The tower grows monotonically as radicands are consed on.

theorem Hex.SquareClass.isSquareIn_or_isSquareIn_mul {F : IntermediateField ℚ ℂ} {a b : ℂ} (haF : a ∈ F) (hbF : b ∈ F) (ha : ¬IsSquareIn F a) {r : ℂ} (hr : r ^ 2 = a) (hb : IsSquareIn (F ⊔ ℚ⟮r⟯) b) : IsSquareIn F b ∨ IsSquareIn F (a * b)

Lemma A transported to intermediate fields of ℂ / ℚ, stated in the ambient field.

theorem Hex.SquareClass.not_isSquareIn_prod (built rest : List ℤ) : Independent (built ++ rest) → ∀ (t u : List ℤ), t.Sublist built → u.Sublist rest → u ≠ [] → ¬IsSquareIn (adjoinSqrt built) ↑(t ++ u).prod

The strengthened claim. Split the radicands as built ++ rest, where adjoinSqrt built is the field constructed so far. Then no subproduct that uses at least one radicand from rest is a square in adjoinSqrt built.

The strengthening is what makes the induction go through: Lemma A turns a putative square at the top of the tower into a subproduct one level down that still meets rest. At the d :: built step the four cases are the head d being selected or not, crossed with Lemma A's two conclusions:

d selected	Lemma A gives	subset used one level down
no	b is a square	t, u
no	d * b is a square	t, d :: u
yes	b = d * p is a square	t', d :: u
yes	d * b = d ^ 2 * p is a square	t', u, after cancelling d ^ 2

The last case needs d ≠ 0, which comes from d not being a square one level down. In every case u stays nonempty, so the subset still meets rest.

theorem Hex.SquareClass.not_isSquareIn_of_perm_cons {ds rest : List ℤ} {d : ℤ} (h : Independent ds) (hp : ds.Perm (d :: rest)) : ¬IsSquareIn (adjoinSqrt rest) ↑d

A radicand is not a square in the field generated by the others.

Independence is symmetric in the radicands, so this holds at an arbitrary index and not only at the top of the tower as built: pick any permutation putting the radicand of interest first.

theorem Hex.SquareClass.sqrt_mem_adjoinSqrt {ds : List ℤ} {d : ℤ} (hd : d ∈ ds) {r : ℂ} (hr : r ^ 2 = ↑d) : r ∈ adjoinSqrt ds

A chosen square root of a radicand of ds lies in the tower.

theorem Hex.SquareClass.sqrt_notMem_adjoinSqrt {ds rest : List ℤ} {d : ℤ} (h : Independent ds) (hp : ds.Perm (d :: rest)) {r : ℂ} (hr : r ^ 2 = ↑d) : r ∉ adjoinSqrt rest

A chosen square root of a radicand does not lie in the field generated by the others. This is the form the primitive-element step consumes, after permuting the radicand of interest to the front.

theorem Hex.SquareClass.relfinrank_adjoinSqrt_cons {d : ℤ} {ds : List ℤ} {r : ℂ} (hr : r ^ 2 = ↑d) (hd : ¬IsSquareIn (adjoinSqrt ds) ↑d) : (adjoinSqrt ds).relfinrank (adjoinSqrt (d :: ds)) = 2

The relative degree of one step of the tower is 2 once the new radicand is not a square in the field built so far.

theorem Hex.SquareClass.finrank_adjoinSqrt {ds : List ℤ} (h : Independent ds) : Module.finrank ℚ ↥(adjoinSqrt ds) = 2 ^ ds.length

The tower theorem, part (1). Independent square classes generate a multiquadratic field of degree exactly 2 ^ n.