Constructible Closure

(Real or complex) constructible numbers are those that can be built from integers using only the operations of addition, subtraction, multiplication, multiplicative inverse, and square roots. This is equivalent to say that a constructible number lies in a series of quadratic extensions of rational numbers.

We slightly generalize this concept to any base field K and the embient field L, and define constructibleClosure as the IntermediateField K L that is the union of all iterated quadratic extension of K.

Main Declarations

• IsIteratedQuadraticExtension K L is a predicate saying there is a series of quadratic extension from K to L.
• constructibleClosure K L is the constructible closure of K within L.
• isPowerOfTwo_natDegree_minpoly_of_mem_constructibleClosure: the degree of a number in the constructible closure is always a power of two.
• mem_constructibleClosure_complex_iff: the projection of complex constructible numbers on to real and imaginary parts are exactly real constructible numbers.

theorem IntermediateField.relrank_le_relrank_of_le_left {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {A B C : IntermediateField K L} (h : A ≤ B) : B.relrank C ≤ A.relrank C

theorem IntermediateField.relrank_sup_left_le {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] (M B : IntermediateField K L) (h : M.relrank B < Cardinal.aleph0) : M.relrank (M ⊔ B) ≤ M.relrank B

theorem IntermediateField.relrank_sup {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] (e f g : IntermediateField K L) (hef : e.relrank f < Cardinal.aleph0) : (e ⊔ g).relrank (f ⊔ g) ≤ e.relrank f

inductive IsIteratedQuadraticExtension {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] : IntermediateField K L → Prop

• bot {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] : IsIteratedQuadraticExtension ⊥
• extension {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] (f g : IntermediateField K L) (hf : IsIteratedQuadraticExtension f) (hfg : f ≤ g) (hg : f.relrank g = 2) : IsIteratedQuadraticExtension g

theorem IsIteratedQuadraticExtension.induction {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] (P : IntermediateField K L → Prop) (bot : P ⊥) (extension : ∀ (f g : IntermediateField K L), IsIteratedQuadraticExtension f → f ≤ g → f.relrank g = 2 → P f → P g) {f : IntermediateField K L} (hf : IsIteratedQuadraticExtension f) : P f

theorem isIteratedQuadraticExtension_of_exists_tower {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {f : IntermediateField K L} {n : ℕ} (g : Fin (n + 1) → IntermediateField K L) (hbot : g 0 = ⊥) (htop : g (Fin.last n) = f) (hle : ∀ (k : Fin n), g k.castSucc ≤ g k.succ) (h : ∀ (k : Fin n), (g k.castSucc).relrank (g k.succ) = 2) : IsIteratedQuadraticExtension f

theorem Sylow.exists_subgroup_tower {G : Type u_4} [Group G] {p n : ℕ} (hp : Nat.Prime p) (h : Nat.card G = p ^ n) : ∃ (f : Fin (n + 1) → Subgroup G), (∀ (k : Fin (n + 1)), Nat.card ↥(f k) = p ^ ↑k) ∧ ∀ (k : Fin n), f k.castSucc ≤ f k.succ

theorem IsIteratedQuadraticExtension.isPowerOfTwo_finrank {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {f : IntermediateField K L} (hf : IsIteratedQuadraticExtension f) : (Module.finrank K ↥f).isPowerOfTwo

theorem isIteratedQuadraticExtension_iff_isPowerOfTwo_finrank {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {f : IntermediateField K L} (hf : IsGalois K ↥f) : IsIteratedQuadraticExtension f ↔ (Module.finrank K ↥f).isPowerOfTwo

theorem Nat.isPowerOfTwo.dvd {m n : ℕ} (h : n.isPowerOfTwo) (hdvd : m ∣ n) : m.isPowerOfTwo

theorem IsIteratedQuadraticExtension.isPowerOfTwo_natDegree_minpoly {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {f : IntermediateField K L} (hf : IsIteratedQuadraticExtension f) {x : L} (hx : x ∈ f) : (minpoly K x).natDegree.isPowerOfTwo

theorem IsIteratedQuadraticExtension.mem_induction {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] (h0 : 2 ≠ 0) (P : L → Prop) (bot : ∀ (x : K), P ((algebraMap K L) x)) (add : ∀ (x y : L), P x → P y → P (x + y)) (inv : ∀ (x : L), P x → P x⁻¹) (mul : ∀ (x y : L), P x → P y → P (x * y)) (sqrt : ∀ (x : L), P (x ^ 2) → P x) {f : IntermediateField K L} (hf : IsIteratedQuadraticExtension f) (x : L) : x ∈ f → P x

theorem IsIteratedQuadraticExtension.extension' {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {f g : IntermediateField K L} (hf : IsIteratedQuadraticExtension f) (hfg : f ≤ g) (hg : f.relrank g ≤ 2) : IsIteratedQuadraticExtension g

theorem IsIteratedQuadraticExtension.sup {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {f g : IntermediateField K L} (hf : IsIteratedQuadraticExtension f) (hg : IsIteratedQuadraticExtension g) : IsIteratedQuadraticExtension (f ⊔ g)

theorem IsIteratedQuadraticExtension.finsetSup {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {ι : Type u_4} (s : Finset ι) (f : ι → IntermediateField K L) (h : ∀ i ∈ s, IsIteratedQuadraticExtension (f i)) : IsIteratedQuadraticExtension (s.sup f)

def constructibleClosure (K : Type u_1) (L : Type u_3) [Field K] [Field L] [Algebra K L] : IntermediateField K L

Equations

• constructibleClosure K L = ⨆ (f : IntermediateField K L), ⨆ (_ : IsIteratedQuadraticExtension f), f

theorem mem_constructibleClosure {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} : x ∈ constructibleClosure K L ↔ ∃ (f : IntermediateField K L), IsIteratedQuadraticExtension f ∧ x ∈ f

theorem isPowerOfTwo_natDegree_minpoly_of_mem_constructibleClosure {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (hx : x ∈ constructibleClosure K L) : (minpoly K x).natDegree.isPowerOfTwo

theorem isPowerOfTwo_finrank_adjoin_of_mem_constructibleClosure {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (hx : x ∈ constructibleClosure K L) : (Module.finrank K ↥K⟮x⟯).isPowerOfTwo

theorem mem_constructibleClosure_iff_isPowerOfTwo_finrank_adjoin {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (hx : IsGalois K ↥K⟮x⟯) : x ∈ constructibleClosure K L ↔ (Module.finrank K ↥K⟮x⟯).isPowerOfTwo

theorem algebraMap_mem_constructibleClosure {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] (x : K) : (algebraMap K L) x ∈ constructibleClosure K L

theorem mem_constructibleClosure_of_mem_subfield {L : Type u_3} [Field L] {x : L} {K : Subfield L} (h : x ∈ K) : x ∈ constructibleClosure (↥K) L

theorem mem_constructibleClosure_of_sq_mem {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] {x : L} (hx : x ^ 2 ∈ constructibleClosure K L) : x ∈ constructibleClosure K L

theorem constructibleClosure_induction {K : Type u_1} {L : Type u_3} [Field K] [Field L] [Algebra K L] (h0 : 2 ≠ 0) (P : L → Prop) (bot : ∀ (x : K), P ((algebraMap K L) x)) (add : ∀ (x y : L), P x → P y → P (x + y)) (inv : ∀ (x : L), P x → P x⁻¹) (mul : ∀ (x y : L), P x → P y → P (x * y)) (sqrt : ∀ (x : L), P (x ^ 2) → P x) (x : L) : x ∈ constructibleClosure K L → P x

theorem constructibleClosure_closure_induction {L : Type u_3} [Field L] (h0 : 2 ≠ 0) {s : Set L} {P : L → Prop} (mem : ∀ x ∈ s, P x) (one : P 1) (add : ∀ (x y : L), P x → P y → P (x + y)) (neg : ∀ (x : L), P x → P (-x)) (inv : ∀ (x : L), P x → P x⁻¹) (mul : ∀ (x y : L), P x → P y → P (x * y)) (sqrt : ∀ (x : L), P (x ^ 2) → P x) (x : L) : x ∈ constructibleClosure (↥(Subfield.closure s)) L → P x

theorem Complex.sq_eq_iff {a b : ℂ} : a ^ 2 = b ↔ a = b.sqrt ∨ a = -b.sqrt

theorem Complex.sqrt_eq_real_add_ite' {a : ℂ} : a.sqrt = ↑√((‖a‖ + a.re) / 2) + ↑((if 0 ≤ a.im then 1 else -1) * √((‖a‖ - a.re) / 2)) * I

theorem Complex.re_sq_of_sq_eq {a b : ℂ} (h : a ^ 2 = b) : a.re ^ 2 = (‖b‖ + b.re) / 2

theorem Complex.im_sq_of_sq_eq {a b : ℂ} (h : a ^ 2 = b) : a.im ^ 2 = (‖b‖ - b.re) / 2

theorem re_im_subset_constructibleClosure {s : Set ℂ} {x : ℂ} (h : x ∈ constructibleClosure ↥(Subfield.closure s) ℂ) : x.re ∈ constructibleClosure ↥(Subfield.closure (Complex.re '' s ∪ Complex.im '' s)) ℝ ∧ x.im ∈ constructibleClosure ↥(Subfield.closure (Complex.re '' s ∪ Complex.im '' s)) ℝ

theorem re_mem_constructibleClosure {s : Set ℂ} {x : ℂ} (h : x ∈ constructibleClosure ↥(Subfield.closure s) ℂ) : x.re ∈ constructibleClosure ↥(Subfield.closure (Complex.re '' s ∪ Complex.im '' s)) ℝ

theorem im_mem_constructibleClosure {s : Set ℂ} {x : ℂ} (h : x ∈ constructibleClosure ↥(Subfield.closure s) ℂ) : x.im ∈ constructibleClosure ↥(Subfield.closure (Complex.re '' s ∪ Complex.im '' s)) ℝ

theorem norm_mem_constructibleClosure {s : Set ℂ} {x : ℂ} (h : x ∈ constructibleClosure ↥(Subfield.closure s) ℂ) : ‖x‖ ∈ constructibleClosure ↥(Subfield.closure (Complex.re '' s ∪ Complex.im '' s)) ℝ

theorem mem_constructibleClosure_of_real {s : Set ℂ} (h : ∀ x ∈ s, (starRingEnd ℂ) x ∈ s) {x : ℝ} (hx : x ∈ constructibleClosure ↥(Subfield.closure (Complex.re '' s ∪ Complex.im '' s)) ℝ) : ↑x ∈ constructibleClosure ↥(Subfield.closure s) ℂ

theorem mem_constructibleClosure_complex_iff {s : Set ℂ} (h : ∀ x ∈ s, (starRingEnd ℂ) x ∈ s) {x : ℂ} : x ∈ constructibleClosure ↥(Subfield.closure s) ℂ ↔ x.re ∈ constructibleClosure ↥(Subfield.closure (Complex.re '' s ∪ Complex.im '' s)) ℝ ∧ x.im ∈ constructibleClosure ↥(Subfield.closure (Complex.re '' s ∪ Complex.im '' s)) ℝ

theorem IsIteratedQuadraticExtension.transfer {K : Type u_1} {K' : Type u_2} {L : Type u_3} [Field K] [Field K'] [Field L] [Algebra K L] [Algebra K' L] (hK : (algebraMap K L).fieldRange = (algebraMap K' L).fieldRange) {f : IntermediateField K L} {f' : IntermediateField K' L} (h : IsIteratedQuadraticExtension f) (hf : f.toSubfield = f'.toSubfield) : IsIteratedQuadraticExtension f'

theorem IsIteratedQuadraticExtension.transfer_iff {K : Type u_1} {K' : Type u_2} {L : Type u_3} [Field K] [Field K'] [Field L] [Algebra K L] [Algebra K' L] (hK : (algebraMap K L).fieldRange = (algebraMap K' L).fieldRange) {f : IntermediateField K L} {f' : IntermediateField K' L} (hf : f.toSubfield = f'.toSubfield) : IsIteratedQuadraticExtension f ↔ IsIteratedQuadraticExtension f'

theorem constructibleClosure_transfer {K : Type u_1} {K' : Type u_2} {L : Type u_3} [Field K] [Field K'] [Field L] [Algebra K L] [Algebra K' L] (hK : (algebraMap K L).fieldRange = (algebraMap K' L).fieldRange) {x : L} (h : x ∈ constructibleClosure K L) : x ∈ constructibleClosure K' L

theorem constructibleClosure_transfer_iff {K : Type u_1} {K' : Type u_2} {L : Type u_3} [Field K] [Field K'] [Field L] [Algebra K L] [Algebra K' L] (hK : (algebraMap K L).fieldRange = (algebraMap K' L).fieldRange) {x : L} : x ∈ constructibleClosure K L ↔ x ∈ constructibleClosure K' L

theorem constructibleClosure_transfer_ℚ_01 {L : Type u_3} [Field L] [CharZero L] {x : L} : x ∈ constructibleClosure ℚ L ↔ x ∈ constructibleClosure (↥(Subfield.closure {0, 1})) L

theorem re_im_image_01 : Complex.re '' {0, 1} ∪ Complex.im '' {0, 1} = {0, 1}

theorem mem_constructibleClosure_complex_ℚ_iff {x : ℂ} : x ∈ constructibleClosure ℚ ℂ ↔ x.re ∈ constructibleClosure ℚ ℝ ∧ x.im ∈ constructibleClosure ℚ ℝ