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,1}, \dots, X_{f,\deg f}$ corresponding to roots of monic irreducible polynomials f with coefficients in k, and quotienting out by a maximal ideal containing every $f - \prod_i (X - X_{f,i})$. The proof follows https://kconrad.math.uconn.edu/blurbs/galoistheory/algclosureshorter.pdf.

Tags

algebraic closure, algebraically closed

def AlgebraicClosure.Monics (k : Type u) [Field k] : Type u

The subtype of monic polynomials.

def AlgebraicClosure.Vars (k : Type u) [Field k] : Type u

Vars k provides n variables $X_{f,1}, \dots, X_{f,n}$ for each monic polynomial f : k[X] of degree n.

def AlgebraicClosure.subProdXSubC {k : Type u} [Field k] (f : Monics k) : Polynomial (MvPolynomial (Vars k) k)

Given a monic polynomial f : k[X], subProdXSubC f is the polynomial $f - \prod_i (X - X_{f,i})$.

def AlgebraicClosure.spanCoeffs (k : Type u) [Field k] : Ideal (MvPolynomial (Vars k) k)

The span of all coefficients of subProdXSubC f as f ranges all polynomials in k[X].

def AlgebraicClosure.finEquivRoots {k : Type u} [Field k] {K : Type u_1} [Field K] [DecidableEq K] {i : k →+* K} {f : Monics k} (hf : (Polynomial.map i ↑f).Splits) : Fin (↑f).natDegree ≃ ↥(Polynomial.map i ↑f).roots.toEnumFinset

If a monic polynomial f : k[X] splits in K, then it has as many roots (counting multiplicity) as its degree.

theorem AlgebraicClosure.Monics.splits_finsetProd {k : Type u} [Field k] {s : Finset (Monics k)} {f : Monics k} (hf : f ∈ s) : (Polynomial.map (algebraMap k (∏ f ∈ s, ↑f).SplittingField) ↑f).Splits

def AlgebraicClosure.toSplittingField {k : Type u} [Field k] (s : Finset (Monics k)) : MvPolynomial (Vars k) k →ₐ[k] (∏ f ∈ s, ↑f).SplittingField

Given a finite set of monic polynomials, construct an algebra homomorphism to the splitting field of the product of the polynomials sending indeterminates $X_{f_i}$ to the distinct roots of f.

theorem AlgebraicClosure.toSplittingField_coeff {k : Type u} [Field k] {s : Finset (Monics k)} {f : Monics k} (h : f ∈ s) (n : ℕ) : (toSplittingField s) ((subProdXSubC f).coeff n) = 0

theorem AlgebraicClosure.spanCoeffs_ne_top (k : Type u) [Field k] : spanCoeffs k ≠ ⊤

def AlgebraicClosure.maxIdeal (k : Type u) [Field k] : Ideal (MvPolynomial (Vars k) k)

A random maximal ideal that contains spanEval k

instance AlgebraicClosure.maxIdeal.isMaximal (k : Type u) [Field k] : (maxIdeal k).IsMaximal

theorem AlgebraicClosure.le_maxIdeal (k : Type u) [Field k] : spanCoeffs k ≤ maxIdeal k

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

instance AlgebraicClosure.instCommRing (k : Type u) [Field k] : CommRing (AlgebraicClosure k)

instance AlgebraicClosure.instInhabited (k : Type u) [Field k] : Inhabited (AlgebraicClosure k)

instance AlgebraicClosure.instSMulOfIsScalarTower (k : Type u) [Field k] {S : Type u_1} [DistribSMul S k] [IsScalarTower S k k] : SMul S (AlgebraicClosure k)

instance AlgebraicClosure.instAlgebra (k : Type u) [Field k] {R : Type u_1} [CommSemiring R] [Algebra R k] : Algebra R (AlgebraicClosure k)

instance AlgebraicClosure.instIsScalarTower (k : Type u) [Field k] {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] [Algebra S k] [Algebra R k] [IsScalarTower R S k] : IsScalarTower R S (AlgebraicClosure k)

instance AlgebraicClosure.instGroupWithZero (k : Type u) [Field k] : GroupWithZero (AlgebraicClosure k)

instance AlgebraicClosure.instField (k : Type u) [Field k] : Field (AlgebraicClosure k)

theorem AlgebraicClosure.Monics.map_eq_prod (k : Type u) [Field k] {f : Monics k} : Polynomial.map (algebraMap k (AlgebraicClosure k)) ↑f = ∏ i : Fin (↑f).natDegree, Polynomial.map (Ideal.Quotient.mk (maxIdeal k)) (Polynomial.X - Polynomial.C (MvPolynomial.X ⟨f, i⟩))

instance AlgebraicClosure.isAlgebraic (k : Type u) [Field k] : Algebra.IsAlgebraic k (AlgebraicClosure k)

instance AlgebraicClosure.instIsAlgClosure (k : Type u) [Field k] : IsAlgClosure k (AlgebraicClosure k)

instance AlgebraicClosure.isAlgClosed (k : Type u) [Field k] : IsAlgClosed (AlgebraicClosure k)

instance AlgebraicClosure.instCharZero (k : Type u) [Field k] [CharZero k] : CharZero (AlgebraicClosure k)

instance AlgebraicClosure.instCharP (k : Type u) [Field k] {p : ℕ} [CharP k p] : CharP (AlgebraicClosure k) p

instance AlgebraicClosure.instIsAlgClosureOfIsAlgebraic (k : Type u) [Field k] {L : Type u_1} [Field L] [Algebra k L] [Algebra.IsAlgebraic k L] : IsAlgClosure k (AlgebraicClosure L)

instance IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) [Algebra.IsAlgebraic K ↥E] : IsAlgClosure K (AlgebraicClosure ↥E)

theorem IntermediateField.AdjoinSimple.normal_algebraicClosure {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x : L} (hx : IsIntegral K x) : Normal K (AlgebraicClosure ↥K⟮x⟯)

theorem IntermediateField.AdjoinDouble.normal_algebraicClosure {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {x y : L} (hx : IsIntegral K x) (hy : IsIntegral K y) : Normal K (AlgebraicClosure ↥K⟮x, y⟯)