# Documentation

Mathlib.FieldTheory.IsAlgClosed.Basic

# 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

class IsAlgClosed (k : Type u) [] :
• splits : ∀ (p : ),

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.

Instances
theorem IsAlgClosed.splits_codomain {k : Type u_1} {K : Type u_2} [] [] [] {f : K →+* k} (p : ) :

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} [] [] [] {f : k →+* K} (p : ) :

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.exists_root {k : Type u} [] [] (p : ) (hp : ) :
x,
theorem IsAlgClosed.exists_pow_nat_eq {k : Type u} [] [] (x : k) {n : } (hn : 0 < n) :
z, z ^ n = x
theorem IsAlgClosed.exists_eq_mul_self {k : Type u} [] [] (x : k) :
z, x = z * z
theorem IsAlgClosed.roots_eq_zero_iff {k : Type u} [] [] {p : } :
p = Polynomial.C ()
theorem IsAlgClosed.exists_eval₂_eq_zero_of_injective {k : Type u} [] {R : Type u_1} [Ring R] [] (f : R →+* k) (hf : ) (p : ) (hp : ) :
x, = 0
theorem IsAlgClosed.exists_eval₂_eq_zero {k : Type u} [] {R : Type u_1} [] [] (f : R →+* k) (p : ) (hp : ) :
x, = 0
theorem IsAlgClosed.exists_aeval_eq_zero_of_injective (k : Type u) [] {R : Type u_1} [] [] [Algebra R k] (hinj : Function.Injective ↑()) (p : ) (hp : ) :
x, ↑() p = 0
theorem IsAlgClosed.exists_aeval_eq_zero (k : Type u) [] {R : Type u_1} [] [] [Algebra R k] (p : ) (hp : ) :
x, ↑() p = 0
theorem IsAlgClosed.of_exists_root (k : Type u) [] (H : ∀ (p : ), x, = 0) :
theorem IsAlgClosed.of_ringEquiv (k : Type u) [] (k' : Type u) [Field k'] (e : k ≃+* k') [] :
theorem IsAlgClosed.degree_eq_one_of_irreducible (k : Type u) [] [] {p : } (hp : ) :
theorem IsAlgClosed.algebraMap_surjective_of_isIntegral {k : Type u_1} {K : Type u_2} [] [Ring K] [] [hk : ] [Algebra k K] (hf : ) :
theorem IsAlgClosed.algebraMap_surjective_of_isIntegral' {k : Type u_1} {K : Type u_2} [] [] [] [] (f : k →+* K) (hf : ) :
theorem IsAlgClosed.algebraMap_surjective_of_isAlgebraic {k : Type u_1} {K : Type u_2} [] [Ring K] [] [] [Algebra k K] (hf : ) :
class IsAlgClosure (R : Type u) (K : Type v) [] [] [Algebra R K] [] :
• alg_closed :
• algebraic :

Typeclass for an extension being an algebraic closure.

Instances
theorem isAlgClosure_iff (k : Type u) [] (K : Type v) [] [Algebra k K] :
instance IsAlgClosure.normal (R : Type u_1) (K : Type u_2) [] [] [Algebra R K] [] :
Normal R K
instance IsAlgClosure.separable (R : Type u_1) (K : Type u_2) [] [] [Algebra R K] [] [] :
structure IsAlgClosed.lift.SubfieldWithHom (K : Type u) (L : Type v) (M : Type w) [] [] [Algebra K L] [] [Algebra K M] :
Type (max v w)
• carrier :

The corresponding Subalgebra

• emb : { x // x s.carrier } →ₐ[K] M

The embedding into the algebraically closed field

This structure is used to prove the existence of a homomorphism from any algebraic extension into an algebraic closure

Instances For
instance IsAlgClosed.lift.SubfieldWithHom.instLESubfieldWithHom {K : Type u} {L : Type v} {M : Type w} [] [] [Algebra K L] [] [Algebra K M] :
noncomputable instance IsAlgClosed.lift.SubfieldWithHom.instInhabitedSubfieldWithHom {K : Type u} {L : Type v} {M : Type w} [] [] [Algebra K L] [] [Algebra K M] :
theorem IsAlgClosed.lift.SubfieldWithHom.le_def {K : Type u} {L : Type v} {M : Type w} [] [] [Algebra K L] [] [Algebra K M] {E₁ : } {E₂ : } :
E₁ E₂ h, ∀ (x : { x // x E₁.carrier }), E₂.emb (↑() x) = E₁.emb x
theorem IsAlgClosed.lift.SubfieldWithHom.compat {K : Type u} {L : Type v} {M : Type w} [] [] [Algebra K L] [] [Algebra K M] {E₁ : } {E₂ : } (h : E₁ E₂) (x : { x // x E₁.carrier }) :
E₂.emb (↑(Subalgebra.inclusion (_ : E₁.carrier E₂.carrier)) x) = E₁.emb x
theorem IsAlgClosed.lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded {K : Type u} {L : Type v} {M : Type w} [] [] [Algebra K L] [] [Algebra K M] (c : ) (hc : IsChain (fun x x_1 => x x_1) c) :
ub, ∀ (N : ), N cN ub
theorem IsAlgClosed.lift.SubfieldWithHom.exists_maximal_subfieldWithHom (K : Type u) (L : Type v) (M : Type w) [] [] [Algebra K L] [] [Algebra K M] :
E, ∀ (N : ), E NN E
noncomputable def IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom (K : Type u) (L : Type v) (M : Type w) [] [] [Algebra K L] [] [Algebra K M] :

The maximal SubfieldWithHom. We later prove that this is equal to ⊤.

Instances For
theorem IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal (K : Type u) (L : Type v) (M : Type w) [] [] [Algebra K L] [] [Algebra K M] (N : ) :
noncomputable def Algebra.adjoin.liftSingleton (R : Type u_1) [] {S : Type u_2} {T : Type u_3} [] [] [Algebra R S] [Algebra R T] (x : S) (y : T) (h : ↑() (minpoly R x) = 0) :
{ x // x Algebra.adjoin R {x} } →ₐ[R] T

Produce an algebra homomorphism Adjoin R {x} →ₐ[R] T sending x to a root of x's minimal polynomial in T.

Instances For
theorem IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top (K : Type u) (L : Type v) (M : Type w) [] [] [Algebra K L] [] [Algebra K M] [] {hL : } :
().carrier =
@[irreducible]
noncomputable def IsAlgClosed.lift {M : Type u_1} [] [] {R : Type u_2} [] {S : Type u_3} [] [] [Algebra R S] [Algebra R M] [] [] (hS : ) :

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

Instances For
theorem IsAlgClosed.lift_def {M : Type u_1} [] [] {R : Type u_2} [] {S : Type u_3} [] [] [Algebra R S] [Algebra R M] [] [] (hS : ) :
= let_fun this := (_ : ); let_fun this_1 := (_ : IsScalarTower R () ()); let_fun this_2 := (_ : ); let f := IsAlgClosed.lift_aux () () M this_2; AlgHom.comp () ()
noncomputable instance IsAlgClosed.perfectRing (k : Type u) [] (p : ) [Fact ()] [CharP k p] [] :
instance IsAlgClosed.instInfinite {K : Type u_1} [] [] :

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

noncomputable def IsAlgClosure.equiv (R : Type u) [] (L : Type v) (M : Type w) [] [] [Algebra R M] [] [] [Algebra R L] [] [] :

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

Instances For
theorem IsAlgClosure.ofAlgebraic (K : Type u_1) (J : Type u_2) (L : Type v) [] [] [] [Algebra K J] [Algebra J L] [] [Algebra K L] [] (hKJ : ) :

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) [] [] [] [] [Algebra R M] [] [] [Algebra S L] [] [] [Algebra R S] [Algebra R L] [] [] [] (hRL : ) :

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

Instances For
noncomputable def IsAlgClosure.equivOfAlgebraic (K : Type u_1) (J : Type u_2) (L : Type v) (M : Type w) [] [] [] [] [Algebra K M] [] [Algebra K J] [Algebra J L] [] [Algebra K L] [] (hKJ : ) :

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

Instances For
noncomputable def IsAlgClosure.equivOfEquivAux {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [] [] [] [] [Algebra R M] [] [] [Algebra S L] [] [] (hSR : S ≃+* R) :
{ e // RingHom.comp () () = RingHom.comp () () }

Used in the definition of equivOfEquiv

Instances For
noncomputable def IsAlgClosure.equivOfEquiv {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [] [] [] [] [Algebra R M] [] [] [Algebra S L] [] [] (hSR : S ≃+* R) :
L ≃+* M

Algebraic closure of isomorphic fields are isomorphic

Instances For
@[simp]
theorem IsAlgClosure.equivOfEquiv_comp_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [] [] [] [] [Algebra R M] [] [] [Algebra S L] [] [] (hSR : S ≃+* R) :
RingHom.comp (↑()) () = RingHom.comp () hSR
@[simp]
theorem IsAlgClosure.equivOfEquiv_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [] [] [] [] [Algebra R M] [] [] [Algebra S L] [] [] (hSR : S ≃+* R) (s : S) :
↑() (↑() s) = ↑() (hSR s)
@[simp]
theorem IsAlgClosure.equivOfEquiv_symm_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [] [] [] [] [Algebra R M] [] [] [Algebra S L] [] [] (hSR : S ≃+* R) (r : R) :
↑(RingEquiv.symm ()) (↑() r) = ↑() (↑() r)
@[simp]
theorem IsAlgClosure.equivOfEquiv_symm_comp_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [] [] [] [] [Algebra R M] [] [] [Algebra S L] [] [] (hSR : S ≃+* R) :
theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly {F : Type u_1} {K : Type u_2} (A : Type u_3) [] [] [] [] [Algebra F K] (hK : ) [Algebra F A] (x : K) :
(Set.range fun ψ => ψ x) = Polynomial.rootSet (minpoly F x) 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.