Algebraically Closed Field

In this file we define the typeclass for algebraically closed fields and algebraic closures, and prove some of their properties.

Main Definitions

• IsAlgClosed k is the typeclass saying k is an algebraically closed field, i.e. every polynomial in k splits.

• IsAlgClosure R K is the typeclass saying K is an algebraic closure of R, where R is a commutative ring. This means that the map from R to K is injective, and K is algebraically closed and algebraic over R

• IsAlgClosed.lift is a map from an algebraic extension L of R, into any algebraically closed extension of R.

• IsAlgClosure.equiv is a proof that any two algebraic closures of the same field are isomorphic.

Tags

algebraic closure, algebraically closed

Main results

• IsAlgClosure.of_splits: if K / k is algebraic, and every monic irreducible polynomial over k splits in K, then K is algebraically closed (in fact an algebraic closure of k). For the stronger fact that only requires every such polynomial has a root in K, see IsAlgClosure.of_exists_root.

  Reference: https://kconrad.math.uconn.edu/blurbs/galoistheory/algclosure.pdf, Theorem 2

class IsAlgClosed (k : Type u) [Field k] : Prop

An algebraically closed field is one where every polynomial splits. Equivalently, all non-constant polynomials have a root. See IsAlgClosed.exists_root and IsAlgClosed.of_exists_root.

• splits (p : Polynomial k) : p.Splits

@[deprecated IsAlgClosed.splits (since := "2025-12-09")]

theorem IsAlgClosed.factors {k : Type u} {inst✝ : Field k} [self : IsAlgClosed k] (p : Polynomial k) : p.Splits

Alias of IsAlgClosed.splits.

@[deprecated "This is a special case of `IsAlgClosed.splits`." (since := "2025-12-09")]

theorem IsAlgClosed.splits_codomain {k : Type u_1} {K : Type u_2} [Field k] [IsAlgClosed k] [CommRing K] {f : K →+* k} (p : Polynomial K) : (Polynomial.map f p).Splits

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_domain {k : Type u_1} {K : Type u_2} [Field k] [IsAlgClosed k] [Field K] {f : k →+* K} (p : Polynomial k) : (Polynomial.map f p).Splits

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

theorem IsAlgClosed.exists_root {k : Type u} [Field k] [IsAlgClosed k] (p : Polynomial k) (hp : p.degree ≠ 0) : ∃ (x : k), p.IsRoot x

If k is algebraically closed, then every nonconstant polynomial has a root.

