# 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

Equations
• = { f : // }
Instances For

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

Equations
Instances For

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicClosure.toSplittingField_evalXSelf (k : Type u) [] {s : } (hf : f s) :

A random maximal ideal that contains spanEval k

Equations
Instances For
Equations
• =

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

Equations
Instances For
Equations
Equations
• = { default := 37 }

The canonical ring homomorphism to AdjoinMonic k.

Equations
Instances For
Equations
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def AlgebraicClosure.Step (k : Type u) [] (n : ) :

The nth step of constructing AlgebraicClosure.

Equations
• = ().fst
Instances For
instance AlgebraicClosure.Step.field (k : Type u) [] (n : ) :
Equations
• = ().snd
theorem AlgebraicClosure.Step.succ (k : Type u) [] (n : ) :
instance AlgebraicClosure.Step.inhabited (k : Type u) [] (n : ) :
Equations
• = { default := 37 }

The canonical inclusion to the 0th step.

Equations
Instances For

The canonical ring homomorphism to the next step.

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

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

Equations
• = { toMonoidHom := { toOneHom := { toFun := , map_one' := }, map_mul' := }, map_zero' := , map_add' := }
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 ()
Equations
Equations
• =
theorem AlgebraicClosure.Step.isIntegral (k : Type u) [] (n : ) (z : ) :
instance AlgebraicClosure.toStepOfLE.directedSystem (k : Type u) [] :
DirectedSystem fun (i j : ) (h : i j) => ()
Equations
• =
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.

Equations
Instances For

AlgebraicClosureAux k is a Field

Equations
Instances For
Equations
• = { default := 37 }
def AlgebraicClosureAux.ofStep (k : Type u) [] (n : ) :

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

Equations
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

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

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

Equations
• = let __src := ; { toRingHom := __src, commutes' := }
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.

Equations
Instances For
instance AlgebraicClosure.instCommRing (k : Type u) [] :
Equations
instance AlgebraicClosure.instInhabited (k : Type u) [] :
Equations
• = { default := 37 }
instance AlgebraicClosure.instSMulAlgebraicClosure (k : Type u) [] {S : Type u_1} [] [] :
SMul S ()
Equations
instance AlgebraicClosure.instAlgebra (k : Type u) [] {R : Type u_1} [] [Algebra R k] :
Equations

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

Equations
Instances For
Equations
• = let e := ; let __spread.0 := ; GroupWithZero.mk zpowRec
instance AlgebraicClosure.instField (k : Type u) [] :
Equations
• One or more equations did not get rendered due to their size.
instance AlgebraicClosure.isAlgClosed (k : Type u) [] :
Equations
• =
Equations
• =