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). Usually this needs to be repeated countably many times (see Exercise 1.13 in [AM69]), but using a theorem of Isaacs [Isa80], once is enough (see https://kconrad.math.uconn.edu/blurbs/galoistheory/algclosure.pdf).

Tags

algebraic closure, algebraically closed

@[reducible, inline]

abbrev AlgebraicClosure.MonicIrreducible (k : Type u) [Field k] : Type u

The subtype of monic irreducible polynomials

Equations

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

def AlgebraicClosure.evalXSelf (k : Type u) [Field k] (f : AlgebraicClosure.MonicIrreducible k) : MvPolynomial (AlgebraicClosure.MonicIrreducible k) k

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

def AlgebraicClosure.spanEval (k : Type u) [Field k] : Ideal (MvPolynomial (AlgebraicClosure.MonicIrreducible k) k)

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

Equations

• AlgebraicClosure.spanEval k = Ideal.span (Set.range (AlgebraicClosure.evalXSelf k))

def AlgebraicClosure.toSplittingField (k : Type u) [Field k] (s : Finset (AlgebraicClosure.MonicIrreducible k)) : MvPolynomial (AlgebraicClosure.MonicIrreducible k) k →ₐ[k] (∏ x ∈ s, ↑x).SplittingField

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.

theorem AlgebraicClosure.toSplittingField_evalXSelf (k : Type u) [Field k] {s : Finset (AlgebraicClosure.MonicIrreducible k)} {f : AlgebraicClosure.MonicIrreducible k} (hf : f ∈ s) : (AlgebraicClosure.toSplittingField k s) (AlgebraicClosure.evalXSelf k f) = 0

theorem AlgebraicClosure.spanEval_ne_top (k : Type u) [Field k] : AlgebraicClosure.spanEval k ≠ ⊤

def AlgebraicClosure.maxIdeal (k : Type u) [Field k] : Ideal (MvPolynomial (AlgebraicClosure.MonicIrreducible 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.spanEval 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.MonicIrreducible 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) ⋯

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)