# Documentation

Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

# Algebraic Closure #

In this file we construct the algebraic closure of a field

## Main Definitions #

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

Instances For

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

Instances For

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

Instances For

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.

Instances For
theorem AlgebraicClosure.toSplittingField_evalXSelf (k : Type u) [] {s : } (hf : f s) :
= 0

A random maximal ideal that contains spanEval k

Instances For

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

Instances For

The canonical ring homomorphism to AdjoinMonic k.

Instances For
theorem AlgebraicClosure.AdjoinMonic.algebraMap (k : Type u) [] :
= RingHom.comp () MvPolynomial.C
theorem AlgebraicClosure.AdjoinMonic.exists_root (k : Type u) [] {f : } (hfm : ) (hfi : ) :
x,
def AlgebraicClosure.stepAux (k : Type u) [] (n : ) :
(α : Type u) ×

The nth step of constructing AlgebraicClosure, together with its Field instance.

Instances For
def AlgebraicClosure.Step (k : Type u) [] (n : ) :

The nth step of constructing AlgebraicClosure.

Instances For
instance AlgebraicClosure.Step.field (k : Type u) [] (n : ) :
theorem AlgebraicClosure.Step.succ (k : Type u) [] (n : ) :
instance AlgebraicClosure.Step.inhabited (k : Type u) [] (n : ) :

The canonical inclusion to the 0th step.

Instances For

The canonical ring homomorphism to the next step.

Instances For
theorem AlgebraicClosure.toStepSucc.exists_root (k : Type u) [] {n : } {f : } (hfm : ) (hfi : ) :
x, = 0
def AlgebraicClosure.toStepOfLE (k : Type u) [] (m : ) (n : ) (h : m n) :

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

Instances For
@[simp]
theorem AlgebraicClosure.coe_toStepOfLE (k : Type u) [] (m : ) (n : ) (h : m n) :
↑() = fun a => Nat.leRecOn h (fun n => ↑()) a
instance AlgebraicClosure.Step.algebra (k : Type u) [] (n : ) :
Algebra k ()
theorem AlgebraicClosure.Step.isIntegral (k : Type u) [] (n : ) (z : ) :
instance AlgebraicClosure.toStepOfLE.directedSystem (k : Type u) [] :
DirectedSystem () fun i j h => ↑()
def AlgebraicClosureAux (k : Type u) [] :

Auxiliary construction for AlgebraicClosure. Although AlgebraicClosureAux does define the algebraic closure of a field, it is redefined at AlgebraicClosure in order to make sure certain instance diamonds commute by definition.

Instances For

AlgebraicClosureAux k is a Field

Instances For
def AlgebraicClosureAux.ofStep (k : Type u) [] (n : ) :

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

Instances For
theorem AlgebraicClosureAux.exists_ofStep (k : Type u) [] (z : ) :
n x, ↑() x = z
theorem AlgebraicClosureAux.exists_root (k : Type u) [] {f : } (hfm : ) (hfi : ) :
x, = 0

AlgebraicClosureAux k is a k-Algebra

Instances For
def AlgebraicClosureAux.ofStepHom (k : Type u) [] (n : ) :

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

Instances For
def AlgebraicClosure (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.

Instances For
instance AlgebraicClosure.instSMulAlgebraicClosure (k : Type u) [] {S : Type u_1} [] [] :
SMul S ()
instance AlgebraicClosure.instAlgebra (k : Type u) [] {R : Type u_1} [] [Algebra R k] :

The equivalence between AlgebraicClosure and AlgebraicClosureAux, which we use to transfer properties of AlgebraicClosureAux to AlgebraicClosure

Instances For