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

Equations

• ⋯ = ⋯

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

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

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

Equations

• AlgebraicClosure.AdjoinMonic k = (MvPolynomial (AlgebraicClosure.MonicIrreducible k) k ⧸ AlgebraicClosure.maxIdeal k)

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

Equations

• AlgebraicClosure.AdjoinMonic.field k = Ideal.Quotient.field (AlgebraicClosure.maxIdeal k)

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

Equations

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

def AlgebraicClosure.toAdjoinMonic (k : Type u) [Field k] : k →+* AlgebraicClosure.AdjoinMonic k

The canonical ring homomorphism to AdjoinMonic k.

Equations

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

instance AlgebraicClosure.AdjoinMonic.algebra (k : Type u) [Field k] : Algebra k (AlgebraicClosure.AdjoinMonic k)

Equations

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

theorem AlgebraicClosure.AdjoinMonic.algebraMap (k : Type u) [Field k] : algebraMap k (AlgebraicClosure.AdjoinMonic k) = (Ideal.Quotient.mk (AlgebraicClosure.maxIdeal k)).comp MvPolynomial.C

theorem AlgebraicClosure.AdjoinMonic.isIntegral (k : Type u) [Field k] (z : AlgebraicClosure.AdjoinMonic k) : IsIntegral k z

theorem AlgebraicClosure.AdjoinMonic.exists_root (k : Type u) [Field k] {f : Polynomial k} (hfm : f.Monic) (hfi : Irreducible f) : ∃ (x : AlgebraicClosure.AdjoinMonic k), Polynomial.eval₂ (AlgebraicClosure.toAdjoinMonic k) x f = 0

def AlgebraicClosure.stepAux (k : Type u) [Field k] (n : ℕ) : (α : Type u) × Field α

The nth step of constructing AlgebraicClosure, together with its Field instance.

Equations

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

def AlgebraicClosure.Step (k : Type u) [Field k] (n : ℕ) : Type u

The nth step of constructing AlgebraicClosure.

Equations

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

theorem AlgebraicClosure.Step.zero (k : Type u) [Field k] : AlgebraicClosure.Step k 0 = k

instance AlgebraicClosure.Step.field (k : Type u) [Field k] (n : ℕ) : Field (AlgebraicClosure.Step k n)

Equations

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

theorem AlgebraicClosure.Step.succ (k : Type u) [Field k] (n : ℕ) : AlgebraicClosure.Step k (n + 1) = AlgebraicClosure.AdjoinMonic (AlgebraicClosure.Step k n)

instance AlgebraicClosure.Step.inhabited (k : Type u) [Field k] (n : ℕ) : Inhabited (AlgebraicClosure.Step k n)

Equations

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

def AlgebraicClosure.toStepZero (k : Type u) [Field k] : k →+* AlgebraicClosure.Step k 0

The canonical inclusion to the 0th step.

Equations

• AlgebraicClosure.toStepZero k = RingHom.id k

def AlgebraicClosure.toStepSucc (k : Type u) [Field k] (n : ℕ) : AlgebraicClosure.Step k n →+* AlgebraicClosure.Step k (n + 1)

The canonical ring homomorphism to the next step.

Equations

• AlgebraicClosure.toStepSucc k n = AlgebraicClosure.toAdjoinMonic (AlgebraicClosure.Step k n)

instance AlgebraicClosure.Step.algebraSucc (k : Type u) [Field k] (n : ℕ) : Algebra (AlgebraicClosure.Step k n) (AlgebraicClosure.Step k (n + 1))

Equations

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

theorem AlgebraicClosure.toStepSucc.exists_root (k : Type u) [Field k] {n : ℕ} {f : Polynomial (AlgebraicClosure.Step k n)} (hfm : f.Monic) (hfi : Irreducible f) : ∃ (x : AlgebraicClosure.Step k (n + 1)), Polynomial.eval₂ (AlgebraicClosure.toStepSucc k n) x f = 0

def AlgebraicClosure.toStepOfLE (k : Type u) [Field k] (m n : ℕ) (h : m ≤ n) : AlgebraicClosure.Step k m →+* AlgebraicClosure.Step k n

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' := ⋯ }

@[simp]

theorem AlgebraicClosure.coe_toStepOfLE (k : Type u) [Field k] (m n : ℕ) (h : m ≤ n) : ⇑(AlgebraicClosure.toStepOfLE k m n h) = fun (a : AlgebraicClosure.Step k m) => Nat.leRecOn h (fun (n : ℕ) => ⇑(AlgebraicClosure.toStepSucc k n)) a

