[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots p))))
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
rw [← Multiset.prod_toList, AlgHom.map_list_prod] at h 
[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (List.prod (List.map (↑(aeval a)) (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p)))))
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
replace h := mt List.prod_isUnit h
[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h :
  ¬∀ (m : (fun x => A) (List.prod (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p))))),
      m ∈ List.map (↑(aeval a)) (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p))) → IsUnit m
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X, exists_exists_and_eq_and,
  Multiset.mem_map, AlgHom.map_sub] at h 
[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ∃ a_1, a_1 ∈ roots p ∧ ¬IsUnit (a - ↑↑ₐ a_1)
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
rcases h with ⟨r, r_mem, r_nu⟩
[GOAL]
case intro.intro
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ roots p
r_nu : ¬IsUnit (a - ↑↑ₐ r)
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
[PROOFSTEP]
exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], (mem_roots'.1 r_mem).2⟩
[GOAL]
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ roots p
r_nu : ¬IsUnit (a - ↑↑ₐ r)
⊢ r ∈ σ a
[PROOFSTEP]
rwa [mem_iff, ← IsUnit.sub_iff]
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
⊢ (fun x => eval x p) '' σ a ⊆ σ (↑(aeval a) p)
[PROOFSTEP]
rintro _ ⟨k, hk, rfl⟩
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
let q := C (eval k p) - p
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
have hroot : IsRoot q k := by simp only [eval_C, eval_sub, sub_self, IsRoot.def]
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
⊢ IsRoot q k
[PROOFSTEP]
simp only [eval_C, eval_sub, sub_self, IsRoot.def]
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot : IsRoot q k
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
rw [← mul_div_eq_iff_isRoot, ← neg_mul_neg, neg_sub] at hroot 
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
⊢ ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
[PROOFSTEP]
simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
⊢ (fun x => eval x p) k ∈ σ (↑(aeval a) p)
[PROOFSTEP]
rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
⊢ ¬IsUnit (↑(aeval a) (↑C k - X) * ↑(aeval a) (-(q / (X - ↑C k))))
[PROOFSTEP]
have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a : 𝕜[X] →ₐ[𝕜] A)
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
hcomm : Commute (↑(aeval a) (↑C k - X)) (↑(aeval a) (-(q / (X - ↑C k))))
⊢ ¬IsUnit (↑(aeval a) (↑C k - X) * ↑(aeval a) (-(q / (X - ↑C k))))
[PROOFSTEP]
apply mt fun h => (hcomm.isUnit_mul_iff.mp h).1
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
k : 𝕜
hk : k ∈ σ a
q : (fun x => 𝕜[X]) (eval k p) := ↑C (eval k p) - p
hroot✝ : (X - ↑C k) * (q / (X - ↑C k)) = q
hroot : (↑C k - X) * -(q / (X - ↑C k)) = q
aeval_q_eq : ↑↑ₐ (eval k p) - ↑(aeval a) p = ↑(aeval a) q
hcomm : Commute (↑(aeval a) (↑C k - X)) (↑(aeval a) (-(q / (X - ↑C k))))
⊢ ¬IsUnit (↑(aeval a) (↑C k - X))
[PROOFSTEP]
simpa only [aeval_X, aeval_C, AlgHom.map_sub] using hk
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
⊢ σ (↑(aeval a) p) = (fun x => eval x p) '' σ a
[PROOFSTEP]
refine'
  Set.eq_of_subset_of_subset (fun k hk => _)
    (subset_polynomial_aeval a p)
      -- write `C k - p` product of linear factors and a constant; show `C k - p ≠ 0`.
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have hprod := eq_prod_roots_of_splits_id (IsAlgClosed.splits (C k - p))
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have h_ne : C k - p ≠ 0 :=
  ne_zero_of_degree_gt <| by rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
