Mathlib.FieldTheory.IsAlgClosed.Basic

IsAlgClosed structure

Full source

/-- Typeclass for algebraically closed fields.

To show `Polynomial.Splits p f` for an arbitrary ring homomorphism `f`,
see `IsAlgClosed.splits_codomain` and `IsAlgClosed.splits_domain`.
-/
@[stacks 09GR "The definition of `IsAlgClosed` in mathlib is 09GR (4)"]
class IsAlgClosed : Prop where
  splits : ∀ p : k[X], p.Splits <| RingHom.id k

Algebraically Closed Field

Informal description

A field $ k $ is called *algebraically closed* if every non-constant polynomial with coefficients in $ k $ has a root in $ k $. This implies that every such polynomial splits into linear factors over $ k $.

IsAlgClosed.splits_codomain theorem

{k K : Type*} [Field k] [IsAlgClosed k] [CommRing K] {f : K →+* k} (p : K[X]) : p.Splits f

Full source

/-- Every polynomial splits in the field extension `f : K →+* k` if `k` is algebraically closed.

See also `IsAlgClosed.splits_domain` for the case where `K` is algebraically closed.
-/
theorem IsAlgClosed.splits_codomain {k K : Type*} [Field k] [IsAlgClosed k] [CommRing K]
    {f : K →+* k} (p : K[X]) : p.Splits f := by
  convert IsAlgClosed.splits (p.map f); simp [splits_map_iff]

Polynomials Split over Codomain of Algebraically Closed Fields

Informal description

Let $k$ be an algebraically closed field and $K$ be a commutative ring. For any ring homomorphism $f \colon K \to k$ and any polynomial $p \in K[X]$, the polynomial $p$ splits in $k$ via $f$. That is, $p$ factors into linear polynomials in $k[X]$ when mapped through $f$.

IsAlgClosed.splits_domain theorem

{k K : Type*} [Field k] [IsAlgClosed k] [Field K] {f : k →+* K} (p : k[X]) : p.Splits f

Full source

/-- Every polynomial splits in the field extension `f : K →+* k` if `K` is algebraically closed.

See also `IsAlgClosed.splits_codomain` for the case where `k` is algebraically closed.
-/
theorem IsAlgClosed.splits_domain {k K : Type*} [Field k] [IsAlgClosed k] [Field K] {f : k →+* K}
    (p : k[X]) : p.Splits f :=
  Polynomial.splits_of_splits_id _ <| IsAlgClosed.splits _

Polynomials Split over Field Extensions from Algebraically Closed Fields

Informal description

Let $k$ be an algebraically closed field and $K$ be any field. For any ring homomorphism $f \colon k \to K$ and any polynomial $p \in k[X]$, the polynomial $p$ splits in $K$ via $f$. That is, $p$ factors into linear polynomials in $K[X]$ when mapped through $f$.

IsAlgClosed.exists_root theorem

[IsAlgClosed k] (p : k[X]) (hp : p.degree ≠ 0) : ∃ x, IsRoot p x

Full source

/--
If `k` is algebraically closed, then every nonconstant polynomial has a root.
-/
@[stacks 09GR "(4) ⟹ (3)"]
theorem exists_root [IsAlgClosed k] (p : k[X]) (hp : p.degree ≠ 0) : ∃ x, IsRoot p x :=
  exists_root_of_splits _ (IsAlgClosed.splits p) hp

Existence of Roots for Non-Constant Polynomials over Algebraically Closed Fields

Informal description

Let $k$ be an algebraically closed field. For any non-constant polynomial $p \in k[X]$, there exists an element $x \in k$ such that $p(x) = 0$.

IsAlgClosed.exists_pow_nat_eq theorem

[IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z, z ^ n = x

Full source

theorem exists_pow_nat_eq [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z, z ^ n = x := by
  have : degreedegree (X ^ n - C x) ≠ 0 := by
    rw [degree_X_pow_sub_C hn x]
    exact ne_of_gt (WithBot.coe_lt_coe.2 hn)
  obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this
  use z
  simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz
  exact sub_eq_zero.1 hz

Existence of $n$-th Roots in Algebraically Closed Fields

Informal description

Let $k$ be an algebraically closed field. For any element $x \in k$ and any positive integer $n$, there exists an element $z \in k$ such that $z^n = x$.

IsAlgClosed.exists_eq_mul_self theorem

[IsAlgClosed k] (x : k) : ∃ z, x = z * z

Full source

theorem exists_eq_mul_self [IsAlgClosed k] (x : k) : ∃ z, x = z * z := by
  rcases exists_pow_nat_eq x zero_lt_two with ⟨z, rfl⟩
  exact ⟨z, sq z⟩

Existence of Square Roots in Algebraically Closed Fields

Informal description

Let $k$ be an algebraically closed field. For any element $x \in k$, there exists an element $z \in k$ such that $x = z^2$.

IsAlgClosed.roots_eq_zero_iff theorem

[IsAlgClosed k] {p : k[X]} : p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)

Full source

theorem 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

Empty Roots iff Constant Polynomial in Algebraically Closed Fields

Informal description

Let $k$ be an algebraically closed field and $p \in k[X]$ a polynomial. The multiset of roots of $p$ is empty if and only if $p$ is a constant polynomial, i.e., $p = c$ for some $c \in k$ (where $c$ is the constant term $p(0)$).

IsAlgClosed.exists_eval₂_eq_zero_of_injective theorem

 {R : Type*} [Semiring R] [IsAlgClosed k] (f : R →+* k) (hf : Function.Injective f) (p : R[X]) (hp : p.degree ≠ 0) :
  ∃ x, p.eval₂ f x = 0

Full source

theorem exists_eval₂_eq_zero_of_injective {R : Type*} [Semiring R] [IsAlgClosed k] (f : R →+* k)
    (hf : Function.Injective f) (p : R[X]) (hp : p.degree ≠ 0) : ∃ x, p.eval₂ f x = 0 :=
  let ⟨x, hx⟩ := exists_root (p.map f) (by rwa [degree_map_eq_of_injective hf])
  ⟨x, by rwa [eval₂_eq_eval_map, ← IsRoot]⟩

Existence of Roots for Non-Constant Polynomials under Injective Homomorphism in Algebraically Closed Fields

Informal description

Let $R$ be a semiring and $k$ an algebraically closed field. Given an injective ring homomorphism $f \colon R \to k$ and a non-constant polynomial $p \in R[X]$, there exists an element $x \in k$ such that the evaluation of $p$ at $x$ via $f$ is zero, i.e., $p$ has a root in $k$ under the homomorphism $f$.

IsAlgClosed.exists_eval₂_eq_zero theorem

 {R : Type*} [DivisionRing R] [IsAlgClosed k] (f : R →+* k) (p : R[X]) (hp : p.degree ≠ 0) : ∃ x, p.eval₂ f x = 0

Full source

theorem exists_eval₂_eq_zero {R : Type*} [DivisionRing R] [IsAlgClosed k] (f : R →+* k) (p : R[X])
    (hp : p.degree ≠ 0) : ∃ x, p.eval₂ f x = 0 :=
  exists_eval₂_eq_zero_of_injective f f.injective p hp

Existence of Roots for Non-Constant Polynomials in Algebraically Closed Fields via Ring Homomorphism

Informal description

Let $R$ be a division ring and $k$ an algebraically closed field. Given a ring homomorphism $f \colon R \to k$ and a non-constant polynomial $p \in R[X]$, there exists an element $x \in k$ such that the evaluation of $p$ at $x$ via $f$ is zero, i.e., $p$ has a root in $k$ under the homomorphism $f$.

IsAlgClosed.exists_aeval_eq_zero_of_injective theorem

 {R : Type*} [CommSemiring R] [IsAlgClosed k] [Algebra R k] (hinj : Function.Injective (algebraMap R k)) (p : R[X])
  (hp : p.degree ≠ 0) : ∃ x : k, aeval x p = 0

Full source

theorem exists_aeval_eq_zero_of_injective {R : Type*} [CommSemiring R] [IsAlgClosed k] [Algebra R k]
    (hinj : Function.Injective (algebraMap R k)) (p : R[X]) (hp : p.degree ≠ 0) :
    ∃ x : k, aeval x p = 0 :=
  exists_eval₂_eq_zero_of_injective (algebraMap R k) hinj p hp

Existence of roots for non-constant polynomials under injective algebra maps in algebraically closed fields

Informal description

Let $R$ be a commutative semiring and $k$ an algebraically closed field with an $R$-algebra structure. If the algebra map $R \to k$ is injective, then for any non-constant polynomial $p \in R[X]$, there exists an element $x \in k$ such that the evaluation of $p$ at $x$ is zero, i.e., $p$ has a root in $k$.

IsAlgClosed.exists_aeval_eq_zero theorem

{R : Type*} [Field R] [IsAlgClosed k] [Algebra R k] (p : R[X]) (hp : p.degree ≠ 0) : ∃ x : k, aeval x p = 0

Full source

theorem 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

Existence of roots for non-constant polynomials in algebraically closed field extensions

Informal description

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$ is zero, i.e., $p$ has a root in $k$.

IsAlgClosed.of_exists_root theorem

(H : ∀ p : k[X], p.Monic → Irreducible p → ∃ x, p.eval x = 0) : IsAlgClosed k

Full source

/--
If every nonconstant polynomial over `k` has a root, then `k` is algebraically closed.
-/
@[stacks 09GR "(3) ⟹ (4)"]
theorem 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

Criterion for Algebraically Closed Fields via Roots of Irreducible Polynomials

Informal description

A field $k$ is algebraically closed if every monic irreducible polynomial $p \in k[X]$ has a root in $k$.

IsAlgClosed.of_ringEquiv theorem

(k' : Type u) [Field k'] (e : k ≃+* k') [IsAlgClosed k] : IsAlgClosed k'

Full source

theorem of_ringEquiv (k' : Type u) [Field k'] (e : k ≃+* k')
    [IsAlgClosed k] : IsAlgClosed k' := by
  apply IsAlgClosed.of_exists_root
  intro p hmp hp
  have hpe : degreedegree (p.map e.symm.toRingHom) ≠ 0 := by
    rw [degree_map]
    exact ne_of_gt (degree_pos_of_irreducible hp)
  rcases IsAlgClosed.exists_root (k := k) (p.map e.symm.toRingHom) hpe with ⟨x, hx⟩
  use e x
  rw [IsRoot] at hx
  apply e.symm.injective
  rw [map_zero, ← hx]
  clear hx hpe hp hmp
  induction p using Polynomial.induction_on <;> simp_all

Algebraic Closure is Preserved under Ring Isomorphism

Informal description

Let $k$ and $k'$ be fields, and let $e \colon k \simeq+* k'$ be a ring isomorphism between them. If $k$ is algebraically closed, then $k'$ is also algebraically closed.

IsAlgClosed.degree_eq_one_of_irreducible theorem

[IsAlgClosed k] {p : k[X]} (hp : Irreducible p) : p.degree = 1

Full source

/--
If `k` is algebraically closed, then every irreducible polynomial over `k` is linear.
-/
@[stacks 09GR "(4) ⟹ (2)"]
theorem degree_eq_one_of_irreducible [IsAlgClosed k] {p : k[X]} (hp : Irreducible p) :
    p.degree = 1 :=
  degree_eq_one_of_irreducible_of_splits hp (IsAlgClosed.splits_codomain _)

Irreducible Polynomials in Algebraically Closed Fields Have Degree One

Informal description

Let $k$ be an algebraically closed field. For any irreducible polynomial $p \in k[X]$, the degree of $p$ is equal to $1$.

IsAlgClosed.algebraMap_bijective_of_isIntegral theorem

 {k K : Type*} [Field k] [Ring K] [IsDomain K] [hk : IsAlgClosed k] [Algebra k K] [Algebra.IsIntegral k K] :
  Function.Bijective (algebraMap k K)

Full source

theorem algebraMap_bijective_of_isIntegral {k K : Type*} [Field k] [Ring K] [IsDomain K]
    [hk : IsAlgClosed k] [Algebra k K] [Algebra.IsIntegral k K] :
    Function.Bijective (algebraMap k K) := by
  refine ⟨RingHom.injective _, fun x ↦ ⟨-(minpoly k x).coeff 0, ?_⟩⟩
  have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (Algebra.IsIntegral.isIntegral x)
  have h : (minpoly k x).degree = 1 := degree_eq_one_of_irreducible k (minpoly.irreducible
    (Algebra.IsIntegral.isIntegral x))
  have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
  rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C,
    add_eq_zero_iff_eq_neg] at this
  exact (RingHom.map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm

Bijectivity of Algebra Maps from Algebraically Closed Fields to Integral Domains

Informal description

Let $k$ be an algebraically closed field and $K$ be an integral domain with a ring structure. Suppose there is an algebra map from $k$ to $K$ such that $K$ is integral over $k$. Then the algebra map $\text{algebraMap} \colon k \to K$ is bijective.

IsAlgClosed.ringHom_bijective_of_isIntegral theorem

 {k K : Type*} [Field k] [CommRing K] [IsDomain K] [IsAlgClosed k] (f : k →+* K) (hf : f.IsIntegral) :
  Function.Bijective f

Full source

theorem ringHom_bijective_of_isIntegral {k K : Type*} [Field k] [CommRing K] [IsDomain K]
    [IsAlgClosed k] (f : k →+* K) (hf : f.IsIntegral) : Function.Bijective f :=
  let _ : Algebra k K := f.toAlgebra
  have : Algebra.IsIntegral k K := ⟨hf⟩
  algebraMap_bijective_of_isIntegral

Bijectivity of Integral Ring Homomorphisms from Algebraically Closed Fields to Integral Domains

Informal description

Let $k$ be an algebraically closed field and $K$ be a commutative integral domain. Given a ring homomorphism $f \colon k \to K$ that is integral (i.e., every element of $K$ is integral over $k$ via $f$), then $f$ is bijective.

IsAlgClosed.algebraMap_surjective_of_isIntegral' theorem

 {k K : Type*} [Field k] [CommRing K] [IsDomain K] [IsAlgClosed k] (f : k →+* K) (hf : f.IsIntegral) :
  Function.Surjective f

Full source

@[deprecated "ringHom_bijective_of_isIntegral" (since := "2025-04-16")]
theorem algebraMap_surjective_of_isIntegral' {k K : Type*} [Field k] [CommRing K] [IsDomain K]
    [IsAlgClosed k] (f : k →+* K) (hf : f.IsIntegral) : Function.Surjective f :=
  (ringHom_bijective_of_isIntegral f hf).surjective

Surjectivity of Integral Ring Homomorphisms from Algebraically Closed Fields to Integral Domains

Informal description

Let $k$ be an algebraically closed field and $K$ be a commutative integral domain. Given a ring homomorphism $f \colon k \to K$ that is integral (i.e., every element of $K$ is integral over $k$ via $f$), then $f$ is surjective.

Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed theorem

 (K : Type v) [Field K] [IsAlgClosed K] [Algebra k K] (p q : k[X]) :
  IsCoprime p q ↔ ∀ a : K, aeval a p ≠ 0 ∨ aeval a q ≠ 0

Full source

lemma Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed (K : Type v) [Field K] [IsAlgClosed K]
    [Algebra k K] (p q : k[X]) : IsCoprimeIsCoprime p q ↔ ∀ a : K, aeval a p ≠ 0 ∨ aeval a q ≠ 0 := by
  refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hu h0 => ?_⟩
  · replace h := h 0
    contrapose! h
    rw [h.left, h.right, map_zero, and_self]
  · rintro ⟨_, rfl⟩ ⟨_, rfl⟩
    obtain ⟨a, ha : _ = _⟩ := IsAlgClosed.exists_root (x.map <| algebraMap k K) <| by
      simpa only [degree_map] using (ne_of_lt <| degree_pos_of_ne_zero_of_nonunit h0 hu).symm
    exact not_and_or.mpr (h a) (by simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and])

Coprimality of Polynomials over Algebraically Closed Fields via Evaluation Non-Vanishing

Informal description

Let $k$ be a field and $K$ be an algebraically closed field extension of $k$ with an algebra structure $[Algebra\,k\,K]$. For any two polynomials $p, q \in k[X]$, the following are equivalent: 1. $p$ and $q$ are coprime in $k[X]$. 2. For every element $a \in K$, at least one of the evaluations $\text{aeval}\,a\,p$ or $\text{aeval}\,a\,q$ is nonzero. Here, $\text{aeval}\,a\,p$ denotes the evaluation of the polynomial $p$ at $a$ in $K$.

IsAlgClosure structure

(R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K] [NoZeroSMulDivisors R K]

Full source

/-- Typeclass for an extension being an algebraic closure. -/
@[stacks 09GS]
class IsAlgClosure (R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K]
    [NoZeroSMulDivisors R K] : Prop where
  isAlgClosed : IsAlgClosed K
  isAlgebraic : Algebra.IsAlgebraic R K

Algebraic Closure of a Commutative Ring

Informal description

The structure `IsAlgClosure R K` asserts that the field extension $ K $ of the commutative ring $ R $ is an algebraic closure, meaning: 1. The canonical map from $ R $ to $ K $ is injective, 2. $ K $ is algebraically closed (every non-constant polynomial over $ K $ has a root in $ K $), and 3. $ K $ is algebraic over $ R $ (every element of $ K $ is a root of some non-zero polynomial with coefficients in $ R $).

isAlgClosure_iff theorem

(K : Type v) [Field K] [Algebra k K] : IsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K

Full source

theorem isAlgClosure_iff (K : Type v) [Field K] [Algebra k K] :
    IsAlgClosureIsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K :=
  ⟨fun h => ⟨h.1, h.2⟩, fun h => ⟨h.1, h.2⟩⟩

Characterization of Algebraic Closure: $K$ is an algebraic closure of $k$ if and only if $K$ is algebraically closed and algebraic over $k$

Informal description

Let $k$ be a field and $K$ be a field extension of $k$ with an algebra structure $[Algebra\,k\,K]$. Then $K$ is an algebraic closure of $k$ if and only if: 1. $K$ is algebraically closed, and 2. $K$ is algebraic over $k$.

IsAlgClosure.normal instance

(R K : Type*) [Field R] [Field K] [Algebra R K] [IsAlgClosure R K] : Normal R K

Full source

instance (priority := 100) IsAlgClosure.normal (R K : Type*) [Field R] [Field K] [Algebra R K]
    [IsAlgClosure R K] : Normal R K where
  toIsAlgebraic := IsAlgClosure.isAlgebraic
  splits' _ := @IsAlgClosed.splits_codomain _ _ _ (IsAlgClosure.isAlgClosed R) _ _ _

Algebraic Closure Implies Normal Extension

Informal description

For any field extension $ K $ of a field $ R $ that is an algebraic closure of $ R $, the extension $ K/R $ is normal. That is, every irreducible polynomial over $ R $ that has a root in $ K $ splits completely in $ K $.

IsAlgClosure.separable instance

(R K : Type*) [Field R] [Field K] [Algebra R K] [IsAlgClosure R K] [CharZero R] : Algebra.IsSeparable R K

Full source

instance (priority := 100) IsAlgClosure.separable (R K : Type*) [Field R] [Field K] [Algebra R K]
    [IsAlgClosure R K] [CharZero R] : Algebra.IsSeparable R K :=
  ⟨fun _ => (minpoly.irreducible (Algebra.IsIntegral.isIntegral _)).separable⟩

Separability of Algebraic Closures in Characteristic Zero

Informal description

For any fields $R$ and $K$ with characteristic zero, if $K$ is an algebraic closure of $R$, then the field extension $K/R$ is separable. This means that the minimal polynomial of every element in $K$ over $R$ has no repeated roots in any extension field.

IsAlgClosed.instIsAlgClosure instance

(F : Type*) [Field F] [IsAlgClosed F] : IsAlgClosure F F

Full source

instance IsAlgClosed.instIsAlgClosure (F : Type*) [Field F] [IsAlgClosed F] : IsAlgClosure F F where
  isAlgClosed := ‹_›
  isAlgebraic := .of_finite F F

An Algebraically Closed Field is its Own Algebraic Closure

Informal description

For any algebraically closed field $F$, $F$ is an algebraic closure of itself. This means that the canonical map from $F$ to itself is injective, $F$ is algebraically closed (every non-constant polynomial over $F$ has a root in $F$), and $F$ is algebraic over itself (every element of $F$ is a root of some non-zero polynomial with coefficients in $F$).

IsAlgClosure.of_splits theorem

 {R K} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [Algebra.IsIntegral R K] [NoZeroSMulDivisors R K]
  (h : ∀ p : R[X], p.Monic → Irreducible p → p.Splits (algebraMap R K)) : IsAlgClosure R K

Full source

theorem IsAlgClosure.of_splits {R K} [CommRing R] [IsDomain R] [Field K] [Algebra R K]
    [Algebra.IsIntegral R K] [NoZeroSMulDivisors R K]
    (h : ∀ p : R[X], p.Monic → Irreducible p → p.Splits (algebraMap R K)) : IsAlgClosure R K where
  isAlgebraic := inferInstance
  isAlgClosed := .of_exists_root _ fun _p _ p_irred ↦
    have ⟨g, monic, irred, dvd⟩ := p_irred.exists_dvd_monic_irreducible_of_isIntegral (K := R)
    exists_root_of_splits _ (splits_of_splits_of_dvd _ (map_monic_ne_zero monic)
      ((splits_id_iff_splits _).mpr <| h g monic irred) dvd) <|
        degree_ne_of_natDegree_ne p_irred.natDegree_pos.ne'

Splitting Criterion for Algebraic Closures

Informal description

Let $R$ be an integral domain and $K$ a field extension of $R$ such that: 1. The canonical map $R \to K$ is injective, 2. $K$ is integral over $R$, and 3. Every monic irreducible polynomial $p \in R[X]$ splits completely in $K$ (i.e., factors into linear factors in $K[X]$). Then $K$ is an algebraic closure of $R$.

IsAlgClosed.surjective_restrictDomain_of_isAlgebraic theorem

 {E : Type*} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsAlgebraic L E] :
  Function.Surjective fun φ : E →ₐ[K] M ↦ φ.restrictDomain L

Full source

/-- If E/L/K is a tower of field extensions with E/L algebraic, and if M is an algebraically
  closed extension of K, then any embedding of L/K into M/K extends to an embedding of E/K.
  Known as the extension lemma in https://math.stackexchange.com/a/687914. -/
theorem surjective_restrictDomain_of_isAlgebraic {E : Type*}
    [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsAlgebraic L E] :
    Function.Surjective fun φ : E →ₐ[K] M ↦ φ.restrictDomain L :=
  fun f ↦ IntermediateField.exists_algHom_of_splits'
    (E := E) f fun s ↦ ⟨Algebra.IsIntegral.isIntegral s, IsAlgClosed.splits_codomain _⟩

Extension Lemma for Algebra Homomorphisms in Algebraic Field Extensions

Informal description

Let $K \subseteq L \subseteq E$ be a tower of field extensions where $E$ is algebraic over $L$, and let $M$ be an algebraically closed extension of $K$. Then the restriction map $\varphi \mapsto \varphi|_L$ from $K$-algebra homomorphisms $\varphi \colon E \to M$ to $K$-algebra homomorphisms $L \to M$ is surjective. In other words, every $K$-algebra homomorphism from $L$ to $M$ extends to a $K$-algebra homomorphism from $E$ to $M$.

IsAlgClosed.lift definition

Full source

/-- A (random) homomorphism from an algebraic extension of R into an algebraically
  closed extension of R. -/
@[stacks 09GU]
noncomputable irreducible_def lift : S →ₐ[R] M := by
  letI : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain _
  letI := FractionRing.liftAlgebra R M
  letI := FractionRing.liftAlgebra R (FractionRing S)
  have := FractionRing.isScalarTower_liftAlgebra R M
  have := FractionRing.isScalarTower_liftAlgebra R (FractionRing S)
  let f : FractionRing S →ₐ[FractionRing R] M := lift_aux (FractionRing R) (FractionRing S) M
  exact (f.restrictScalars R).comp ((Algebra.ofId S (FractionRing S)).restrictScalars R)

Lift of an algebraic extension into an algebraically closed extension

Informal description

Given a commutative ring $ R $, an algebraic extension $ S $ of $ R $, and an algebraically closed extension $ M $ of $ R $, there exists a (random) homomorphism $ \text{lift} : S \to M $ of $ R $-algebras. This homomorphism maps elements of $ S $ into $ M $ while preserving the algebraic structure over $ R $.

IsAlgClosed.lift_def theorem

: eta_helper Eq✝ @lift.{} @(delta% @definition✝)

Full source

/-- A (random) homomorphism from an algebraic extension of R into an algebraically
  closed extension of R. -/
@[stacks 09GU]
noncomputable irreducible_def lift : S →ₐ[R] M := by
  letI : IsDomain R := (FaithfulSMul.algebraMap_injective R S).isDomain _
  letI := FractionRing.liftAlgebra R M
  letI := FractionRing.liftAlgebra R (FractionRing S)
  have := FractionRing.isScalarTower_liftAlgebra R M
  have := FractionRing.isScalarTower_liftAlgebra R (FractionRing S)
  let f : FractionRing S →ₐ[FractionRing R] M := lift_aux (FractionRing R) (FractionRing S) M
  exact (f.restrictScalars R).comp ((Algebra.ofId S (FractionRing S)).restrictScalars R)

[Not applicable - internal definition]

Informal description

[This appears to be an internal definition or implementation detail without mathematical content that can be informally stated]

IsAlgClosed.perfectRing instance

(p : ℕ) [Fact p.Prime] [CharP k p] [IsAlgClosed k] : PerfectRing k p

Full source

noncomputable instance (priority := 100) perfectRing (p : ℕ) [Fact p.Prime] [CharP k p]
    [IsAlgClosed k] : PerfectRing k p :=
  PerfectRing.ofSurjective k p fun _ => IsAlgClosed.exists_pow_nat_eq _ <| NeZero.pos p

Algebraically Closed Fields of Positive Characteristic are Perfect Rings

Informal description

For any prime number $p$ and any algebraically closed field $k$ of characteristic $p$, $k$ is a perfect ring. That is, the Frobenius endomorphism $x \mapsto x^p$ is bijective on $k$.

IsAlgClosed.perfectField instance

[IsAlgClosed k] : PerfectField k

Full source

noncomputable instance (priority := 100) perfectField [IsAlgClosed k] : PerfectField k := by
  obtain _ | ⟨p, _, _⟩ := CharP.exists' k
  exacts [.ofCharZero, PerfectRing.toPerfectField k p]

Algebraically Closed Fields are Perfect

Informal description

Every algebraically closed field $k$ is a perfect field.

IsAlgClosed.instInfinite instance

{K : Type*} [Field K] [IsAlgClosed K] : Infinite K

Full source

/-- Algebraically closed fields are infinite since `Xⁿ⁺¹ - 1` is separable when `#K = n` -/
instance (priority := 500) {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
    rw [card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _)]
    unfold f
    rw [← C_1, natDegree_X_pow_sub_C]
  rw [hroot]
  exact Fintype.card_le_of_injective _ Subtype.coe_injective

Algebraically Closed Fields are Infinite

Informal description

Every algebraically closed field $K$ is infinite.

IsAlgClosure.equiv definition

: L ≃ₐ[R] M

Full source

/-- A (random) isomorphism between two algebraic closures of `R`. -/
@[stacks 09GV]
noncomputable def equiv : L ≃ₐ[R] M :=
  AlgEquiv.ofBijective _ (IsAlgClosure.isAlgebraic.algHom_bijective₂
    (IsAlgClosed.lift : L →ₐ[R] M)
    (IsAlgClosed.lift : M →ₐ[R] L)).1

Isomorphism between algebraic closures of a commutative ring

Informal description

Given two algebraic closures $ L $ and $ M $ of a commutative ring $ R $, there exists an $ R $-algebra isomorphism between $ L $ and $ M $.

IsAlgClosure.ofAlgebraic theorem

[Algebra.IsAlgebraic K J] : IsAlgClosure K L

Full source

/-- If `J` is an algebraic extension of `K` and `L` is an algebraic closure of `J`, then it is
  also an algebraic closure of `K`. -/
theorem ofAlgebraic [Algebra.IsAlgebraic K J] : IsAlgClosure K L :=
  ⟨IsAlgClosure.isAlgClosed J, .trans K J L⟩

Algebraic Closure of an Algebraic Extension is Algebraic Closure of Base Field

Informal description

Let $K$ be a field and $J$ an algebraic extension of $K$. If $L$ is an algebraic closure of $J$, then $L$ is also an algebraic closure of $K$.

IsAlgClosure.equivOfAlgebraic' definition

[Nontrivial S] [NoZeroSMulDivisors R S] [Algebra.IsAlgebraic R L] : L ≃ₐ[R] M

Full source

/-- A (random) isomorphism between an algebraic closure of `R` and an algebraic closure of
  an algebraic extension of `R` -/
noncomputable def equivOfAlgebraic' [Nontrivial S] [NoZeroSMulDivisors R S]
    [Algebra.IsAlgebraic R L] : L ≃ₐ[R] M := by
  have : NoZeroSMulDivisors R L := NoZeroSMulDivisors.trans_faithfulSMul R S L
  have : IsAlgClosure R L :=
    { isAlgClosed := IsAlgClosure.isAlgClosed S
      isAlgebraic := ‹_› }
  exact IsAlgClosure.equiv _ _ _

Isomorphism between algebraic extensions of a commutative ring under algebraic conditions

Informal description

Given a commutative ring $R$ and field extensions $L$ and $M$ of $R$ where: 1. $S$ is a nontrivial ring, 2. There are no zero divisors in scalar multiplication between $R$ and $S$, 3. $L$ is algebraic over $R$, then there exists an $R$-algebra isomorphism between $L$ and $M$.

IsAlgClosure.equivOfAlgebraic definition

[Algebra.IsAlgebraic K J] : L ≃ₐ[K] M

Full source

/-- A (random) isomorphism between an algebraic closure of `K` and an algebraic closure
  of an algebraic extension of `K` -/
noncomputable def equivOfAlgebraic [Algebra.IsAlgebraic K J] : L ≃ₐ[K] M :=
  have := Algebra.IsAlgebraic.trans K J L
  equivOfAlgebraic' K J _ _

Isomorphism of algebraic closures over an algebraic extension

Informal description

Given a field extension $ J $ of $ K $ that is algebraic, there exists a $ K $-algebra isomorphism between any two algebraic closures $ L $ and $ M $ of $ J $. This means that if $ J $ is an algebraic extension of $ K $, then any two algebraic closures of $ J $ are isomorphic as $ K $-algebras.

IsAlgClosure.equivOfEquivAux definition

(hSR : S ≃+* R) : { e : L ≃+* M // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom }

Full source

/-- Used in the definition of `equivOfEquiv` -/
noncomputable def equivOfEquivAux (hSR : S ≃+* R) :
    { e : L ≃+* M // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom } := by
  letI : Algebra R S := RingHom.toAlgebra hSR.symm.toRingHom
  letI : Algebra S R := RingHom.toAlgebra hSR.toRingHom
  have : IsDomain S := (FaithfulSMul.algebraMap_injective S L).isDomain _
  letI : Algebra R L := RingHom.toAlgebra ((algebraMap S L).comp (algebraMap R S))
  haveI : IsScalarTower R S L := .of_algebraMap_eq fun _ => rfl
  haveI : IsScalarTower S R L := .of_algebraMap_eq (by simp [RingHom.algebraMap_toAlgebra])
  have : FaithfulSMul R S := (faithfulSMul_iff_algebraMap_injective R S).mpr hSR.symm.injective
  have : Algebra.IsAlgebraic R L := (IsAlgClosure.isAlgebraic.extendScalars
    (show Function.Injective (algebraMap S R) from hSR.injective))
  refine ⟨equivOfAlgebraic' R S L M, ?_⟩
  ext x
  simp only [RingEquiv.toRingHom_eq_coe, Function.comp_apply, RingHom.coe_comp,
    AlgEquiv.coe_ringEquiv, RingEquiv.coe_toRingHom]
  conv_lhs => rw [← hSR.symm_apply_apply x]
  show equivOfAlgebraic' R S L M (algebraMap R L (hSR x)) = _
  rw [AlgEquiv.commutes]

Existence of compatible isomorphism between algebraic closures under base ring isomorphism

Informal description

Given a commutative ring isomorphism $h_{SR} : S \simeq R$, there exists a ring isomorphism $e : L \simeq M$ such that the diagram \[ \begin{tikzcd} S \arrow{r}{h_{SR}} \arrow{d}[swap]{\text{algebraMap } S L} & R \arrow{d}{\text{algebraMap } R M} \\ L \arrow{r}[swap]{e} & M \end{tikzcd} \] commutes. Here $L$ and $M$ are algebraic closures of $S$ and $R$ respectively, and the vertical maps are the canonical algebra homomorphisms.

IsAlgClosure.equivOfEquiv definition

(hSR : S ≃+* R) : L ≃+* M

Full source

/-- Algebraic closure of isomorphic fields are isomorphic -/
noncomputable def equivOfEquiv (hSR : S ≃+* R) : L ≃+* M :=
  equivOfEquivAux L M hSR

Isomorphism of algebraic closures induced by base ring isomorphism

Informal description

Given a ring isomorphism $ h_{SR} : S \simeq R $, there exists a ring isomorphism $ L \simeq M $ between the algebraic closures $ L $ of $ S $ and $ M $ of $ R $, such that the following diagram commutes: \[ \begin{tikzcd} S \arrow{r}{h_{SR}} \arrow{d}[swap]{\text{algebraMap } S L} & R \arrow{d}{\text{algebraMap } R M} \\ L \arrow{r}[swap]{\simeq} & M \end{tikzcd} \] Here, the vertical maps are the canonical algebra homomorphisms.

IsAlgClosure.equivOfEquiv_comp_algebraMap theorem

(hSR : S ≃+* R) : (↑(equivOfEquiv L M hSR) : L →+* M).comp (algebraMap S L) = (algebraMap R M).comp hSR

Full source

@[simp]
theorem equivOfEquiv_comp_algebraMap (hSR : S ≃+* R) :
    (↑(equivOfEquiv L M hSR) : L →+* M).comp (algebraMap S L) = (algebraMap R M).comp hSR :=
  (equivOfEquivAux L M hSR).2

Compatibility of algebraic closure isomorphism with base ring homomorphism

Informal description

Given a ring isomorphism $h_{SR} \colon S \simeq R$, the ring homomorphism $\text{equivOfEquiv}\, L\, M\, h_{SR} \colon L \to M$ obtained from the isomorphism of algebraic closures satisfies the commutative diagram: \[ \text{equivOfEquiv}\, L\, M\, h_{SR} \circ \text{algebraMap}\, S\, L = \text{algebraMap}\, R\, M \circ h_{SR}. \] Here, $L$ and $M$ are algebraic closures of $S$ and $R$ respectively, and $\text{algebraMap}$ denotes the canonical embedding of the base ring into its algebraic closure.

IsAlgClosure.equivOfEquiv_algebraMap theorem

(hSR : S ≃+* R) (s : S) : equivOfEquiv L M hSR (algebraMap S L s) = algebraMap R M (hSR s)

Full source

@[simp]
theorem equivOfEquiv_algebraMap (hSR : S ≃+* R) (s : S) :
    equivOfEquiv L M hSR (algebraMap S L s) = algebraMap R M (hSR s) :=
  RingHom.ext_iff.1 (equivOfEquiv_comp_algebraMap L M hSR) s

Commutativity of Algebraic Closure Isomorphism with Base Ring Embedding

Informal description

Given a ring isomorphism $h_{SR} \colon S \simeq R$ and an element $s \in S$, the image of $s$ under the algebraic closure isomorphism $\text{equivOfEquiv}\, L\, M\, h_{SR} \colon L \to M$ is equal to the image of $h_{SR}(s)$ under the canonical embedding $\text{algebraMap}\, R\, M$. In other words, the following diagram commutes for any $s \in S$: \[ \text{equivOfEquiv}\, L\, M\, h_{SR} (\text{algebraMap}\, S\, L\, s) = \text{algebraMap}\, R\, M\, (h_{SR}(s)). \] Here, $L$ and $M$ are algebraic closures of $S$ and $R$ respectively, and $\text{algebraMap}$ denotes the canonical embedding of the base ring into its algebraic closure.

IsAlgClosure.equivOfEquiv_symm_algebraMap theorem

(hSR : S ≃+* R) (r : R) : (equivOfEquiv L M hSR).symm (algebraMap R M r) = algebraMap S L (hSR.symm r)

Full source

@[simp]
theorem equivOfEquiv_symm_algebraMap (hSR : S ≃+* R) (r : R) :
    (equivOfEquiv L M hSR).symm (algebraMap R M r) = algebraMap S L (hSR.symm r) :=
  (equivOfEquiv L M hSR).injective (by simp)

Commutativity of Inverse Algebraic Closure Isomorphism with Base Ring Embedding

Informal description

Given a ring isomorphism $h_{SR} \colon S \simeq R$ and an element $r \in R$, the inverse of the algebraic closure isomorphism $\text{equivOfEquiv}\, L\, M\, h_{SR}$ maps the image of $r$ under the canonical embedding $\text{algebraMap}\, R\, M$ to the image of $h_{SR}^{-1}(r)$ under the canonical embedding $\text{algebraMap}\, S\, L$. In other words, the following holds: \[ (\text{equivOfEquiv}\, L\, M\, h_{SR})^{-1}(\text{algebraMap}\, R\, M\, r) = \text{algebraMap}\, S\, L\, (h_{SR}^{-1}(r)). \] Here, $L$ and $M$ are algebraic closures of $S$ and $R$ respectively, and $\text{algebraMap}$ denotes the canonical embedding of the base ring into its algebraic closure.

IsAlgClosure.equivOfEquiv_symm_comp_algebraMap theorem

(hSR : S ≃+* R) : ((equivOfEquiv L M hSR).symm : M →+* L).comp (algebraMap R M) = (algebraMap S L).comp hSR.symm

Full source

@[simp]
theorem equivOfEquiv_symm_comp_algebraMap (hSR : S ≃+* R) :
    ((equivOfEquiv L M hSR).symm : M →+* L).comp (algebraMap R M) =
      (algebraMap S L).comp hSR.symm :=
  RingHom.ext_iff.2 (equivOfEquiv_symm_algebraMap L M hSR)

Commutative Diagram for Inverse Algebraic Closure Isomorphism and Base Ring Embeddings

Informal description

Given a ring isomorphism $h_{SR} \colon S \simeq R$, the composition of the inverse of the algebraic closure isomorphism $\text{equivOfEquiv}\, L\, M\, h_{SR} \colon M \to L$ with the canonical embedding $\text{algebraMap}\, R\, M$ is equal to the composition of the canonical embedding $\text{algebraMap}\, S\, L$ with the inverse isomorphism $h_{SR}^{-1} \colon R \to S$. In other words, the following diagram commutes: \[ (\text{equivOfEquiv}\, L\, M\, h_{SR})^{-1} \circ \text{algebraMap}\, R\, M = \text{algebraMap}\, S\, L \circ h_{SR}^{-1}. \] Here, $L$ and $M$ are algebraic closures of $S$ and $R$ respectively, and $\text{algebraMap}$ denotes the canonical embedding of the base ring into its algebraic closure.

Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly theorem

[IsAlgClosed A] (x : K) : (Set.range fun ψ : K →ₐ[F] A ↦ ψ x) = (minpoly F x).rootSet A

Full source

/-- Let `A` be an algebraically closed field and let `x ∈ K`, with `K/F` an algebraic extension
  of fields. Then the images of `x` by the `F`-algebra morphisms from `K` to `A` are exactly
  the roots in `A` of the minimal polynomial of `x` over `F`. -/
theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly [IsAlgClosed A] (x : K) :
    (Set.range fun ψ : K →ₐ[F] A ↦ ψ x) = (minpoly F x).rootSet A :=
  range_eval_eq_rootSet_minpoly_of_splits A (fun _ ↦ IsAlgClosed.splits_codomain _) x

Image of Algebraic Element under Homomorphisms Equals Roots of Minimal Polynomial

Informal description

Let $A$ be an algebraically closed field and $K/F$ be an algebraic field extension. For any element $x \in K$, the set of images of $x$ under all $F$-algebra homomorphisms $\psi \colon K \to A$ is equal to the set of roots in $A$ of the minimal polynomial of $x$ over $F$. That is, \[ \{\psi(x) \mid \psi \colon K \to A \text{ is an } F\text{-algebra homomorphism}\} = \{a \in A \mid \text{minpoly}_F(x)(a) = 0\}. \]

IntermediateField.algHomEquivAlgHomOfSplits definition

 (L : IntermediateField F A) (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) : (K →ₐ[F] L) ≃ (K →ₐ[F] A)

Full source

/-- All `F`-embeddings of a field `K` into another field `A` factor through any intermediate
field of `A/F` in which the minimal polynomial of elements of `K` splits. -/
@[simps]
def IntermediateField.algHomEquivAlgHomOfSplits (L : IntermediateField F A)
    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) :
    (K →ₐ[F] L) ≃ (K →ₐ[F] A) where
  toFun := L.val.comp
  invFun f := f.codRestrict _ fun x ↦
    ((Algebra.IsIntegral.isIntegral x).map f).mem_intermediateField_of_minpoly_splits <| by
      rw [minpoly.algHom_eq f f.injective]; exact hL x
  left_inv _ := rfl
  right_inv _ := by rfl

Equivalence of Algebra Homomorphisms via Intermediate Field with Splitting Condition

Informal description

Given an intermediate field $ L $ between fields $ F $ and $ A $, and a condition that for every element $ x \in K $, the minimal polynomial of $ x $ over $ F $ splits in $ L $, there exists an equivalence between the set of $ F $-algebra homomorphisms from $ K $ to $ L $ and the set of $ F $-algebra homomorphisms from $ K $ to $ A $. More precisely, the equivalence is constructed as follows: - The forward map is given by composing any $ F $-algebra homomorphism $ K \to L $ with the inclusion $ L \hookrightarrow A $. - The inverse map restricts any $ F $-algebra homomorphism $ K \to A $ to $ L $, ensuring that the image lies in $ L $ by verifying that the minimal polynomial of each $ x \in K $ splits in $ L $.

IntermediateField.algHomEquivAlgHomOfSplits_apply_apply theorem

 (L : IntermediateField F A) (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
  algHomEquivAlgHomOfSplits A L hL f x = algebraMap L A (f x)

Full source

theorem IntermediateField.algHomEquivAlgHomOfSplits_apply_apply (L : IntermediateField F A)
    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
    algHomEquivAlgHomOfSplits A L hL f x = algebraMap L A (f x) := rfl

Evaluation of Algebra Homomorphism Equivalence via Splitting Condition

Informal description

Let $F$, $K$, $A$ be fields with $K/F$ and $A/F$ field extensions, and let $L$ be an intermediate field between $F$ and $A$. Suppose that for every $x \in K$, the minimal polynomial of $x$ over $F$ splits in $L$. Then for any $F$-algebra homomorphism $f \colon K \to L$ and any $x \in K$, the evaluation of the equivalence map $\text{algHomEquivAlgHomOfSplits}$ at $f$ and $x$ is equal to the image of $f(x)$ under the canonical inclusion $L \hookrightarrow A$. That is, \[ \text{algHomEquivAlgHomOfSplits}(f)(x) = \iota(f(x)) \] where $\iota \colon L \to A$ is the inclusion map.

Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits definition

 (L : Type*) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A]
  (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) : (K →ₐ[F] L) ≃ (K →ₐ[F] A)

Full source

/-- All `F`-embeddings of a field `K` into another field `A` factor through any subextension
of `A/F` in which the minimal polynomial of elements of `K` splits. -/
noncomputable def Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits (L : Type*) [Field L]
    [Algebra F L] [Algebra L A] [IsScalarTower F L A]
    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) :
    (K →ₐ[F] L) ≃ (K →ₐ[F] A) :=
  (AlgEquiv.refl.arrowCongr (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L A))).trans <|
    IntermediateField.algHomEquivAlgHomOfSplits A (IsScalarTower.toAlgHom F L A).fieldRange
    fun x ↦ splits_of_algHom (hL x) (AlgHom.rangeRestrict _)

