# mathlibdocumentation

field_theory.algebraic_closure

# Algebraic Closure #

In this file we define the typeclass for algebraically closed fields and algebraic closures. We also construct an algebraic closure for any field.

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

• algebraic_closure k is an algebraic closure of k (in the same universe). It is constructed by taking the polynomial ring generated by indeterminates x_f corresponding to monic irreducible polynomials f with coefficients in k, and quotienting out by a maximal ideal containing every f(x_f), and then repeating this step countably many times. See Exercise 1.13 in Atiyah--Macdonald.

## TODO #

Show that any algebraic extension embeds into any algebraically closed extension (via Zorn's lemma).

## 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.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] [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] [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] [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] :
def algebraic_closure.monic_irreducible (k : Type u) [field k] :
Type u

The subtype of monic irreducible polynomials

Equations
def algebraic_closure.eval_X_self (k : Type u) [field k]  :

Sends a monic irreducible polynomial f to f(x_f) where x_f is a formal indeterminate.

Equations
def algebraic_closure.span_eval (k : Type u) [field k] :

The span of f(x_f) across monic irreducible polynomials f where x_f is an indeterminate.

Equations
def algebraic_closure.to_splitting_field (k : Type u) [field k]  :
→ₐ[k] (∏ (x : in s, x).splitting_field

Given a finset of monic irreducible polynomials, construct an algebra homomorphism to the splitting field of the product of the polynomials sending each indeterminate x_f represented by the polynomial f in the finset to a root of f.

Equations
theorem algebraic_closure.to_splitting_field_eval_X_self (k : Type u) [field k] (hf : f s) :
theorem algebraic_closure.span_eval_ne_top (k : Type u) [field k] :
def algebraic_closure.max_ideal (k : Type u) [field k] :

A random maximal ideal that contains span_eval k

Equations
@[instance]
theorem algebraic_closure.le_max_ideal (k : Type u) [field k] :
def algebraic_closure.adjoin_monic (k : Type u) [field k] :
Type u

The first step of constructing algebraic_closure: adjoin a root of all monic polynomials

Equations
@[instance]
Equations
@[instance]
Equations
def algebraic_closure.to_adjoin_monic (k : Type u) [field k] :

The canonical ring homomorphism to adjoin_monic k.

Equations
@[instance]
Equations
theorem algebraic_closure.adjoin_monic.exists_root (k : Type u) [field k] {f : polynomial k} (hfm : f.monic) (hfi : irreducible f) :
∃ (x : ,
def algebraic_closure.step_aux (k : Type u) [field k] (n : ) :
Σ (α : Type u),

The nth step of constructing algebraic_closure, together with its field instance.

Equations
def algebraic_closure.step (k : Type u) [field k] (n : ) :
Type u

The nth step of constructing algebraic_closure.

Equations
@[instance]
def algebraic_closure.step.field (k : Type u) [field k] (n : ) :
Equations
@[instance]
def algebraic_closure.step.inhabited (k : Type u) [field k] (n : ) :
Equations
def algebraic_closure.to_step_zero (k : Type u) [field k] :

The canonical inclusion to the 0th step.

Equations
def algebraic_closure.to_step_succ (k : Type u) [field k] (n : ) :
→+* (n + 1)

The canonical ring homomorphism to the next step.

Equations
@[instance]
def algebraic_closure.step.algebra_succ (k : Type u) [field k] (n : ) :
(n + 1))
Equations
theorem algebraic_closure.to_step_succ.exists_root (k : Type u) [field k] {n : } {f : polynomial } (hfm : f.monic) (hfi : irreducible f) :
∃ (x : (n + 1)), = 0
def algebraic_closure.to_step_of_le (k : Type u) [field k] (m n : ) (h : m n) :

The canonical ring homomorphism to a step with a greater index.

Equations
@[simp]
theorem algebraic_closure.coe_to_step_of_le (k : Type u) [field k] (m n : ) (h : m n) :
h) = (λ (n : ),
@[instance]
def algebraic_closure.step.algebra (k : Type u) [field k] (n : ) :
Equations
@[instance]
def algebraic_closure.step.scalar_tower (k : Type u) [field k] (n : ) :
(n + 1))
theorem algebraic_closure.step.is_integral (k : Type u) [field k] (n : ) (z : n) :
z
@[instance]
def algebraic_closure.to_step_of_le.directed_system (k : Type u) [field k] :
(λ (i j : ) (h : i j), h))
def algebraic_closure (k : Type u) [field k] :
Type u

The canonical algebraic closure of a field, the direct limit of adding roots to the field for each polynomial over the field.

Equations
@[instance]
def algebraic_closure.field (k : Type u) [field k] :
Equations
• = (λ (i j : ) (h : i j), h)
@[instance]
def algebraic_closure.inhabited (k : Type u) [field k] :
Equations
def algebraic_closure.of_step (k : Type u) [field k] (n : ) :

The canonical ring embedding from the nth step to the algebraic closure.

Equations
@[instance]
def algebraic_closure.algebra_of_step (k : Type u) [field k] (n : ) :
Equations
theorem algebraic_closure.of_step_succ (k : Type u) [field k] (n : ) :
(n + 1)).comp =
theorem algebraic_closure.exists_of_step (k : Type u) [field k] (z : algebraic_closure k) :
∃ (n : ) (x : , x = z
theorem algebraic_closure.exists_root (k : Type u) [field k] {f : polynomial } (hfm : f.monic) (hfi : irreducible f) :
∃ (x : , = 0
@[instance]
def algebraic_closure.is_alg_closed (k : Type u) [field k] :
@[instance]
def algebraic_closure.algebra (k : Type u) [field k] :
Equations
def algebraic_closure.of_step_hom (k : Type u) [field k] (n : ) :

Canonical algebra embedding from the nth step to the algebraic closure.

Equations
theorem algebraic_closure.is_algebraic (k : Type u) [field k] :
@[instance]
def algebraic_closure.is_alg_closure (k : Type u) [field 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.