Field construction

Stream: new members

[Nick_adfor]

Theorem:
There exists a field that is not algebraically closed but has the property that every polynomial of degree less than or equal to n has a root.

[Nick_adfor]

The math proof is as follows. But I wonder how to formalise it.
There exists a field that is not algebraically closed but has the property that every polynomial of degree less than or equal to $n$ has a root.
Verification of the Construction Satisfying the Theorem Requirements
The theorem requires constructing a field $F$ that satisfies the following two conditions:
a. $F$ is not algebraically closed.
b. Every polynomial $f(x) \in F[x]$ with $1 \leq \deg(f) \leq n$ has a root in $F$. Given a base field $k = \mathbb{Q}$ (or any other non-algebraically closed field), we construct $F$ as the $n$-closure of $k$:
Let $k_0 = k$.
For $m \geq 0$, define $k_{m+1}$ as the field obtained by adjoining all roots (in the algebraic closure $\bar{k}$) of polynomials $g(x) \in k_m[x]$ with $1 \leq \deg(g) \leq n$ to $k_m$.
Take $F = \bigcup_{m=0}^\infty k_m$ (the union is taken in $\bar{k}$). Below we verify that this construction satisfies the theorem requirements.

1. Verification that every polynomial $f(x) \in F[x]$ with $1 \leq \deg(f) \leq n$ has a root in $F$
   Let $f(x) \in F[x]$ with $1 \leq \deg(f) \leq n$. Since $F = \bigcup_{m=0}^\infty k_m$ and the coefficients of $f(x)$ are finite, there exists an integer $m \geq 0$ such that all coefficients belong to $k_m$, i.e., $f(x) \in k_m[x]$. By the construction of $k_{m+1}$, all roots of polynomials in $k_m[x]$ with degrees between 1 and $n$ are adjoined to $k_m$ to form $k_{m+1}$. Therefore, $f(x)$ has a root in $k_{m+1} \subseteq F$.

2. Verification that $F$ is not algebraically closed
   We need to show that there exists a polynomial in $F[x]$ that has no root in $F$. Consider a prime number $p > n$ and the polynomial $h(x) = x^p - 2 \in \mathbb{Q}[x] \subseteq F[x]$. Assume for contradiction that $h(x)$ has a root $\alpha$ in $F$. Then $\alpha \in k_m$ for some $m \geq 0$. Let $\mu(x) \in k_{m-1}[x]$ be the minimal polynomial of $\alpha$ over $k_{m-1}$. Since $\alpha$ is a root of $h(x)$, $\mu(x)$ divides $h(x)$ in $k_{m-1}[x]$, so $\deg(\mu) \leq \deg(h) = p$. On the other hand, the minimal polynomial of $\alpha$ over $\mathbb{Q}$ is $x^p - 2$, which has degree $p$. Since $k_{m-1} \supseteq \mathbb{Q}$, we have $[k_{m-1}(\alpha):k_{m-1}]$ divides $[\mathbb{Q}(\alpha):\mathbb{Q}] = p$ (because $p$ is prime and the characteristic is 0). Thus $[k_{m-1}(\alpha):k_{m-1}] = 1$ or $p$:
   If it is 1, then $\alpha \in k_{m-1}$, contradicting $\alpha \notin k_{m-1}$.
   If it is $p$, then $\deg(\mu) = p > n$ (since $p > n$), contradicting $\deg(\mu) \leq n$. Thus, our assumption is false, and $h(x)$ has no root in $F$. Therefore, $F$ is not algebraically closed.
   Conclusion
   This construction satisfies the theorem requirements:
   $F$ is not algebraically closed (as shown by the polynomial $x^p - 2$ having no root).
   Every polynomial $f(x) \in F[x]$ with $1 \leq \deg(f) \leq n$ has a root in $F$.

[Nick_adfor]

Now I begin this way.

import Mathlib

variable {k K : Type*} [Field k] [Field K] [Algebra k K] [IsAlgClosed K]
variable (n : ℕ)
variable (F : IntermediateField k K)

open Polynomial

def roots_of_deg_le_n (F : IntermediateField k K) : Set K :=
  { α | ∃ (f : Polynomial k), 1 ≤ f.natDegree ∧ f.natDegree ≤ n ∧
    eval₂ (algebraMap k K) α f = 0 }

def next_subfield (F : IntermediateField k K) : IntermediateField k K :=
  IntermediateField.adjoin k (roots_of_deg_le_n n F)

def chain (n : ℕ) (F : IntermediateField k K) : ℕ → IntermediateField k K
| 0 => F
| (m+1) => next_subfield n (chain n F m)

variable {n}

lemma chain_mono (n : ℕ) (F : IntermediateField k K) {i j : ℕ} (h : i ≤ j) :
  (chain n F i) ≤ (chain n F j) := by
  induction h with
  | refl =>
    rfl
  | @step m hm ih =>
    trans chain n F m
    · exact ih
    · suffices chain n F m ≤ next_subfield n (chain n F m) by
        simp [chain, this]
      intro x hx
      sorry

lemma exists_m_covering_coeffs {n : ℕ} {F : IntermediateField k K} {f : Polynomial F} (hf_nonzero : f ≠ 0) :
  ∃ m, ∀ i ∈ f.support, (f.coeff i : K) ∈ (chain n F m : Set K) := by
  sorry

theorem small_polynomial_has_root {f : Polynomial F} (hdeg1 : 1 ≤ f.natDegree) (hdegn : f.natDegree ≤ n) :
  ∃ α : F, eval₂ (algebraMap F K) (α : K) f = 0 :=
by
  sorry

variable (k : Type*) [Field k] [Algebra ℚ k] [IsAlgClosed K]

theorem F_not_alg_closed [hk : Nontrivial k] (hkQ : Nonempty (k ≃ₐ[ℚ] ℚ)) :
  ¬ (∀ g : Polynomial F, ∃ α : F, Polynomial.eval₂ (algebraMap F K) (α : K) g = 0) :=
by
  sorry

[Kenny Lau]

@Nick_adfor use the direct limit

[Nick_adfor]

Kenny Lau said:

Nick_adfor use the direct limit

What is the direct limit?

[Kenny Lau]

it's like the union but you don't have the bigger set yet

[Kenny Lau]

consider Fin n = {0, 1, 2, ..., n-1}, where each Fin n embeds to the next Fin (n+1)

[Kenny Lau]

then their "union" (along these embeddings) would be Nat

[Nick_adfor]

(deleted)

[Nick_adfor]

Kenny Lau said:

it's like the union but you don't have the bigger set yet

