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

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

theorem is_alg_closed.of_exists_root (k : Type u) [field k] :
(∀ (p : , p.monic(∃ (x : k), = 0))

theorem is_alg_closed.degree_eq_one_of_irreducible (k : Type u) [field k] {p : polynomial k} :
p 0p.degree = 1

@[instance]

@[class]
def is_alg_closure (k : Type u) [field k] (K : Type v) [field K] [ K] :
Prop

Typeclass for an extension being an algebraic closure.

Equations
Instances
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]  :
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} :
f.monic(∃ (x : ,

def algebraic_closure.step_aux (k : Type u) [field k] :
(Σ (α : Type u), field α)

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

Equations
def algebraic_closure.step (k : Type u) [field k] :
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 } :
f.monic(∃ (x : (n + 1)), = 0)

def algebraic_closure.to_step_of_le (k : Type u) [field k] (m n : ) :
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
@[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 } :
f.monic(∃ (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] :