# mathlibdocumentation

field_theory.is_alg_closed.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 #

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

• is_alg_closure k K is the typeclass saying K is an algebraic closure of k.

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

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

## TODO #

Show that any two algebraic closures are isomorphic

## Tags #

algebraic closure, algebraically closed

@[class]
structure is_alg_closed (k : Type u) [field k] :
Prop
• splits : ∀ (p : ,

Typeclass for algebraically closed fields.

To show polynomial.splits p f for an arbitrary ring homomorphism f, see is_alg_closed.splits_codomain and is_alg_closed.splits_domain.

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

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

See also is_alg_closed.splits_domain for the case where K is algebraically closed.

theorem is_alg_closed.splits_domain {k : Type u_1} {K : Type u_2} [field k] [field K] {f : k →+* K} (p : polynomial k) :

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

See also is_alg_closed.splits_codomain for the case where k is algebraically closed.

theorem is_alg_closed.exists_root {k : Type u} [field k] (p : polynomial k) (hp : p.degree 0) :
∃ (x : k), p.is_root x
theorem is_alg_closed.exists_pow_nat_eq {k : Type u} [field k] (x : k) {n : } (hn : 0 < n) :
∃ (z : k), z ^ n = x
theorem is_alg_closed.exists_eq_mul_self {k : Type u} [field k] (x : k) :
∃ (z : k), x = z * z
theorem is_alg_closed.exists_eval₂_eq_zero_of_injective {k : Type u} [field k] {R : Type u_1} [ring R] (f : R →+* k) (hf : function.injective f) (p : polynomial R) (hp : p.degree 0) :
∃ (x : k), p = 0
theorem is_alg_closed.exists_eval₂_eq_zero {k : Type u} [field k] {R : Type u_1} [field R] (f : R →+* k) (p : polynomial R) (hp : p.degree 0) :
∃ (x : k), p = 0
theorem is_alg_closed.exists_aeval_eq_zero_of_injective (k : Type u) [field k] {R : Type u_1} [comm_ring R] [ k] (hinj : function.injective k)) (p : polynomial R) (hp : p.degree 0) :
∃ (x : k), p = 0
theorem is_alg_closed.exists_aeval_eq_zero (k : Type u) [field k] {R : Type u_1} [field R] [ k] (p : polynomial R) (hp : p.degree 0) :
∃ (x : k), p = 0
theorem is_alg_closed.of_exists_root (k : Type u) [field k] (H : ∀ (p : , p.monic(∃ (x : k), = 0)) :
theorem is_alg_closed.degree_eq_one_of_irreducible (k : Type u) [field k] {p : polynomial k} (h_nz : p 0) (hp : irreducible p) :
p.degree = 1
theorem is_alg_closed.algebra_map_surjective_of_is_integral {k : Type u_1} {K : Type u_2} [field k] [ring K] [is_domain K] [hk : is_alg_closed k] [ K] (hf : K) :
theorem is_alg_closed.algebra_map_surjective_of_is_integral' {k : Type u_1} {K : Type u_2} [field k] [comm_ring K] [is_domain K] [hk : is_alg_closed k] (f : k →+* K) (hf : f.is_integral) :
theorem is_alg_closed.algebra_map_surjective_of_is_algebraic {k : Type u_1} {K : Type u_2} [field k] [ring K] [is_domain K] [hk : is_alg_closed k] [ K] (hf : K) :
@[class]
structure is_alg_closure (k : Type u) [field k] (K : Type v) [field K] [ K] :
Prop
• alg_closed :
• algebraic :

Typeclass for an extension being an algebraic closure.

Instances
theorem is_alg_closure_iff (k : Type u) [field k] (K : Type v) [field K] [ K] :
theorem exists_spectrum_of_is_alg_closed_of_finite_dimensional (𝕜 : Type u_1) [field 𝕜] {A : Type u_2} [nontrivial A] [ring A] [ A] [I : A] (f : A) :
∃ (c : 𝕜), ¬is_unit (f - A) c)

Every element f in a nontrivial finite-dimensional algebra A over an algebraically closed field K has non-empty spectrum: that is, there is some c : K so f - c • 1 is not invertible.

structure lift.subfield_with_hom (K : Type u) (L : Type v) (M : Type w) [field K] [field L] [ L] [field M] [ M] (hL : L) :
Type (max v w)

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

