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,\mathrm{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.

Equations

• AlgebraicClosure.Monics k = { f : Polynomial k // f.Monic }

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.

Equations

• AlgebraicClosure.Vars k = ((f : AlgebraicClosure.Monics k) × Fin (↑f).natDegree)

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

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

Equations

• AlgebraicClosure.subProdXSubC f = Polynomial.map (algebraMap k (MvPolynomial (AlgebraicClosure.Vars k) k)) ↑f - ∏ i : Fin (↑f).natDegree, (Polynomial.X - Polynomial.C (MvPolynomial.X ⟨f, i⟩))

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

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

Equations

• AlgebraicClosure.spanCoeffs k = Ideal.span (Set.range fun (fn : AlgebraicClosure.Monics k × ℕ) => (AlgebraicClosure.subProdXSubC fn.1).coeff fn.2)

def AlgebraicClosure.finEquivRoots {k : Type u} [Field k] {K : Type u_1} [Field K] [DecidableEq K] {i : k →+* K} {f : AlgebraicClosure.Monics k} (hf : Polynomial.Splits i ↑f) : Fin (↑f).natDegree ≃ { x : K × ℕ // x ∈ (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.

Equations

• AlgebraicClosure.finEquivRoots hf = (Finset.equivFinOfCardEq ⋯).symm

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

def AlgebraicClosure.toSplittingField {k : Type u} [Field k] (s : Finset (AlgebraicClosure.Monics k)) : MvPolynomial (AlgebraicClosure.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.

Equations

• AlgebraicClosure.toSplittingField s = MvPolynomial.aeval fun (fi : AlgebraicClosure.Vars k) => if hf : fi.fst ∈ s then (↑((AlgebraicClosure.finEquivRoots ⋯) fi.snd)).1 else 37

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

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

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

A random maximal ideal that contains spanEval k

Equations

• AlgebraicClosure.maxIdeal k = Classical.choose ⋯

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

theorem AlgebraicClosure.le_maxIdeal (k : Type u) [Field k] : AlgebraicClosure.spanCoeffs k ≤ AlgebraicClosure.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.

Stacks Tag 09GT

Equations

• AlgebraicClosure k = (MvPolynomial (AlgebraicClosure.Vars k) k ⧸ AlgebraicClosure.maxIdeal k)

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

Equations

• AlgebraicClosure.instCommRing k = Ideal.Quotient.commRing (AlgebraicClosure.maxIdeal k)

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

Equations

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

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

Equations

• AlgebraicClosure.instSMulOfIsScalarTower k = Submodule.Quotient.instSMul' (AlgebraicClosure.maxIdeal k)

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

Equations

• AlgebraicClosure.instAlgebra k = Ideal.Quotient.algebra R

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)

Equations

• AlgebraicClosure.instGroupWithZero k = GroupWithZero.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• AlgebraicClosure.instField k = Field.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x1 : ℚ≥0) (x2 : AlgebraicClosure k) => x1 • x2) ⋯ ⋯ (fun (x1 : ℚ) (x2 : AlgebraicClosure k) => x1 • x2) ⋯

theorem AlgebraicClosure.Monics.map_eq_prod (k : Type u) [Field k] {f : AlgebraicClosure.Monics k} : Polynomial.map (algebraMap k (AlgebraicClosure k)) ↑f = ∏ i : Fin (↑f).natDegree, Polynomial.map (Ideal.Quotient.mk (AlgebraicClosure.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) {L : Type u_1} [Field k] [Field L] [Algebra k L] [Algebra.IsAlgebraic k L] : IsAlgClosure k (AlgebraicClosure L)