# 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

The subtype of monic irreducible polynomials

## Equations

- AlgebraicClosure.MonicIrreducible k = { f : Polynomial k // f.Monic ∧ Irreducible f }

## Instances For

Sends a monic irreducible polynomial `f`

to `f(x_f)`

where `x_f`

is a formal indeterminate.

## Equations

- AlgebraicClosure.evalXSelf k f = Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X f) ↑f

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

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

- AlgebraicClosure.AdjoinMonic.inhabited k = { default := 37 }

The canonical ring homomorphism to `AdjoinMonic k`

.

## Equations

- AlgebraicClosure.toAdjoinMonic k = (Ideal.Quotient.mk (AlgebraicClosure.maxIdeal k)).comp MvPolynomial.C

## Instances For

## Equations

- AlgebraicClosure.AdjoinMonic.algebra k = (AlgebraicClosure.toAdjoinMonic k).toAlgebra

The `n`

th step of constructing `AlgebraicClosure`

, together with its `Field`

instance.

## Equations

- AlgebraicClosure.stepAux k n = Nat.recOn n ⟨k, inferInstance⟩ fun (x : ℕ) (ih : (α : Type u) × Field α) => ⟨AlgebraicClosure.AdjoinMonic ih.fst, AlgebraicClosure.AdjoinMonic.field ih.fst⟩

## Instances For

The `n`

th step of constructing `AlgebraicClosure`

.

## Equations

- AlgebraicClosure.Step k n = (AlgebraicClosure.stepAux k n).fst

## Instances For

## Equations

- AlgebraicClosure.Step.field k n = (AlgebraicClosure.stepAux k n).snd

## Equations

- AlgebraicClosure.Step.inhabited k n = { default := 37 }

The canonical inclusion to the `0`

th step.

## Equations

## Instances For

The canonical ring homomorphism to the next step.

## Equations

## Instances For

## Equations

- AlgebraicClosure.Step.algebraSucc k n = (AlgebraicClosure.toStepSucc k n).toAlgebra

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

## Equations

- AlgebraicClosure.toStepOfLE k m n h = { toFun := AlgebraicClosure.toStepOfLE' k m n h, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

## Instances For

## Equations

- AlgebraicClosure.Step.algebra k n = (AlgebraicClosure.toStepOfLE k 0 n ⋯).toAlgebra

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

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

- AlgebraicClosureAux k = Ring.DirectLimit (AlgebraicClosure.Step k) fun (i j : ℕ) (h : i ≤ j) => ⇑(AlgebraicClosure.toStepOfLE k i j h)

## Instances For

## Equations

- AlgebraicClosureAux.instInhabited k = { default := 37 }

The canonical ring embedding from the `n`

th step to the algebraic closure.

## Equations

- AlgebraicClosureAux.ofStep k n = Ring.DirectLimit.of (AlgebraicClosure.Step k) (fun (i j : ℕ) (h : i ≤ j) => ⇑(AlgebraicClosure.toStepOfLE k i j h)) n

## Instances For

`AlgebraicClosureAux k`

is a `k`

-`Algebra`

## Equations

- AlgebraicClosureAux.instAlgebra k = (AlgebraicClosureAux.ofStep k 0).toAlgebra

## Instances For

Canonical algebra embedding from the `n`

th step to the algebraic closure.

## Equations

- AlgebraicClosureAux.ofStepHom k n = let __src := AlgebraicClosureAux.ofStep k n; { toRingHom := __src, commutes' := ⋯ }

## Instances For

## Equations

- ⋯ = ⋯

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

## Equations

- AlgebraicClosure k = (MvPolynomial (AlgebraicClosureAux k) k ⧸ RingHom.ker (MvPolynomial.aeval id).toRingHom)

## Instances For

## Equations

- AlgebraicClosure.instCommRing k = Ideal.Quotient.commRing (RingHom.ker (MvPolynomial.aeval id).toRingHom)

## Equations

- AlgebraicClosure.instInhabited k = { default := 37 }

## Equations

## Equations

## Equations

- ⋯ = ⋯

The equivalence between `AlgebraicClosure`

and `AlgebraicClosureAux`

, which we use to transfer
properties of `AlgebraicClosureAux`

to `AlgebraicClosure`

## Equations

## Instances For

## Equations

- AlgebraicClosure.instGroupWithZero k = let e := AlgebraicClosure.algEquivAlgebraicClosureAux k; let __spread.0 := ⋯; GroupWithZero.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯

## Equations

- One or more equations did not get rendered due to their size.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