# mathlib3documentation

field_theory.is_alg_closed.algebraic_closure

# Algebraic Closure #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we construct the algebraic closure of a field

## Main Definitions #

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

## Tags #

algebraic closure, algebraically closed

@[reducible]

The subtype of monic irreducible polynomials

Equations
noncomputable 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
noncomputable 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
noncomputable def algebraic_closure.to_splitting_field (k : Type u) [field k]  :
→ₐ[k] (s.prod (λ (x : , 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
noncomputable def algebraic_closure.max_ideal (k : Type u) [field k] :

A random maximal ideal that contains span_eval k

Equations
Instances for algebraic_closure.max_ideal
@[protected, instance]

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

Equations
Instances for algebraic_closure.adjoin_monic
@[protected, instance]
noncomputable def algebraic_closure.adjoin_monic.field (k : Type u) [field k] :
Equations
@[protected, instance]
noncomputable def algebraic_closure.adjoin_monic.inhabited (k : Type u) [field k] :
Equations
noncomputable def algebraic_closure.to_adjoin_monic (k : Type u) [field k] :

The canonical ring homomorphism to adjoin_monic k.

Equations
@[protected, instance]
noncomputable def algebraic_closure.adjoin_monic.algebra (k : Type u) [field k] :
Equations
theorem algebraic_closure.adjoin_monic.exists_root (k : Type u) [field k] {f : polynomial k} (hfm : f.monic) (hfi : irreducible f) :
noncomputable 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 : ) :

The nth step of constructing algebraic_closure.

Equations
Instances for algebraic_closure.step
@[protected, instance]
noncomputable def algebraic_closure.step.field (k : Type u) [field k] (n : ) :
Equations
@[protected, instance]
noncomputable def algebraic_closure.step.inhabited (k : Type u) [field k] (n : ) :
Equations

The canonical inclusion to the 0th step.

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

The canonical ring homomorphism to the next step.

Equations
@[protected, instance]
noncomputable 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
noncomputable 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 : ),
@[protected, instance]
noncomputable def algebraic_closure.step.algebra (k : Type u) [field k] (n : ) :
Equations
@[protected, 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
@[protected, 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] :

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

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

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

Equations
@[protected, instance]
noncomputable 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
@[protected, instance]
@[protected, instance]
noncomputable def algebraic_closure.algebra (k : Type u) [field k] {R : Type u_1} [alg : k] :
Equations
theorem algebraic_closure.algebra_map_def (k : Type u) [field k] {R : Type u_1} [alg : k] :
= k)
@[protected, instance]
def algebraic_closure.is_scalar_tower (k : Type u) [field k] {R : Type u_1} {S : Type u_2} [ S] [ k] [ k] [ k] :
noncomputable def algebraic_closure.of_step_hom (k : Type u) [field k] (n : ) :

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

Equations
@[protected, instance]