It means that my original informal proof might have a typo? : (

[Kenny Lau]

what typo

[Kenny Lau]

i was just suggesting that you can use the direct limit to construct the "union"

[Nick_adfor]

In my formal proof I use IntermediateField as I find it quickly in Mathlib. What about direct sum? I'm not so familiar with it.

[Kenny Lau]

do you know what these mathematical objects are? lean is not magic, you should know the maths first

[Nick_adfor]

If F is algebraically closed, then the chain F₀ ⊆ F₁ ⊆ ... ⊆ Fₙ ⊆ ... should stabilize (i.e., Fᵢ₊₁ = Fᵢ for all sufficiently large i), because all roots of polynomials are already in F.

[Kenny Lau]

ah, i misread, if you're using algebraic closure then there's no need to use direct limit, please disregard all of my previous comments

[Kenny Lau]

so, what's the question?

[Nick_adfor]

algebraic closure and direct limit seem to be both used

[Kenny Lau]

you don't need the direct limit here

[Nick_adfor]

If I meet other trouble when filling sorry I may try direct limit.

[Nick_adfor]

Algebraic closure and direct limits are complementary that can indeed be used together. The direct limit construction allows us to build increasingly larger fields by systematically adjoining roots, while algebraic closure represents the “endpoint” of this process - a field containing all possible roots of polynomials.

[Nick_adfor]

Kenny Lau said:

so, what's the question?

Right now there's only a broad framework with sorry, while the specific details have yet to be filled in.

[Nick_adfor]

Just stuck on chain_mono

[Kenny Lau]

it would be easier for people to answer your question if they are precise and minimised

[Nick_adfor]

The first is to check if the proof framework has typo and other ways. Fortunately you have given me one direct limit.

The second is to fill in the sorry one by one.

[Nick_adfor]

I wonder this sorry.

import Mathlib

variable {k K : Type*} [Field k] [Field K] [Algebra k K] [IsAlgClosed K]
variable (n : ℕ)
variable (F : IntermediateField k K)

open Polynomial

def roots_of_deg_le_n (F : IntermediateField k K) : Set K :=
  { α | ∃ (f : Polynomial k), 1 ≤ f.natDegree ∧ f.natDegree ≤ n ∧
    eval₂ (algebraMap k K) α f = 0 }

def next_subfield (F : IntermediateField k K) : IntermediateField k K :=
  IntermediateField.adjoin k (roots_of_deg_le_n n F)

def chain (n : ℕ) (F : IntermediateField k K) : ℕ → IntermediateField k K
| 0 => F
| (m+1) => next_subfield n (chain n F m)

variable {n}

lemma chain_mono (n : ℕ) (F : IntermediateField k K) {i j : ℕ} (h : i ≤ j) :
  (chain n F i) ≤ (chain n F j) := by
  induction h with
  | refl =>
    rfl
  | @step m hm ih =>
    trans chain n F m
    · exact ih
    · suffices chain n F m ≤ next_subfield n (chain n F m) by
        simp [chain, this]
      intro x hx
      sorry

[Kenny Lau]

@Nick_adfor subset_adjoin

[Nick_adfor]

Kenny Lau said:

Nick_adfor subset_adjoin

No. As the origin definition of next_subfield is wrong.

[Nick_adfor]

I fix it like this.

def next_subfield (F : IntermediateField k K) : IntermediateField k K :=
  IntermediateField.adjoin k ((F : Set K) ∪ roots_of_deg_le_n n F)

[Nick_adfor]

import Mathlib

variable {k K : Type*} [Field k] [Field K] [Algebra k K] [IsAlgClosed K]
variable (n : ℕ)
variable (F : IntermediateField k K)

open Polynomial

def roots_of_deg_le_n (F : IntermediateField k K) : Set K :=
  { α | ∃ (f : Polynomial k), 1 ≤ f.natDegree ∧ f.natDegree ≤ n ∧
    eval₂ (algebraMap k K) α f = 0 }

def next_subfield (F : IntermediateField k K) : IntermediateField k K :=
  IntermediateField.adjoin k ((F : Set K) ∪ roots_of_deg_le_n n F)

def chain (n : ℕ) (F : IntermediateField k K) : ℕ → IntermediateField k K
| 0 => F
| (m+1) => next_subfield n (chain n F m)

variable {n}

lemma chain_mono (n : ℕ) (F : IntermediateField k K) {i j : ℕ} (h : i ≤ j) :
  (chain n F i) ≤ (chain n F j) := by
  induction h with
  | refl =>
    rfl
  | @step m hm ih =>
    trans chain n F m
    · exact ih
    · show chain n F m ≤ next_subfield n (chain n F m)
      intro x hx
      exact IntermediateField.subset_adjoin k _ (Or.inl hx)

lemma exists_m_covering_coeffs {n : ℕ} {F : IntermediateField k K} {f : Polynomial F} (hf_nonzero : f ≠ 0) :
  ∃ m, ∀ i ∈ f.support, (f.coeff i : K) ∈ (chain n F m : Set K) := by
  sorry

theorem small_polynomial_has_root {f : Polynomial F} (hdeg1 : 1 ≤ f.natDegree) (hdegn : f.natDegree ≤ n) :
  ∃ α : F, eval₂ (algebraMap F K) (α : K) f = 0 :=
by
  sorry

variable (k : Type*) [Field k] [Algebra ℚ k] [IsAlgClosed K]

theorem F_not_alg_closed [hk : Nontrivial k] (hkQ : Nonempty (k ≃ₐ[ℚ] ℚ)) :
  ¬ (∀ g : Polynomial F, ∃ α : F, Polynomial.eval₂ (algebraMap F K) (α : K) g = 0) :=
by
  sorry

[Wuyang]

Refining next_subfield with the union fixes the monotonicity issue nicely.
You might also try searching LeanFinder (www.leanfinder.org) for similar IntermediateField and chain constructions.

[Wuyang]

@leanfinder Lean formalization of fields where all polynomials of bounded degree have roots but field is not algebraically closed

[leanfinder]

Here’s what I found:

• theorem IsAlgClosed.of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → ∃ x, p.eval x = 0) : IsAlgClosed k := by refine ⟨fun p ↦ Or.inr ?_⟩ intro q hq _ have : Irreducible (q * C (leadingCoeff q)⁻¹) := by classical rw [← coe_normUnit_of_ne_zero hq.ne_zero] exact (associated_normalize _).irreducible hq obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) this exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx "Let $k$ be a field. If every monic irreducible polynomial $p \in k[X]$ has a root in $k$, then $k$ is algebraically closed." (score: 0.705)

• theorem IsAlgClosed.exists_root [IsAlgClosed k] (p : k[X]) (hp : p.degree ≠ 0) : ∃ x, IsRoot p x := exists_root_of_splits _ (IsAlgClosed.splits p) hp "Let $k$ be an algebraically closed field. For any non-constant polynomial $p \in k[X]$ (i.e., with $\deg(p) \neq 0$), there exists an element $x \in k$ such that $p(x) = 0$." (score: 0.699)

• structure IsAlgClosed : Prop None "A field $k$ is called algebraically closed if every non-constant polynomial with coefficients in $k$ has a root in $k$. Equivalently, every such polynomial splits into linear factors over $k$." (score: 0.690)

• theorem IsAlgClosed.exists_aeval_eq_zero {R : Type*} [Field R] [IsAlgClosed k] [Algebra R k] (p : R[X]) (hp : p.degree ≠ 0) : ∃ x : k, aeval x p = 0 := exists_eval₂_eq_zero (algebraMap R k) p hp "Let $R$ be a field and $k$ an algebraically closed field with an $R$-algebra structure. For any non-constant polynomial $p \in R[X]$, there exists an element $x \in k$ such that the evaluation of $p$ at $x$ (via the $R$-algebra structure) equals zero, i.e., $\text{aeval}_x(p) = 0$." (score: 0.689)

• theorem IsAlgClosure.of_exist_roots (h : ∀ p : F[X], p.Monic → Irreducible p → ∃ x : E, aeval x p = 0) : IsAlgClosure F E := .of_splits fun p _ _ ↦ have ⟨σ⟩ := nonempty_algHom_of_exist_roots fun x : p.SplittingField ↦ have := Algebra.IsAlgebraic.isIntegral (K := F).1 x h _ (minpoly.monic this) (minpoly.irreducible this) splits_of_algHom (SplittingField.splits _) σ "Let $E/F$ be an algebraic field extension. If every monic irreducible polynomial $p \in F[X]$ has a root in $E$, then $E$ is an algebraic closure of $F$." (score: 0.689)