Equivalence of algebra homomorphisms via splitting intermediate field

Informal description

Given a field extension $ K / F $ that is algebraic, and another field $ L $ with $ F $-algebra structures $ F \to L \to A $ forming a scalar tower, if for every $ x \in K $ the minimal polynomial of $ x $ over $ F $ splits in $ L $, then there is an equivalence between the set of $ F $-algebra homomorphisms from $ K $ to $ L $ and the set of $ F $-algebra homomorphisms from $ K $ to $ A $.

Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply theorem

 (L : Type*) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A]
  (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
  Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits A L hL f x = algebraMap L A (f x)

Full source

theorem Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply (L : Type*) [Field L]
    [Algebra F L] [Algebra L A] [IsScalarTower F L A]
    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
    Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits A L hL f x = algebraMap L A (f x) := rfl

Evaluation of Algebra Homomorphism Equivalence via Splitting Condition

Informal description

Let $K/F$ be an algebraic field extension, and let $L$ be a field with $F$-algebra structures forming a scalar tower $F \to L \to A$. Suppose that for every $x \in K$, the minimal polynomial of $x$ over $F$ splits in $L$. Then for any $F$-algebra homomorphism $f \colon K \to L$ and any $x \in K$, the evaluation of the equivalence map $\text{algHomEquivAlgHomOfSplits}$ at $f$ and $x$ is given by the composition of $f$ with the canonical inclusion $L \hookrightarrow A$, i.e., \[ \text{algHomEquivAlgHomOfSplits}(f)(x) = \iota(f(x)) \] where $\iota \colon L \to A$ is the inclusion map.

Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul theorem

 {K : Type*} [Field K] [IsAlgClosed K] [CharZero K] {f g : K[X]} (hf0 : f ≠ 0) :
  (∀ x, IsRoot f x → IsRoot g x) ↔ f ∣ f.derivative * g

Full source

/-- Over an algebraically closed field of characteristic zero a necessary and sufficient condition
for the set of roots of a nonzero polynomial `f` to be a subset of the set of roots of `g` is that
`f` divides `f.derivative * g`. Over an integral domain, this is a sufficient but not necessary
condition. See `isRoot_of_isRoot_of_dvd_derivative_mul` -/
theorem Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul {K : Type*} [Field K]
    [IsAlgClosed K] [CharZero K] {f g : K[X]} (hf0 : f ≠ 0) :
    (∀ x, IsRoot f x → IsRoot g x) ↔ f ∣ f.derivative * g := by
  refine ⟨?_, isRoot_of_isRoot_of_dvd_derivative_mul hf0⟩
  by_cases hg0 : g = 0
  · simp [hg0]
  by_cases hdf0 : derivative f = 0
  · rw [eq_C_of_derivative_eq_zero hdf0]
    simp only [eval_C, derivative_C, zero_mul, dvd_zero, implies_true]
  have hdg :  f.derivative * g ≠ 0 := mul_ne_zero hdf0 hg0
  classical rw [Splits.dvd_iff_roots_le_roots (IsAlgClosed.splits f) hf0 hdg, Multiset.le_iff_count]
  simp only [count_roots, rootMultiplicity_mul hdg]
  refine forall_imp fun a => ?_
  by_cases haf : f.eval a = 0
  · have h0 : 0 < f.rootMultiplicity a := (rootMultiplicity_pos hf0).2 haf
    rw [derivative_rootMultiplicity_of_root haf]
    intro h
    calc rootMultiplicity a f
        = rootMultiplicity a f - 1 + 1 := (Nat.sub_add_cancel (Nat.succ_le_iff.1 h0)).symm
      _ ≤ rootMultiplicity a f - 1 + rootMultiplicity a g := add_le_add le_rfl (Nat.succ_le_iff.1
        ((rootMultiplicity_pos hg0).2 (h haf)))
  · simp [haf, rootMultiplicity_eq_zero haf]

Root Inclusion Criterion for Polynomials over Algebraically Closed Fields: $f \mid f' g \iff \text{roots}(f) \subseteq \text{roots}(g)$

Informal description

Let $K$ be an algebraically closed field of characteristic zero, and let $f, g \in K[X]$ be polynomials with $f \neq 0$. Then the following are equivalent: 1. Every root of $f$ is also a root of $g$. 2. The polynomial $f$ divides the product $f' \cdot g$, where $f'$ is the derivative of $f$.

Mathlib.FieldTheory.IsAlgClosed.Basic

Main Definitions

Tags

Main results