theorem IsAlgClosed.exists_pow_nat_eq {k : Type u} [Field k] [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ (z : k), z ^ n = x

theorem IsAlgClosed.exists_eq_mul_self {k : Type u} [Field k] [IsAlgClosed k] (x : k) : ∃ (z : k), x = z * z

theorem IsAlgClosed.roots_eq_zero_iff {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)

theorem IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots = 0 ↔ p.natDegree = 0

theorem IsAlgClosed.roots_eq_zero_iff_degree_nonpos {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots = 0 ↔ p.degree ≤ 0

theorem IsAlgClosed.card_roots_eq_natDegree {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} : p.roots.card = p.natDegree

theorem IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero {A : Type u_1} {B : Type u_2} [Semiring A] [Field B] [IsAlgClosed B] {f : A →+* B} {p : Polynomial A} (hf : f p.leadingCoeff ≠ 0) : (Polynomial.map f p).roots.card = p.natDegree

theorem IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff {A : Type u_1} {B : Type u_2} [Semiring A] [Field B] [IsAlgClosed B] (f : A →+* B) {p : Polynomial A} (h : IsUnit p.leadingCoeff) : (Polynomial.map f p).roots.card = p.natDegree

theorem IsAlgClosed.card_roots_map_eq_natDegree_of_injective {A : Type u_1} {B : Type u_2} [Semiring A] [Field B] [IsAlgClosed B] {f : A →+* B} (p : Polynomial A) (hf : Function.Injective ⇑f) : (Polynomial.map f p).roots.card = p.natDegree

theorem IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing {A : Type u_1} {B : Type u_2} [Ring A] [IsSimpleRing A] [Field B] [IsAlgClosed B] (f : A →+* B) (p : Polynomial A) : (Polynomial.map f p).roots.card = p.natDegree

theorem IsAlgClosed.card_aroots_eq_natDegree_of_leadingCoeff_ne_zero {A : Type u_1} {B : Type u_2} [CommRing A] [Field B] [IsAlgClosed B] [Algebra A B] {p : Polynomial A} (hf : (algebraMap A B) p.leadingCoeff ≠ 0) : (p.aroots B).card = p.natDegree

theorem IsAlgClosed.card_aroots_eq_natDegree_of_isUnit_leadingCoeff {A : Type u_1} {B : Type u_2} [CommRing A] [Field B] [IsAlgClosed B] [Algebra A B] {p : Polynomial A} (h : IsUnit p.leadingCoeff) : (p.aroots B).card = p.natDegree

theorem IsAlgClosed.card_aroots_eq_natDegree {A : Type u_1} {B : Type u_2} [CommRing A] [Field B] [IsAlgClosed B] [Algebra A B] [FaithfulSMul A B] {p : Polynomial A} : (p.aroots B).card = p.natDegree

theorem IsAlgClosed.dvd_iff_roots_le_roots {k : Type u} [Field k] [IsAlgClosed k] {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) : p ∣ q ↔ p.roots ≤ q.roots

theorem IsAlgClosed.associated_iff_roots_eq_roots {k : Type u} [Field k] [IsAlgClosed k] {p q : Polynomial k} (hp : p ≠ 0) (hq : q ≠ 0) : Associated p q ↔ p.roots = q.roots

theorem IsAlgClosed.exists_eval₂_eq_zero_of_injective {k : Type u} [Field k] {R : Type u_1} [Semiring R] [IsAlgClosed k] (f : R →+* k) (hf : Function.Injective ⇑f) (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ (x : k), Polynomial.eval₂ f x p = 0

theorem IsAlgClosed.exists_eval₂_eq_zero {k : Type u} [Field k] {R : Type u_1} [Ring R] [IsSimpleRing R] [IsAlgClosed k] (f : R →+* k) (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ (x : k), Polynomial.eval₂ f x p = 0

theorem IsAlgClosed.exists_aeval_eq_zero_of_injective (k : Type u) [Field k] {R : Type u_1} [CommSemiring R] [IsAlgClosed k] [Algebra R k] (hinj : Function.Injective ⇑(algebraMap R k)) (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ (x : k), (Polynomial.aeval x) p = 0

theorem IsAlgClosed.exists_aeval_eq_zero (k : Type u) [Field k] {R : Type u_1} [CommSemiring R] [IsAlgClosed k] [Algebra R k] [FaithfulSMul R k] (p : Polynomial R) (hp : p.degree ≠ 0) : ∃ (x : k), (Polynomial.aeval x) p = 0

theorem IsAlgClosed.of_exists_root (k : Type u) [Field k] (H : ∀ (p : Polynomial k), p.Monic → Irreducible p → ∃ (x : k), Polynomial.eval x p = 0) : IsAlgClosed k

If every nonconstant polynomial over k has a root, then k is algebraically closed.

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

theorem IsAlgClosed.degree_eq_one_of_irreducible (k : Type u) [Field k] [IsAlgClosed k] {p : Polynomial k} (hp : Irreducible p) : p.degree = 1

If k is algebraically closed, then every irreducible polynomial over k is linear.

theorem IsAlgClosed.algebraMap_bijective_of_isIntegral {k : Type u_1} {K : Type u_2} [Field k] [Ring K] [IsDomain K] [hk : IsAlgClosed k] [Algebra k K] [Algebra.IsIntegral k K] : Function.Bijective ⇑(algebraMap k K)

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

theorem IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic {k : Type u_1} {K : Type u_2} [Field k] [Field K] [IsAlgClosed k] [Algebra k K] (L : IntermediateField k K) [Algebra.IsAlgebraic k ↥L] : L = ⊥

If k is algebraically closed, K / k is a field extension, L / k is an intermediate field which is algebraic, then L is equal to k. A corollary of IsAlgClosed.algebraMap_surjective_of_isAlgebraic.

theorem Polynomial.isCoprime_iff_aeval_ne_zero_of_isAlgClosed (k : Type u) [Field k] (K : Type v) [Field K] [IsAlgClosed K] [Algebra k K] (p q : Polynomial k) : IsCoprime p q ↔ ∀ (a : K), (aeval a) p ≠ 0 ∨ (aeval a) q ≠ 0

class IsAlgClosure (R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K] [Module.IsTorsionFree R K] : Prop

Typeclass for an extension being an algebraic closure.

• isAlgClosed : IsAlgClosed K
• isAlgebraic : Algebra.IsAlgebraic R K

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

@[instance 100]

instance IsAlgClosure.normal (R : Type u_1) (K : Type u_2) [Field R] [Field K] [Algebra R K] [IsAlgClosure R K] : Normal R K

@[instance 100]

instance IsAlgClosure.separable (R : Type u_1) (K : Type u_2) [Field R] [Field K] [Algebra R K] [IsAlgClosure R K] [CharZero R] : Algebra.IsSeparable R K

instance IsAlgClosed.instIsAlgClosure (F : Type u_1) [Field F] [IsAlgClosed F] : IsAlgClosure F F

theorem IsAlgClosure.of_splits {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [Algebra.IsIntegral R K] [Module.IsTorsionFree R K] (h : ∀ (p : Polynomial R), p.Monic → Irreducible p → (Polynomial.map (algebraMap R K) p).Splits) : IsAlgClosure R K

theorem IsAlgClosed.eval_surjective {M : Type w} [Field M] [IsAlgClosed M] {p : Polynomial M} (hp : p.natDegree ≠ 0) : Function.Surjective fun (x : M) => Polynomial.eval x p

theorem IsAlgClosed.surjective_restrictDomain_of_isAlgebraic {K : Type u} [Field K] {L : Type v} {M : Type w} [Field L] [Algebra K L] [Field M] [Algebra K M] [IsAlgClosed M] {E : Type u_1} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsAlgebraic L E] : Function.Surjective fun (φ : E →ₐ[K] M) => AlgHom.restrictDomain L φ

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.

noncomputable def IsAlgClosed.lift {M : Type w} [Field M] [IsAlgClosed M] {R : Type u} [CommRing R] [IsDomain R] {S : Type v} [CommRing S] [IsDomain S] [Algebra R S] [Algebra R M] [Module.IsTorsionFree R S] [Module.IsTorsionFree R M] [Algebra.IsAlgebraic R S] : S →ₐ[R] M

A (random) homomorphism from an algebraic extension of R into an algebraically closed extension of R.

theorem IsAlgClosed.nonempty_algEquiv_or_of_finrank_eq_two {F : Type u_1} {F' : Type u_2} (E : Type u_3) [Field F] [Field F'] [Field E] [Algebra F F'] [Algebra F E] [Algebra.IsAlgebraic F E] [IsAlgClosed F'] (h : Module.finrank F F' = 2) : Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

@[instance 100]

instance IsAlgClosed.perfectRing (k : Type u) [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] [IsAlgClosed k] : PerfectRing k p

@[instance 100]

instance IsAlgClosed.perfectField (k : Type u) [Field k] [IsAlgClosed k] : PerfectField k

@[instance 500]

instance IsAlgClosed.instInfinite {K : Type u_1} [Field K] [IsAlgClosed K] : Infinite K

Algebraically closed fields are infinite since Xⁿ⁺¹ - 1 is separable when #K = n

noncomputable def IsAlgClosure.equiv (R : Type u) [CommRing R] [IsDomain R] (L : Type v) (M : Type w) [Field L] [Field M] [Algebra R M] [Module.IsTorsionFree R M] [IsAlgClosure R M] [Algebra R L] [Module.IsTorsionFree R L] [IsAlgClosure R L] : L ≃ₐ[R] M

A (random) isomorphism between two algebraic closures of R.

theorem IsAlgClosure.ofAlgebraic (K : Type u_1) (J : Type u_2) (L : Type v) [Field K] [Field J] [Field L] [Algebra K J] [Algebra J L] [IsAlgClosure J L] [Algebra K L] [IsScalarTower K J L] [Algebra.IsAlgebraic K J] : IsAlgClosure K L

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.

noncomputable def IsAlgClosure.equivOfAlgebraic' (R : Type u) (S : Type u_3) (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [Module.IsTorsionFree R M] [IsAlgClosure R M] [Algebra S L] [Module.IsTorsionFree S L] [IsAlgClosure S L] [Algebra R S] [Algebra R L] [IsScalarTower R S L] [IsDomain R] [IsDomain S] [Module.IsTorsionFree R S] [Algebra.IsAlgebraic R L] : L ≃ₐ[R] M

A (random) isomorphism between an algebraic closure of R and an algebraic closure of an algebraic extension of R

noncomputable def IsAlgClosure.equivOfAlgebraic (K : Type u_1) (J : Type u_2) (L : Type v) (M : Type w) [Field K] [Field J] [Field L] [Field M] [Algebra K M] [IsAlgClosure K M] [Algebra K J] [Algebra J L] [IsAlgClosure J L] [Algebra K L] [IsScalarTower K J L] [Algebra.IsAlgebraic K J] : L ≃ₐ[K] M

A (random) isomorphism between an algebraic closure of K and an algebraic closure of an algebraic extension of K

noncomputable def IsAlgClosure.equivOfEquivAux {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [Module.IsTorsionFree R M] [IsAlgClosure R M] [Algebra S L] [Module.IsTorsionFree S L] [IsAlgClosure S L] [IsDomain R] [IsDomain S] (hSR : S ≃+* R) : { e : L ≃+* M // e.toRingHom.comp (algebraMap S L) = (algebraMap R M).comp hSR.toRingHom }

Used in the definition of equivOfEquiv

noncomputable def IsAlgClosure.equivOfEquiv {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [Module.IsTorsionFree R M] [IsAlgClosure R M] [Algebra S L] [Module.IsTorsionFree S L] [IsAlgClosure S L] [IsDomain R] [IsDomain S] (hSR : S ≃+* R) : L ≃+* M

Algebraic closure of isomorphic fields are isomorphic

@[simp]

theorem IsAlgClosure.equivOfEquiv_comp_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [Module.IsTorsionFree R M] [IsAlgClosure R M] [Algebra S L] [Module.IsTorsionFree S L] [IsAlgClosure S L] [IsDomain R] [IsDomain S] (hSR : S ≃+* R) : (↑(equivOfEquiv L M hSR)).comp (algebraMap S L) = (algebraMap R M).comp ↑hSR

@[simp]

theorem IsAlgClosure.equivOfEquiv_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [Module.IsTorsionFree R M] [IsAlgClosure R M] [Algebra S L] [Module.IsTorsionFree S L] [IsAlgClosure S L] [IsDomain R] [IsDomain S] (hSR : S ≃+* R) (s : S) : (equivOfEquiv L M hSR) ((algebraMap S L) s) = (algebraMap R M) (hSR s)

@[simp]

theorem IsAlgClosure.equivOfEquiv_symm_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [Module.IsTorsionFree R M] [IsAlgClosure R M] [Algebra S L] [Module.IsTorsionFree S L] [IsAlgClosure S L] [IsDomain R] [IsDomain S] (hSR : S ≃+* R) (r : R) : (equivOfEquiv L M hSR).symm ((algebraMap R M) r) = (algebraMap S L) (hSR.symm r)

@[simp]

theorem IsAlgClosure.equivOfEquiv_symm_comp_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [Module.IsTorsionFree R M] [IsAlgClosure R M] [Algebra S L] [Module.IsTorsionFree S L] [IsAlgClosure S L] [IsDomain R] [IsDomain S] (hSR : S ≃+* R) : (↑(equivOfEquiv L M hSR).symm).comp (algebraMap R M) = (algebraMap S L).comp ↑hSR.symm

theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] [IsAlgClosed A] (x : K) : (Set.range fun (ψ : K →ₐ[F] A) => ψ x) = (minpoly F x).rootSet A

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.

def IntermediateField.algHomEquivAlgHomOfSplits {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : IntermediateField F A) (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) : (K →ₐ[F] ↥L) ≃ (K →ₐ[F] A)

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.

@[simp]

theorem IntermediateField.algHomEquivAlgHomOfSplits_symm_apply {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : IntermediateField F A) (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (f : K →ₐ[F] A) : (algHomEquivAlgHomOfSplits A L hL).symm f = f.codRestrict L.toSubalgebra ⋯

@[simp]

theorem IntermediateField.algHomEquivAlgHomOfSplits_apply {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : IntermediateField F A) (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (φ₂ : K →ₐ[F] ↥L) : (algHomEquivAlgHomOfSplits A L hL) φ₂ = L.val.comp φ₂

theorem IntermediateField.algHomEquivAlgHomOfSplits_apply_apply {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : IntermediateField F A) (hL : ∀ (x : K), (Polynomial.map (algebraMap F ↥L) (minpoly F x)).Splits) (f : K →ₐ[F] ↥L) (x : K) : ((algHomEquivAlgHomOfSplits A L hL) f) x = (algebraMap (↥L) A) (f x)

noncomputable def Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : Type u_4) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A] (hL : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) : (K →ₐ[F] L) ≃ (K →ₐ[F] A)

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.

theorem Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits_apply_apply {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [Algebra F K] [Algebra F A] [Algebra.IsAlgebraic F K] (L : Type u_4) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A] (hL : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) (f : K →ₐ[F] L) (x : K) : ((algHomEquivAlgHomOfSplits A L hL) f) x = (algebraMap L A) (f x)

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

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