@[instance]
def lift.subfield_with_hom.has_le {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [ L] [field M] [ M] {hL : L} :
has_le M hL)
Equations
@[instance]
def lift.subfield_with_hom.inhabited {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [ L] [field M] [ M] {hL : L} :
inhabited M hL)
Equations
theorem lift.subfield_with_hom.le_def {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [ L] [field M] [ M] {hL : L} {E₁ E₂ : hL} :
E₁ E₂ ∃ (h : E₁.carrier E₂.carrier), ∀ (x : (E₁.carrier)), (E₂.emb) x) = (E₁.emb) x
theorem lift.subfield_with_hom.compat {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [ L] [field M] [ M] {hL : L} {E₁ E₂ : hL} (h : E₁ E₂) (x : (E₁.carrier)) :
(E₂.emb) x) = (E₁.emb) x
@[instance]
def lift.subfield_with_hom.preorder {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [ L] [field M] [ M] {hL : L} :
preorder M hL)
Equations
theorem lift.subfield_with_hom.maximal_subfield_with_hom_chain_bounded {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [ L] [field M] [ M] {hL : L} (c : set M hL)) (hc : c) (hcn : c.nonempty) :
∃ (ub : hL), ∀ (N : hL), N cN ub
theorem lift.subfield_with_hom.exists_maximal_subfield_with_hom {K : Type u} {L : Type v} (M : Type w) [field K] [field L] [ L] [field M] [ M] (hL : L) :
∃ (E : hL), ∀ (N : hL), E NN E
def lift.subfield_with_hom.maximal_subfield_with_hom {K : Type u} {L : Type v} (M : Type w) [field K] [field L] [ L] [field M] [ M] (hL : L) :
hL

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

Equations
theorem lift.subfield_with_hom.maximal_subfield_with_hom_is_maximal {K : Type u} {L : Type v} (M : Type w) [field K] [field L] [ L] [field M] [ M] (hL : L) (N : hL) :
theorem lift.subfield_with_hom.maximal_subfield_with_hom_eq_top {K : Type u} {L : Type v} (M : Type w) [field K] [field L] [ L] [field M] [ M] (hL : L) :
def is_alg_closed.lift (K : Type u) [field K] (L : Type v) (M : Type w) [field L] [ L] [field M] [ M] (hL : L) :

A (random) hom from an algebraic extension of K into an algebraically closed extension of K

Equations
def is_alg_closure.equiv (K : Type u) [field K] (L : Type v) (M : Type w) [field L] [field M] [ M] [ M] [ L] [ L] :

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

Equations
def is_alg_closure.equiv_of_algebraic (J : Type u_1) (K : Type u) [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [ M] [ M] [ J] [ L] [ L] [ L] [ L] (hKJ : J) :

An equiv between an algebraic closure of K and an algebraic closure of an algebraic extension of K

Equations
• hKJ = let _inst : := _ in M
def is_alg_closure.equiv_of_equiv_aux {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [ M] [ M] [ L] [ L] (hJK : J ≃+* K) :
{e // e.to_ring_hom.comp L) = M).comp hJK.to_ring_hom}

Used in the definition of equiv_of_equiv

Equations
def is_alg_closure.equiv_of_equiv {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [ M] [ M] [ L] [ L] (hJK : J ≃+* K) :
L ≃+* M

Algebraic closure of isomorphic fields are isomorphic

Equations
@[simp]
theorem is_alg_closure.equiv_of_equiv_comp_algebra_map {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [ M] [ M] [ L] [ L] (hJK : J ≃+* K) :
hJK).comp L) = M).comp hJK
@[simp]
theorem is_alg_closure.equiv_of_equiv_algebra_map {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [ M] [ M] [ L] [ L] (hJK : J ≃+* K) (j : J) :
hJK) ( L) j) = M) (hJK j)
@[simp]
theorem is_alg_closure.equiv_of_equiv_symm_algebra_map {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [ M] [ M] [ L] [ L] (hJK : J ≃+* K) (k : K) :
hJK).symm) ( M) k) = L) ((hJK.symm) k)
@[simp]
theorem is_alg_closure.equiv_of_equiv_symm_comp_algebra_map {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [ M] [ M] [ L] [ L] (hJK : J ≃+* K) :
hJK).symm).comp M) = L).comp (hJK.symm)