⊢ ?m.286583 < degree (↑C k - p)
[PROOFSTEP]
rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have lead_ne := leadingCoeff_ne_zero.mpr h_ne
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have lead_unit := (Units.map ↑ₐ.toMonoidHom (Units.mk0 _ lead_ne)).isUnit
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
have p_a_eq : aeval a (C k - p) = ↑ₐ k - aeval a p := by simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
⊢ ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
[PROOFSTEP]
simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk : k ∈ σ (↑(aeval a) p)
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
rw [mem_iff, ← p_a_eq, hprod, aeval_mul, ((Commute.all _ _).map (aeval a : 𝕜[X] →ₐ[𝕜] A)).isUnit_mul_iff, aeval_C] at hk 
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hk :
  ¬(IsUnit (↑↑ₐ (leadingCoeff (↑C k - p))) ∧
      IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p))))))
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
replace hk := exists_mem_of_not_isUnit_aeval_prod (not_and.mp hk lead_unit)
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
hk : ∃ k_1, k_1 ∈ σ a ∧ eval k_1 (↑C k - p) = 0
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
rcases hk with ⟨r, r_mem, r_ev⟩
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
r : 𝕜
r_mem : r ∈ σ a
r_ev : eval r (↑C k - p) = 0
⊢ k ∈ (fun x => eval x p) '' σ a
[PROOFSTEP]
exact ⟨r, r_mem, symm (by simpa [eval_sub, eval_C, sub_eq_zero] using r_ev)⟩
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hdeg : 0 < degree p
k : 𝕜
hprod : ↑C k - p = ↑C (leadingCoeff (↑C k - p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (↑C k - p)))
h_ne : ↑C k - p ≠ 0
lead_ne : leadingCoeff (↑C k - p) ≠ 0
lead_unit : IsUnit ↑(↑(Units.map ↑↑ₐ) (Units.mk0 (leadingCoeff (↑C k - p)) lead_ne))
p_a_eq : ↑(aeval a) (↑C k - p) = ↑↑ₐ k - ↑(aeval a) p
r : 𝕜
r_mem : r ∈ σ a
r_ev : eval r (↑C k - p) = 0
⊢ k = (fun x => eval x p) r
[PROOFSTEP]
simpa [eval_sub, eval_C, sub_eq_zero] using r_ev
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
[PROOFSTEP]
nontriviality A
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
[PROOFSTEP]
refine' Or.elim (le_or_gt (degree p) 0) (fun h => _) (map_polynomial_aeval_of_degree_pos a p)
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
h : degree p ≤ 0
⊢ σ (↑(aeval a) p) = (fun k => eval k p) '' σ a
[PROOFSTEP]
rw [eq_C_of_degree_le_zero h]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
p : 𝕜[X]
hnon : Set.Nonempty (σ a)
✝ : Nontrivial A
h : degree p ≤ 0
⊢ σ (↑(aeval a) (↑C (coeff p 0))) = (fun k => eval k (↑C (coeff p 0))) '' σ a
[PROOFSTEP]
simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]
[GOAL]
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
n : ℕ
⊢ (fun x => x ^ n) '' σ a ⊆ σ (a ^ n)
[PROOFSTEP]
simpa only [eval_pow, eval_X, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X])
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ σ (a ^ n) = (fun x => x ^ n) '' σ a
[PROOFSTEP]
simpa only [aeval_X_pow, eval_pow, eval_X] using
  map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rwa [degree_X_pow, Nat.cast_pos])
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
n : ℕ
hn : 0 < n
⊢ 0 < degree (X ^ n)
[PROOFSTEP]
rwa [degree_X_pow, Nat.cast_pos]
[GOAL]
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : IsAlgClosed 𝕜
a : A
ha : Set.Nonempty (σ a)
n : ℕ
⊢ σ (a ^ n) = (fun x => x ^ n) '' σ a
[PROOFSTEP]
simpa only [aeval_X_pow, eval_pow, eval_X] using map_polynomial_aeval_of_nonempty a (X ^ n) ha
[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p ; rw [h_eval_p]; simp
[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ ¬IsUnit (↑(aeval a) p)
[PROOFSTEP]
rw [← aeval_def] at h_eval_p 
[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : ↑(aeval a) p = 0
⊢ ¬IsUnit (↑(aeval a) p)
[PROOFSTEP]
rw [h_eval_p]
[GOAL]
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : ↑(aeval a) p = 0
⊢ ¬IsUnit 0
[PROOFSTEP]
simp
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) p)
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
rw [eq_prod_roots_of_monic_of_splits_id h_mon (IsAlgClosed.splits p)] at nu 
[GOAL]
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))))
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
obtain ⟨k, hk, _⟩ := exists_mem_of_not_isUnit_aeval_prod nu
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))))
k : 𝕜
hk : k ∈ σ a
right✝ : eval k p = 0
⊢ Set.Nonempty (σ a)
[PROOFSTEP]
exact ⟨k, hk⟩