instance AlgebraicClosure.Step.algebra (k : Type u) [Field k] (n : ℕ) : Algebra k (AlgebraicClosure.Step k n)

Equations

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

instance AlgebraicClosure.Step.scalar_tower (k : Type u) [Field k] (n : ℕ) : IsScalarTower k (AlgebraicClosure.Step k n) (AlgebraicClosure.Step k (n + 1))

Equations

• ⋯ = ⋯

theorem AlgebraicClosure.Step.isIntegral (k : Type u) [Field k] (n : ℕ) (z : AlgebraicClosure.Step k n) : IsIntegral k z

instance AlgebraicClosure.toStepOfLE.directedSystem (k : Type u) [Field k] : DirectedSystem (AlgebraicClosure.Step k) fun (i j : ℕ) (h : i ≤ j) => ⇑(AlgebraicClosure.toStepOfLE k i j h)

Equations

• ⋯ = ⋯

def AlgebraicClosureAux (k : Type u) [Field 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

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

def AlgebraicClosureAux.field (k : Type u) [Field k] : Field (AlgebraicClosureAux k)

AlgebraicClosureAux k is a Field

Equations

• AlgebraicClosureAux.field k = Field.DirectLimit.field (AlgebraicClosure.Step k) (AlgebraicClosure.toStepOfLE k)

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

Equations

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

def AlgebraicClosureAux.ofStep (k : Type u) [Field k] (n : ℕ) : AlgebraicClosure.Step k n →+* AlgebraicClosureAux k

The canonical ring embedding from the nth 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

theorem AlgebraicClosureAux.ofStep_succ (k : Type u) [Field k] (n : ℕ) : (AlgebraicClosureAux.ofStep k (n + 1)).comp (AlgebraicClosure.toStepSucc k n) = AlgebraicClosureAux.ofStep k n

theorem AlgebraicClosureAux.exists_ofStep (k : Type u) [Field k] (z : AlgebraicClosureAux k) : ∃ (n : ℕ) (x : AlgebraicClosure.Step k n), (AlgebraicClosureAux.ofStep k n) x = z

theorem AlgebraicClosureAux.exists_root (k : Type u) [Field k] {f : Polynomial (AlgebraicClosureAux k)} (hfm : f.Monic) (hfi : Irreducible f) : ∃ (x : AlgebraicClosureAux k), Polynomial.eval x f = 0

theorem AlgebraicClosureAux.instIsAlgClosed (k : Type u) [Field k] : IsAlgClosed (AlgebraicClosureAux k)

def AlgebraicClosureAux.instAlgebra (k : Type u) [Field k] : Algebra k (AlgebraicClosureAux k)

AlgebraicClosureAux k is a k-Algebra

Equations

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

def AlgebraicClosureAux.ofStepHom (k : Type u) [Field k] (n : ℕ) : AlgebraicClosure.Step k n →ₐ[k] AlgebraicClosureAux k

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

Equations

• AlgebraicClosureAux.ofStepHom k n = { toRingHom := AlgebraicClosureAux.ofStep k n, commutes' := ⋯ }

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

Equations

• ⋯ = ⋯

theorem AlgebraicClosureAux.isAlgClosure (k : Type u) [Field k] : IsAlgClosure k (AlgebraicClosureAux 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 (AlgebraicClosureAux k) k ⧸ RingHom.ker (MvPolynomial.aeval id).toRingHom)

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

Equations

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

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' (RingHom.ker (MvPolynomial.aeval id).toRingHom)

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)

Equations

• ⋯ = ⋯

def AlgebraicClosure.algEquivAlgebraicClosureAux (k : Type u) [Field k] : AlgebraicClosure k ≃ₐ[k] AlgebraicClosureAux k

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

Equations

• AlgebraicClosure.algEquivAlgebraicClosureAux k = id (Ideal.quotientKerAlgEquivOfSurjective ⋯)

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

Equations

• AlgebraicClosure.instGroupWithZero k = GroupWithZero.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯

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.isAlgClosed (k : Type u) [Field k] : IsAlgClosed (AlgebraicClosure k)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

theorem Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] {f g : Polynomial K} (hf0 : f ≠ 0) : (∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ Polynomial.derivative f * g

Over an algebraically closed field of characteristic zero a necessary and sufficient condition for the set of roots of a nonzero polynomial f to be a subset of the set of roots of g is that f divides f.derivative * g. Over an integral domain, this is a sufficient but not necessary condition. See isRoot_of_isRoot_of_dvd_derivative_mul