• instance IsAlgClosed.instInfinite {K : Type*} [Field K] [IsAlgClosed K] : Infinite K := by apply Infinite.of_not_fintype intro hfin set n := Fintype.card K set f := (X : K[X]) ^ (n + 1) - 1 have hfsep : Separable f := separable_X_pow_sub_C 1 (by simp [n]) one_ne_zero apply Nat.not_succ_le_self (Fintype.card K) have hroot : n.succ = Fintype.card (f.rootSet K) := by erw [card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _), natDegree_X_pow_sub_C] rw [hroot] exact Fintype.card_le_of_injective _ Subtype.coe_injective "Every algebraically closed field $K$ is infinite." (score: 0.684)

• theorem exists_root {f : ℂ[X]} (hf : 0 < degree f) : ∃ z : ℂ, IsRoot f z := by by_contra! hf' /- Since f has no roots, f⁻¹ is differentiable. And since f is a polynomial, it tends to
  infinity at infinity, thus f⁻¹ tends to zero at infinity. By Liouville's theorem, f⁻¹ = 0. -/
  have (z : ℂ) : (f.eval z)⁻¹ = 0 :=
  (f.differentiable.inv hf').apply_eq_of_tendsto_cocompact z <|
  Metric.cobounded_eq_cocompact (α := ℂ) ▸ (Filter.tendsto_inv₀_cobounded.comp <| by
  simpa only [tendsto_norm_atTop_iff_cobounded]
  using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop)
  -- Thus f = 0, contradicting the fact that 0 < degree f. obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this] simp at hf "For any nonconstant polynomial $f$ with complex coefficients (i.e., $f \in \mathbb{C}[X]$ and $\deg(f) > 0$), there exists a complex number $z \in \mathbb{C}$ such that $f(z) = 0$. This means that every nonconstant complex polynomial has at least one root in the complex numbers." (score: 0.684)

• theorem instIsAlgClosed : IsAlgClosed (AlgebraicClosureAux k) := IsAlgClosed.of_exists_root _ fun _ => exists_root k "The auxiliary algebraic closure of a field $k$, denoted as $\text{AlgebraicClosureAux}(k)$, is algebraically closed. This means that every non-constant polynomial with coefficients in $\text{AlgebraicClosureAux}(k)$ has a root in $\text{AlgebraicClosureAux}(k)$. The proof constructs this closure by ensuring the existence of roots for irreducible monic polynomials." (score: 0.683)

• theorem Complex.exists_root {f : ℂ[X]} (hf : 0 < degree f) : ∃ z : ℂ, IsRoot f z := by by_contra! hf' /- Since f has no roots, f⁻¹ is differentiable. And since f is a polynomial, it tends to
  infinity at infinity, thus f⁻¹ tends to zero at infinity. By Liouville's theorem, f⁻¹ = 0. -/
  have (z : ℂ) : (f.eval z)⁻¹ = 0 :=
  (f.differentiable.inv hf').apply_eq_of_tendsto_cocompact z <|
  Metric.cobounded_eq_cocompact (α := ℂ) ▸ (Filter.tendsto_inv₀_cobounded.comp <| by
  simpa only [tendsto_norm_atTop_iff_cobounded]
  using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop)
  -- Thus f = 0, contradicting the fact that 0 < degree f. obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this] simp at hf "For any nonconstant complex polynomial $f \in \mathbb{C}[X]$ (i.e., with $\deg(f) > 0$), there exists a complex number $z \in \mathbb{C}$ such that $f(z) = 0$." (score: 0.680)

• theorem IsAlgClosed.roots_eq_zero_iff [IsAlgClosed k] {p : k[X]} : p.roots = 0 ↔ p = Polynomial.C (p.coeff 0) := by refine ⟨fun h => ?_, fun hp => by rw [hp, roots_C]⟩ rcases le_or_lt (degree p) 0 with hd | hd · exact eq_C_of_degree_le_zero hd · obtain ⟨z, hz⟩ := IsAlgClosed.exists_root p hd.ne' rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz simp at hz "Let $k$ be an algebraically closed field. For any polynomial $p \in k[X]$, the multiset of roots of $p$ is empty if and only if $p$ is a constant polynomial (i.e., $p$ equals the constant polynomial $\text{C}(p(0))$ where $p(0)$ is the constant term of $p$)." (score: 0.679)

[Aaron Liu]

Nick_adfor said:

Since xᵖ - 2 is irreducible over ℚ (by Eisenstein's criterion with prime 2), it is also irreducible over kₘ₋₁ (as kₘ₋₁ contains ℚ and the characteristic is 0).

Can you explain this part? I don't understand.

[Kenny Lau]

hmm, interesting find

[Nick_adfor]

Here I leave two sorry in small_polynomial_has_root. Now wonder how to fix this.

import Mathlib

variable {k K : Type*} [Field k] [Field K] [Algebra k K]
variable (n : ℕ)
variable (F : IntermediateField k K)

open Polynomial

def roots_of_deg_le_n (F : IntermediateField k K) : Set K :=
  { α | ∃ (f : Polynomial F), 1 ≤ f.natDegree ∧ f.natDegree ≤ n ∧
    eval₂ (algebraMap F K) α f = 0 }

def next_subfield (F : IntermediateField k K) : IntermediateField k K :=
  IntermediateField.adjoin k ((F : Set K) ∪ roots_of_deg_le_n n F)

def chain (n : ℕ) (F : IntermediateField k K) : ℕ → IntermediateField k K
| 0 => F
| (m+1) => next_subfield n (chain n F m)

variable {n}

lemma chain_mono (n : ℕ) (F : IntermediateField k K) {i j : ℕ} (h : i ≤ j) :
  (chain n F i) ≤ (chain n F j) := by
  induction h with
  | refl =>
    rfl
  | @step m hm ih =>
    trans chain n F m
    · exact ih
    · show chain n F m ≤ next_subfield n (chain n F m)
      intro x hx
      exact IntermediateField.subset_adjoin k _ (Or.inl hx)

variable [DecidableEq K]

theorem small_polynomial_has_root {f : Polynomial F} (hdeg1 : 1 ≤ f.natDegree) (hdegn : f.natDegree ≤ n) :
  ∃ (m : ℕ) (α : chain n F m), eval₂ (algebraMap _ K) α f = 0 := by
  by_cases hf_zero : f = 0
  · exfalso; rw [hf_zero, natDegree_zero] at hdeg1; linarith
  have exists_m_covering_coeffs {n : ℕ} {F : IntermediateField k K} {f : Polynomial F} (hf_nonzero : f ≠ 0) :
  ∃ m, ∀ i ∈ f.support, (f.coeff i : K) ∈ (chain n F m : Set K) := by
    use 0
    intro i hi
    exact (f.coeff i).2
  obtain ⟨m, hm⟩ := exists_m_covering_coeffs hf_zero
  let f' : Polynomial (chain n F m) :=
    Polynomial.ofFinsupp {
      support := f.support,
      toFun := fun i =>
        if hi : i ∈ f.support then
          ⟨f.coeff i, hm i hi⟩
        else
          0,
      mem_support_toFun := fun i => by
        by_cases hi : i ∈ f.support
        · simp only [hi, ↓reduceDIte, ne_eq, true_iff, ZeroMemClass.zero_def, Subtype.mk.injEq, ZeroMemClass.coe_eq_zero]
          exact mem_support_iff.mp hi
        · simp only [hi, ↓reduceDIte, ZeroMemClass.zero_def, ne_eq]
          exact Iff.symm not_true
    }
  let E : IntermediateField k K := chain n F m
  let φ : ↥E →+* K := {
    toFun := fun x => (x : K),
    map_zero' := by simp only [ZeroMemClass.coe_zero],
    map_add'  := by intros; simp only [AddMemClass.coe_add],
    map_one'  := by simp only [OneMemClass.coe_one],
    map_mul'  := by intros; simp only [MulMemClass.coe_mul]
  }
  let f'_mapped : Polynomial K := f'.map φ
  have h_root : ∃ α : next_subfield n E, eval₂ (algebraMap _ K) α f'_mapped = 0 := by
    sorry
  obtain ⟨α, hα⟩ := h_root
  use m+1, α
  have f'_eq : f'_mapped = f.map (algebraMap F K) := by
    ext i
    simp [f'_mapped, f', φ, Polynomial.coeff_map]
    sorry
  rw [f'_eq] at hα
  have alg_map_id : algebraMap K K = RingHom.id K := rfl
  rw [alg_map_id] at hα
  have eval_relation : eval₂ (algebraMap F K) (α : K) f = 0 := by
    rw [← hα, Polynomial.eval₂_map, RingHom.id_comp]
  rw [eval_relation]

variable (k : Type*) [Field k] [Algebra ℚ k] [IsAlgClosed K]

theorem F_not_alg_closed [hk : Nontrivial k] (hkQ : Nonempty (k ≃ₐ[ℚ] ℚ)) :
  ¬ (∀ g : Polynomial F, ∃ α : F, Polynomial.eval₂ (algebraMap F K) (α : K) g = 0) :=
by
  sorry

[Nick_adfor]

Aaron Liu said:

Can you explain this part? I don't understand.

Can you explain your misunderstanding? I don’t understand your not understanding.

[Damiano Testa]

Somewhere, your argument should use the fact that ℚ is not real closed. In particular, if you had started your construction with ℝ and added all missing roots of degree 2 polynomials, then it would be hard to find a polynomial without a root in the extension.

[Nick_adfor]

Damiano Testa said:

In particular, if you had started your construction with ℝ.

But I do not use ℝ

[Yaël Dillies]

Damiano Testa said:

Somewhere, your argument should use the fact that ℚ is not real closed.

Is the "where" not exactly the application of Eisenstein's criterion?

[Damiano Testa]

That's the "where" on ℚ, but then there is no (correct) argument for why this still applies further up in the sequence.

[Nick_adfor]

Now I write like this. There seems to be nothing wrong with "where" and Eisenstein.

import Mathlib

variable {k K : Type*} [Field k] [Field K] [Algebra k K]
variable (n : ℕ)
variable (F : IntermediateField k K)

open Polynomial

def roots_of_deg_le_n (F : IntermediateField k K) : Set K :=
  { α | ∃ (f : Polynomial F), 1 ≤ f.natDegree ∧ f.natDegree ≤ n ∧
    eval₂ (algebraMap F K) α f = 0 }

def next_subfield (F : IntermediateField k K) : IntermediateField k K :=
  IntermediateField.adjoin k ((F : Set K) ∪ roots_of_deg_le_n n F)

def chain (n : ℕ) (F : IntermediateField k K) : ℕ → IntermediateField k K
| 0 => F
| (m+1) => next_subfield n (chain n F m)

variable {n}

lemma chain_mono (n : ℕ) (F : IntermediateField k K) {i j : ℕ} (h : i ≤ j) :
  (chain n F i) ≤ (chain n F j) := by
  induction h with
  | refl =>
    rfl
  | @step m hm ih =>
    trans chain n F m
    · exact ih
    · show chain n F m ≤ next_subfield n (chain n F m)
      intro x hx
      exact IntermediateField.subset_adjoin k _ (Or.inl hx)

variable [DecidableEq K] [IsAlgClosed K]

theorem small_polynomial_has_root {f : Polynomial F} (hdeg1 : 1 ≤ f.natDegree) (hdegn : f.natDegree ≤ n) :
  ∃ (m : ℕ) (α : chain n F m), eval₂ (algebraMap _ K) α f = 0 := by
  by_cases hf_zero : f = 0
  · exfalso; rw [hf_zero, natDegree_zero] at hdeg1; linarith
  have exists_m_covering_coeffs {n : ℕ} {F : IntermediateField k K} {f : Polynomial F} (hf_nonzero : f ≠ 0) :
  ∃ m, ∀ i ∈ f.support, (f.coeff i : K) ∈ (chain n F m : Set K) := by
    use 0
    intro i hi
    exact (f.coeff i).2
  obtain ⟨m, hm⟩ := exists_m_covering_coeffs hf_zero
  let f' : Polynomial (chain n F m) :=
    Polynomial.ofFinsupp {
      support := f.support,
      toFun := fun i =>
        if hi : i ∈ f.support then
          ⟨f.coeff i, hm i hi⟩
        else
          0,
      mem_support_toFun := fun i => by
        by_cases hi : i ∈ f.support
        · simp only [hi, ↓reduceDIte, ne_eq, true_iff, ZeroMemClass.zero_def, Subtype.mk.injEq, ZeroMemClass.coe_eq_zero]
          exact mem_support_iff.mp hi
        · simp only [hi, ↓reduceDIte, ZeroMemClass.zero_def, ne_eq]
          exact Iff.symm not_true
    }
  let E : IntermediateField k K := chain n F m
  let φ : ↥E →+* K := {
    toFun := fun x => (x : K),
    map_zero' := by simp only [ZeroMemClass.coe_zero],
    map_add'  := by intros; simp only [AddMemClass.coe_add],
    map_one'  := by simp only [OneMemClass.coe_one],
    map_mul'  := by intros; simp only [MulMemClass.coe_mul]
  }
  let f'_mapped : Polynomial K := f'.map φ
  have h_root : ∃ α : next_subfield n E, eval₂ (algebraMap _ K) α f'_mapped = 0 := by
      have h_natDeg_f' : 1 ≤ (f' : Polynomial (chain n F m)).natDegree := by
        have : (f' : Polynomial (chain n F m)).support = f.support := by
          rfl
        have hf_ne : f ≠ 0 := by
          intro H; rw [H, natDegree_zero] at hdeg1; linarith
        have : (f' : Polynomial (chain n F m)).natDegree = f.natDegree := by
          exact rfl
        exact this ▸ hdeg1
      have hf'_nonzero : (f' : Polynomial (chain n F m)) ≠ 0 := by
        intro H; rw [H, natDegree_zero] at h_natDeg_f'; linarith
      have : ∃ (x : K), eval₂ (algebraMap (chain n F m) K) x (f' : Polynomial (chain n F m)) = 0 := by
        have hd : (f' : Polynomial (chain n F m)).degree ≠ 0 := by
          have : 1 ≤ (f' : Polynomial (chain n F m)).natDegree := h_natDeg_f'
          intro Hdeg0
          have : (f' : Polynomial (chain n F m)).natDegree = 0 := by
            exact (degree_eq_iff_natDegree_eq hf'_nonzero).mp Hdeg0
          linarith
        have α_in : ∃ α : K, α ∈ roots_of_deg_le_n n (chain n F m) ∧
          eval₂ (algebraMap (chain n F m) K) α f' = 0 := by
            have hd_mapped : f'_mapped.degree ≠ 0 := by
              have hf'_nonzero : f' ≠ 0 := by exact hf'_nonzero
              have h_map_inj : Function.Injective φ.toFun := by exact Subtype.val_injective
              have hd_mapped : f'_mapped.degree = (f' : Polynomial (chain n F m)).degree := by
                rw [degree_map]
              intro hdeg
              rw [hdeg] at hd_mapped
              exact hd (id (Eq.symm hd_mapped))
            obtain ⟨α, hα⟩ := IsAlgClosed.exists_root f'_mapped hd_mapped
            use α
            constructor
            · use f'
              constructor
              · exact hdeg1
              constructor
              · exact hdegn
              · have eval_eq : eval₂ (algebraMap (chain n F m) K) α f' = Polynomial.eval α f'_mapped := by
                  exact eval₂_eq_eval_map (algebraMap (↥(chain n F m)) K)
                rw [eval_eq]
                exact hα
            · have eval_eq : eval₂ (algebraMap (chain n F m) K) α f' = Polynomial.eval α f'_mapped := by
                  exact eval₂_eq_eval_map (algebraMap (↥(chain n F m)) K)
              rw [eval_eq]
              exact hα
        obtain ⟨α, hα_in, hα_root⟩ := α_in
        exact ⟨α, hα_root⟩
      obtain ⟨αK, hαK⟩ := this
      have αK_in_roots : αK ∈ roots_of_deg_le_n n E := by
        use (f' : Polynomial (chain n F m))
        constructor
        · have : 1 ≤ (f' : Polynomial (chain n F m)).natDegree := h_natDeg_f'
          exact this
        constructor
        · have : (f' : Polynomial (chain n F m)).natDegree = f.natDegree := by
            rfl
          calc
            (f' : Polynomial (chain n F m)).natDegree = f.natDegree := this
            _ ≤ n := hdegn
        · exact hαK
      have α_in_adjoin_set : (αK : K) ∈ ((E : Set K) ∪ roots_of_deg_le_n n E) := Or.inr αK_in_roots
      let α_sub : next_subfield n E := ⟨αK, IntermediateField.subset_adjoin k _ α_in_adjoin_set⟩
      use α_sub
      have : eval₂ (algebraMap K K) (↑α_sub) f'_mapped = 0 := by
        have h_map: f'_mapped = (f' : Polynomial (chain n F m)).map (φ : (↥E) →+* K) := rfl
        rw [h_map, Polynomial.eval₂_map]
        have : (↑α_sub : K) = αK := rfl
        rw [this]
        exact hαK
      exact this
  obtain ⟨α, hα⟩ := h_root
  use m+1, α
  have f'_eq : f'_mapped = f.map (algebraMap F K) := by
    ext i
    simp only [coeff_map, IntermediateField.algebraMap_apply]
    sorry
  rw [f'_eq] at hα
  have alg_map_id : algebraMap K K = RingHom.id K := rfl
  rw [alg_map_id] at hα
  have eval_relation : eval₂ (algebraMap F K) (α : K) f = 0 := by
    rw [← hα, Polynomial.eval₂_map, RingHom.id_comp]
  rw [eval_relation]

variable (k : Type*) [Field k] [Algebra ℚ k] [IsAlgClosed K]

theorem F_not_alg_closed [hk : Nontrivial k] (hkQ : Nonempty (k ≃ₐ[ℚ] ℚ)) :
  ¬ (∀ g : Polynomial F, ∃ α : F, Polynomial.eval₂ (algebraMap F K) (α : K) g = 0) :=
by
  sorry

[Kenny Lau]

Nick_adfor said:

Aaron Liu said:

Can you explain this part? I don't understand.

Can you explain your misunderstanding? I don’t understand your not understanding.

you seem to be confusing "irreducible" with "no roots"; I see that in your second informal proof you have stopped using the word "irreducible", but the logic is still wrong. Specifically, this part:

• But [k(α):k] = p > n, while Fᵢ only adds roots of polynomials of degree ≤ n, a contradiction.

[Nick_adfor]

Kenny Lau said:

Nick_adfor said:

Aaron Liu said:

Can you explain this part? I don't understand.

Can you explain your misunderstanding? I don’t understand your not understanding.

you seem to be confusing "irreducible" with "no roots"; I see that in your second informal proof you have stopped using the word "irreducible", but the logic is still wrong. Specifically, this part:

• But [k(α):k] = p > n, while Fᵢ only adds roots of polynomials of degree ≤ n, a contradiction.
  

Oh, I'm still working on theorem small_polynomial_has_root. I haven't come to theorem F_not_alg_closed yet.

[Aaron Liu]

Irreducible implies no roots, and having roots implies not irreducible, at least for non-linear polynomials (docs#Polynomial.degree_eq_one_of_irreducible_of_root).

[Aaron Liu]

Nick_adfor said:

Aaron Liu said:

Can you explain this part? I don't understand.

Can you explain your misunderstanding? I don’t understand your not understanding.

You conclude that xᵖ - 2 is irreducible over ℚ, but why does this mean it's also irreducible over kₘ₋₁?

[Nick_adfor]

Thank you for your reminder. I haven't mathematically verified this section rigorously because I haven't reached theorem F_not_alg_closed in lean yet. How should I revise this to make it correct? I haven't yet found a good mathematical approach. I'm still working on theorem small_polynomial_has_root in Lean code now.

[Nick_adfor]

Kenny Lau said:

Nick_adfor said:

Aaron Liu said:

Can you explain this part? I don't understand.

Can you explain your misunderstanding? I don’t understand your not understanding.

you seem to be confusing "irreducible" with "no roots"; I see that in your second informal proof you have stopped using the word "irreducible", but the logic is still wrong. Specifically, this part:

• But [k(α):k] = p > n, while Fᵢ only adds roots of polynomials of degree ≤ n, a contradiction.
  

I do not use the second informal proof. Just now I've deleted it. My formal proof is based on the first informal proof. If there's something wrong with the first informal proof, you can also point it out, it might influence the formalization in theorem F_not_alg_closed. And theorem small_polynomial_has_root still leaves some sorry. You can also point it out that if there's mathematical typo.

[Kenny Lau]

@Nick_adfor we've pointed it out many times, F irreducible over Q does not imply F irreducible over k[m-1]

[Nick_adfor]

Now finish theorem small_polynomial_has_root.

import Mathlib

variable {k K : Type*} [Field k] [Field K] [Algebra k K]
variable (n : ℕ)
variable (F : IntermediateField k K)

open Polynomial

/--
`roots_of_deg_le_n F` is the set of elements in `K` that are roots of polynomials over `F`
with degree at least `1` and at most `n`.
-/
def roots_of_deg_le_n (F : IntermediateField k K) : Set K :=
  { α | ∃ (f : Polynomial F), 1 ≤ f.natDegree ∧ f.natDegree ≤ n ∧
    eval₂ (algebraMap F K) α f = 0 }

/--
`next_subfield F` is the intermediate field obtained by adjoining to `F` all elements of
`roots_of_deg_le_n n F`.
-/
def next_subfield (F : IntermediateField k K) : IntermediateField k K :=
  IntermediateField.adjoin k ((F : Set K) ∪ roots_of_deg_le_n n F)

/--
`chain n F` is a sequence of intermediate fields starting from `F` where each next step
is obtained via `next_subfield`.
-/
def chain (n : ℕ) (F : IntermediateField k K) : ℕ → IntermediateField k K
| 0 => F
| (m+1) => next_subfield n (chain n F m)

variable {n}
variable [DecidableEq K] [IsAlgClosed K]

/--
If a polynomial `f` over `F` has degree between `1` and `n`, then there exists some
stage `m` in the chain where `f` has a root in `chain n F m`.
-/
theorem small_polynomial_has_root {f : Polynomial F} (hdeg1 : 1 ≤ f.natDegree) (hdegn : f.natDegree ≤ n) :
  ∃ (m : ℕ) (α : chain n F m), eval₂ (algebraMap _ K) α f = 0 := by
  by_cases hf_zero : f = 0
  · exfalso; rw [hf_zero, natDegree_zero] at hdeg1; linarith
  have exists_m_covering_coeffs {n : ℕ} {F : IntermediateField k K} {f : Polynomial F} (hf_nonzero : f ≠ 0) :
  ∃ m, ∀ i ∈ f.support, (f.coeff i : K) ∈ (chain n F m : Set K) := by
    use 0
    intro i hi
    exact (f.coeff i).2
  obtain ⟨m, hm⟩ := exists_m_covering_coeffs hf_zero
  let f' : Polynomial (chain n F m) :=
    Polynomial.ofFinsupp {
      support := f.support,
      toFun := fun i =>
        if hi : i ∈ f.support then
          ⟨f.coeff i, hm i hi⟩
        else
          0,
      mem_support_toFun := fun i => by
        by_cases hi : i ∈ f.support
        · simp only [hi, ↓reduceDIte, ne_eq, true_iff, ZeroMemClass.zero_def, Subtype.mk.injEq, ZeroMemClass.coe_eq_zero]
          exact mem_support_iff.mp hi
        · simp only [hi, ↓reduceDIte, ZeroMemClass.zero_def, ne_eq]
          exact Iff.symm not_true
    }
  let E : IntermediateField k K := chain n F m
  let φ : ↥E →+* K := {
    toFun := fun x => (x : K),
    map_zero' := by simp only [ZeroMemClass.coe_zero],
    map_add'  := by intros; simp only [AddMemClass.coe_add],
    map_one'  := by simp only [OneMemClass.coe_one],
    map_mul'  := by intros; simp only [MulMemClass.coe_mul]
  }
  let f'_mapped : Polynomial K := f'.map φ
  have h_root : ∃ α : next_subfield n E, eval₂ (algebraMap _ K) α f'_mapped = 0 := by
      have h_natDeg_f' : 1 ≤ (f' : Polynomial (chain n F m)).natDegree := by
        have : (f' : Polynomial (chain n F m)).natDegree = f.natDegree := by
          exact rfl
        exact this ▸ hdeg1
      have hf'_nonzero : (f' : Polynomial (chain n F m)) ≠ 0 := by
        intro H; rw [H, natDegree_zero] at h_natDeg_f'; linarith
      have : ∃ (x : K), eval₂ (algebraMap (chain n F m) K) x (f' : Polynomial (chain n F m)) = 0 := by
        have hd : (f' : Polynomial (chain n F m)).degree ≠ 0 := by
          intro Hdeg0
          have : (f' : Polynomial (chain n F m)).natDegree = 0 := by
            exact (degree_eq_iff_natDegree_eq hf'_nonzero).mp Hdeg0
          linarith
        have α_in : ∃ α : K, α ∈ roots_of_deg_le_n n (chain n F m) ∧
          eval₂ (algebraMap (chain n F m) K) α f' = 0 := by
            have hd_mapped : f'_mapped.degree ≠ 0 := by
              have hd_mapped : f'_mapped.degree = (f' : Polynomial (chain n F m)).degree := by
                rw [degree_map]
              intro hdeg
              rw [hdeg] at hd_mapped
              exact hd (id (Eq.symm hd_mapped))
            obtain ⟨α, hα⟩ := IsAlgClosed.exists_root f'_mapped hd_mapped
            use α
            constructor
            · use f'
              constructor
              · exact hdeg1
              constructor
              · exact hdegn
              · have eval_eq : eval₂ (algebraMap (chain n F m) K) α f' = Polynomial.eval α f'_mapped := by
                  exact eval₂_eq_eval_map (algebraMap (↥(chain n F m)) K)
                rw [eval_eq]
                exact hα
            · have eval_eq : eval₂ (algebraMap (chain n F m) K) α f' = Polynomial.eval α f'_mapped := by
                  exact eval₂_eq_eval_map (algebraMap (↥(chain n F m)) K)
              rw [eval_eq]
              exact hα
        obtain ⟨α, hα_in, hα_root⟩ := α_in
        exact ⟨α, hα_root⟩
      obtain ⟨αK, hαK⟩ := this
      have αK_in_roots : αK ∈ roots_of_deg_le_n n E := by
        use (f' : Polynomial (chain n F m))
        constructor
        · have : 1 ≤ (f' : Polynomial (chain n F m)).natDegree := h_natDeg_f'
          exact this
        constructor
        · have : (f' : Polynomial (chain n F m)).natDegree = f.natDegree := by
            rfl
          calc
            (f' : Polynomial (chain n F m)).natDegree = f.natDegree := this
            _ ≤ n := hdegn
        · exact hαK
      have α_in_adjoin_set : (αK : K) ∈ ((E : Set K) ∪ roots_of_deg_le_n n E) := Or.inr αK_in_roots
      let α_sub : next_subfield n E := ⟨αK, IntermediateField.subset_adjoin k _ α_in_adjoin_set⟩
      use α_sub
      have : eval₂ (algebraMap K K) (↑α_sub) f'_mapped = 0 := by
        have h_map: f'_mapped = (f' : Polynomial (chain n F m)).map (φ : (↥E) →+* K) := rfl
        rw [h_map, Polynomial.eval₂_map]
        have : (↑α_sub : K) = αK := rfl
        rw [this]
        exact hαK
      exact this
  obtain ⟨α, hα⟩ := h_root
  use m+1, α
  have f'_eq : f'_mapped = f.map (algebraMap F K) := by
    ext i
    simp only [coeff_map, IntermediateField.algebraMap_apply]
    by_cases hi : i ∈ f.support
    · rw [Polynomial.coeff_map]
      rw [Polynomial.coeff_ofFinsupp]
      simp only [mem_support_iff, ne_eq, dite_not]
      · by_cases h0 : f.coeff i = 0
        · have : f.coeff i ≠ 0 := (mem_support_iff.mp hi)
          exact False.elim (this h0)
        · refine Subtype.coe_eq_iff.mpr ?_
          rw [Finsupp.coe_mk]
          simp only [exists_eq_subtype_mk_iff, φ]
          rw [dif_neg h0]
    · by_cases hfi : f.coeff i = 0
      · rw [Polynomial.coeff_map, Polynomial.coeff_ofFinsupp, Subtype.coe_mk]
        simp only [mem_support_iff, ne_eq, dite_not]
        by_cases h0 : f.coeff i = 0
        · simp only [h0, ZeroMemClass.coe_zero, map_eq_zero]
          simp only [Finsupp.coe_mk, dite_eq_left_iff, E]
          exact fun h => False.elim (h hfi)
        · dsimp [φ]
          exact False.elim (h0 hfi)
      · have : f.coeff i ≠ 0 := hfi
        have : i ∈ f.support := by
          simp only [mem_support_iff, ne_eq, this]
          exact fun a => a
        contradiction
  rw [f'_eq] at hα
  have alg_map_id : algebraMap K K = RingHom.id K := rfl
  rw [alg_map_id] at hα
  have eval_relation : eval₂ (algebraMap F K) (α : K) f = 0 := by
    rw [← hα, Polynomial.eval₂_map, RingHom.id_comp]
  rw [eval_relation]

variable (k : Type*) [Field k] [Algebra ℚ k] [IsAlgClosed K]

/-- `F_not_alg_closed`: `F` cannot be algebraically closed under given assumptions. -/
theorem F_not_alg_closed [hk : Nontrivial k] (hkQ : Nonempty (k ≃ₐ[ℚ] ℚ)) :
  ¬ (∀ g : Polynomial F, ∃ α : F, Polynomial.eval₂ (algebraMap F K) (α : K) g = 0) :=
by
  sorry

[Kenny Lau]

why do you have all those extra newlines?

[Nick_adfor]

Kenny Lau said:

why do you have all those extra newlines?

I originally wrote my comments for some lines after '--Notes:', but Zulip doesn't allow that more messages. So I used Ctrl+H to delete them, though this left some extra blank lines.

[Nick_adfor]

Now fixed.

[Nick_adfor]

Snipaste_2025-08-12_21-38-07.jpg
As I do not know how to post latex here, I use a photo.

[Kenny Lau]

your proof is too long, it's not maintainable, you should split it into lemmas

[Kenny Lau]

latex is just $$e^{i\pi}+1=0$$: $e^{i\pi}+1=0$

[Kenny Lau]

I don't think the compositum result you quoted is correct...

[Kenny Lau]

i advise you to find a correct math proof before formalising it in lean, because otherwise you might be putting your effort in vain

[Kenny Lau]

another approach is to sorry all of the previous results so that you can just state that part in lean, and then prove it in lean if you want

[Nick_adfor]

(deleted)

[Nick_adfor]

(deleted)

[Nick_adfor]

Kenny Lau said:

another approach is to sorry all of the previous results so that you can just state that part in lean, and then prove it in lean if you want

As it has already post here, I recommend you to have a whole check of my posting code.

Nick_adfor said:

import Mathlib

variable {k K : Type*} [Field k] [Field K] [Algebra k K] [IsAlgClosed K]
variable (n : ℕ)
variable (F : IntermediateField k K)

open Polynomial

def roots_of_deg_le_n (F : IntermediateField k K) : Set K :=
  { α | ∃ (f : Polynomial k), 1 ≤ f.natDegree ∧ f.natDegree ≤ n ∧
    eval₂ (algebraMap k K) α f = 0 }

def next_subfield (F : IntermediateField k K) : IntermediateField k K :=
  IntermediateField.adjoin k ((F : Set K) ∪ roots_of_deg_le_n n F)

def chain (n : ℕ) (F : IntermediateField k K) : ℕ → IntermediateField k K
| 0 => F
| (m+1) => next_subfield n (chain n F m)

variable {n}

lemma chain_mono (n : ℕ) (F : IntermediateField k K) {i j : ℕ} (h : i ≤ j) :
  (chain n F i) ≤ (chain n F j) := by
  induction h with
  | refl =>
    rfl
  | @step m hm ih =>
    trans chain n F m
    · exact ih
    · show chain n F m ≤ next_subfield n (chain n F m)
      intro x hx
      exact IntermediateField.subset_adjoin k _ (Or.inl hx)

lemma exists_m_covering_coeffs {n : ℕ} {F : IntermediateField k K} {f : Polynomial F} (hf_nonzero : f ≠ 0) :
  ∃ m, ∀ i ∈ f.support, (f.coeff i : K) ∈ (chain n F m : Set K) := by
  sorry

theorem small_polynomial_has_root {f : Polynomial F} (hdeg1 : 1 ≤ f.natDegree) (hdegn : f.natDegree ≤ n) :
  ∃ α : F, eval₂ (algebraMap F K) (α : K) f = 0 :=
by
  sorry

variable (k : Type*) [Field k] [Algebra ℚ k] [IsAlgClosed K]

theorem F_not_alg_closed [hk : Nontrivial k] (hkQ : Nonempty (k ≃ₐ[ℚ] ℚ)) :
  ¬ (∀ g : Polynomial F, ∃ α : F, Polynomial.eval₂ (algebraMap F K) (α : K) g = 0) :=
by
  sorry

[Nick_adfor]

Kenny Lau said:

i advise you to find a correct math proof before formalising it in lean, because otherwise you might be putting your effort in vain

Since my primary task is to derive practical constructions from abstract theorems, completing even half of this work would be acceptable. So I do not need to worry about that.

[Nick_adfor]

Kenny Lau said:

I don't think the compositum result you quoted is correct...

The fixed one without irreducible is in the both the photo and editted initial message. If it is wrong still, you can point it out.

[Nick_adfor]

Kenny Lau said:

your proof is too long, it's not maintainable, you should split it into lemmas

If this aligns with your coding style, I'm happy for you to adapt it accordingly. However, as it differs from my own approach, I currently have no plans to break it down into numerous lemmas (which would require many intermediate 'have' statements).

[Nick_adfor]

Now with lemmas.

import Mathlib

variable {k K : Type*} [Field k] [Field K] [Algebra k K]
variable (n : ℕ)
variable (F : IntermediateField k K)

open Polynomial

/--
`roots_of_deg_le_n F` is the set of elements in `K` that are roots of polynomials over `F`
with degree at least `1` and at most `n`.
-/
def roots_of_deg_le_n (F : IntermediateField k K) : Set K :=
  { α | ∃ (f : Polynomial F), 1 ≤ f.natDegree ∧ f.natDegree ≤ n ∧
    eval₂ (algebraMap F K) α f = 0 }

/--
`next_subfield F` is the intermediate field obtained by adjoining to `F` all elements of
`roots_of_deg_le_n n F`.
-/
def next_subfield (F : IntermediateField k K) : IntermediateField k K :=
  IntermediateField.adjoin k ((F : Set K) ∪ roots_of_deg_le_n n F)

/--
`chain n F` is a sequence of intermediate fields starting from `F` where each next step
is obtained via `next_subfield`.
-/
def chain (n : ℕ) (F : IntermediateField k K) : ℕ → IntermediateField k K
| 0 => F
| (m+1) => next_subfield n (chain n F m)

/--
Given a polynomial `f` over `F` and a proof that all its coefficients are in `E`,
lifts `f` to a polynomial over `E`.
-/
def lift_polynomial {F : IntermediateField k K} {E : IntermediateField k K}
  (f : Polynomial F) (h_coeff : ∀ i ∈ f.support, (f.coeff i : K) ∈ (E : Set K)) :
  Polynomial E :=
Polynomial.ofFinsupp {
  support := f.support,
  toFun := fun i =>
    if hi : i ∈ f.support then
      ⟨f.coeff i, h_coeff i hi⟩
    else
      0,
  mem_support_toFun := fun i => by
    by_cases hi : i ∈ f.support
    · simp only [hi, ↓reduceDIte, ne_eq, true_iff, ZeroMemClass.zero_def, Subtype.mk.injEq, ZeroMemClass.coe_eq_zero]
      exact mem_support_iff.mp hi
    · simp only [hi, ↓reduceDIte, ZeroMemClass.zero_def, ne_eq]
      exact Iff.symm not_true
}

/--
The natural inclusion map from an intermediate field `E` to `K` as a ring homomorphism.
-/
def inclusion_map (E : IntermediateField k K) : E →+* K := {
  toFun := fun x => (x : K),
  map_zero' := by simp only [ZeroMemClass.coe_zero],
  map_add'  := by intros; simp only [AddMemClass.coe_add],
  map_one'  := by simp only [OneMemClass.coe_one],
  map_mul'  := by intros; simp only [MulMemClass.coe_mul]
}

/--
Maps a polynomial over `E` to a polynomial over `K` using the inclusion map.
-/
noncomputable def map_polynomial (E : IntermediateField k K) (f' : Polynomial E) : Polynomial K :=
  f'.map (inclusion_map E)


/-- Show that there exists a stage m where all coefficients of f are in chain n F m. This is because coefficients are in F, which is the 0-th stage of the chain-/
lemma exists_m_covering_coeffs {n : ℕ} {F : IntermediateField k K} {f : Polynomial F} :
    ∃ m, ∀ i ∈ f.support, (f.coeff i : K) ∈ (chain n F m : Set K) := by
  by_cases hf_zero : f = 0
  · -- If f = 0, f.support is empty, so any m satisfies the condition
    use 0
    intro i hi
    exact Subtype.coe_prop (f.coeff i)
  · -- If f ≠ 0, coefficients are in F
    use 0
    intro i hi
    exact (f.coeff i).2

/--
Given a polynomial over an intermediate field E in an algebraically closed extension K,
if the polynomial has degree between 1 and n, then it has a root in K that lies in
the set of roots of degree ≤ n polynomials over E.
-/
lemma exists_root_in_K_and_roots_set {E : IntermediateField k K} [IsAlgClosed K] (f' : Polynomial E) (hdeg1 : 1 ≤ f'.natDegree)
  (hdegn : f'.natDegree ≤ n) (hf'_nonzero : f' ≠ 0) :
  ∃ (x : K), eval₂ (algebraMap E K) x f' = 0 := by
  let f'_mapped := f'.map (inclusion_map E)

  -- Show degree is not zero (since it's at least 1)
  have hd : f'.degree ≠ 0 := by
    intro Hdeg0
    have := (degree_eq_iff_natDegree_eq hf'_nonzero).mp Hdeg0
    have h_natDeg_f' : f'.natDegree = 0 := by
      exact this
    linarith

  -- Find a root that's in roots_of_deg_le_n
  have α_in : ∃ α : K, α ∈ roots_of_deg_le_n n E ∧
    eval₂ (algebraMap E K) α f' = 0 := by
      -- Show mapped polynomial has nonzero degree
      have hd_mapped : f'_mapped.degree ≠ 0 := by
        rw [degree_map]
        exact hd

      -- Use IsAlgClosed to get a root
      obtain ⟨α, hα⟩ := IsAlgClosed.exists_root f'_mapped hd_mapped
      use α
      constructor
      · -- First condition: provide the witness polynomial f'
        use f'
        constructor
        · exact hdeg1
        constructor
        · exact hdegn
        · rw [eval₂_eq_eval_map (algebraMap E K)]
          exact hα
      · rw [eval₂_eq_eval_map (algebraMap E K)]
        exact hα

  obtain ⟨α, hα_in, hα_root⟩ := α_in
  exact ⟨α, hα_root⟩

/--
Given a polynomial over E with degree between 1 and n, there exists a root
in the next extension field obtained by adjoining roots of degree ≤ n polynomials.
-/
lemma exists_root_in_next_subfield {E : IntermediateField k K} [IsAlgClosed K] (f' : Polynomial E) (hdeg1 : 1 ≤ f'.natDegree) (hdegn : f'.natDegree ≤ n) :
  ∃ α : next_subfield n E, eval₂ (algebraMap K K) α (f'.map (inclusion_map E)) = 0 := by
  let φ := inclusion_map E
  let f'_mapped := f'.map φ

  -- First show f' has degree at least 1
  have h_natDeg_f' : 1 ≤ f'.natDegree := hdeg1

  -- Show f' is nonzero
  have hf'_nonzero : f' ≠ 0 := by
    intro H; rw [H, natDegree_zero] at h_natDeg_f'; linarith

  -- Get root from algebraic closure
  obtain ⟨αK, hαK⟩ := exists_root_in_K_and_roots_set n f' hdeg1 hdegn hf'_nonzero

  -- Package the root
  let α_sub : next_subfield n E := ⟨αK, IntermediateField.subset_adjoin k _ (Or.inr
    ⟨f', hdeg1, hdegn, hαK⟩)⟩

  use α_sub
  simp only [RingHom.id_comp, eval₂_map, Subtype.coe_mk]
  rw [← hαK]
  exact rfl

/--
The lifted polynomial, when mapped to K through the inclusion, equals
the original polynomial mapped through the algebra map.
-/
lemma lifted_poly_commutes {F E : IntermediateField k K} [DecidableEq K] (f : Polynomial F) (h_coeff : ∀ i ∈ f.support, (f.coeff i : K) ∈ (E : Set K)) :
  (lift_polynomial f h_coeff).map (inclusion_map E) = f.map (algebraMap F K) := by
  ext i
  simp only [coeff_map, IntermediateField.algebraMap_apply, coeff_ofFinsupp]
  by_cases hi : i ∈ f.support
  · -- Case when i ∈ support
    simp only [hi, lift_polynomial, dite_true]
    by_cases h0 : f.coeff i = 0
    · -- Contradictory case where coeff is zero but in support
      have := mem_support_iff.mp hi
      contradiction
    · -- Nonzero coefficient case
      simp [dif_neg h0]
      exact rfl
  · -- Case when i ∉ support
    simp only [hi, lift_polynomial, dite_false, ZeroMemClass.zero_def]
    by_cases h0 : f.coeff i = 0
    · -- Consistent zero case
      simp only [mem_support_iff, ne_eq, dite_not, coeff_ofFinsupp, Finsupp.coe_mk, h0, ↓reduceDIte,
        ZeroMemClass.coe_zero, map_eq_zero, ZeroMemClass.zero_def]
    · -- Contradictory case where coeff nonzero but not in support
      have := mem_support_iff.mpr h0
      contradiction

/--
If a polynomial `f` over `F` has degree between `1` and `n`, then there exists some
stage `m` in the chain where `f` has a root in `chain n F m`.
-/
theorem small_polynomial_has_root {f : Polynomial F} [IsAlgClosed K] [DecidableEq K] (hdeg1 : 1 ≤ f.natDegree) (hdegn : f.natDegree ≤ n) :
  ∃ (m : ℕ) (α : chain n F m), eval₂ (algebraMap _ K) α f = 0 := by
  -- First handle the trivial case where f is zero (which contradicts the degree condition)
  by_cases hf_zero : f = 0
  · exfalso; rw [hf_zero, natDegree_zero] at hdeg1; linarith

  -- Get the specific m that covers all coefficients of our polynomial f
  obtain ⟨m, hm⟩ := exists_m_covering_coeffs (n := n) (F := F)

  -- Lift the polynomial f to a polynomial over the m-th stage of our chain
  let f' := lift_polynomial f hm

  -- Define E as the m-th stage of our chain for convenience
  let E := chain n F m

  -- Define the inclusion map from E to K as a ring homomorphism
  -- This will let us map our polynomial f' to K
  let φ := inclusion_map E

  -- Create a version of f' mapped to K via the inclusion φ
  -- Now we can work with f'_mapped as a polynomial over the algebraically closed field K
  let f'_mapped := f'.map φ

  -- Show that f'_mapped has a root in the next stage of the chain
  have h_root : ∃ α : next_subfield n E, eval₂ (algebraMap _ K) α f'_mapped = 0 := by
      exact exists_root_in_next_subfield n f' hdeg1 hdegn

  -- Get the root we found
  obtain ⟨α, hα⟩ := h_root
  use m+1, α

  -- Prove f'_mapped equals f mapped via algebraMap F K by coefficient-wise equality
  have f'_eq : f'_mapped = f.map (algebraMap F K) := by
    exact lifted_poly_commutes f hm
  -- Rewrite using the equality we just proved
  rw [f'_eq] at hα

  -- The algebra map from K to K is just the identity
  have alg_map_id : algebraMap K K = RingHom.id K := rfl
  rw [alg_map_id] at hα

  -- Show the evaluation relation we need for the original polynomial f
  have eval_relation : eval₂ (algebraMap F K) (α : K) f = 0 := by
    rw [← hα, Polynomial.eval₂_map, RingHom.id_comp]  -- Simplify using the identity map
  rw [eval_relation]

/-- `F_not_alg_closed`: `F` cannot be algebraically closed under given assumptions. -/
theorem F_not_alg_closed (k : Type*) [Field k] [Algebra ℚ k] [IsAlgClosed K] [hk : Nontrivial k] (hkQ : Nonempty (k ≃ₐ[ℚ] ℚ)) :
  ¬ (∀ g : Polynomial F, ∃ α : F, Polynomial.eval₂ (algebraMap F K) (α : K) g = 0) :=
by
  sorry

[Nick_adfor]

(deleted)