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]

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

The subtype of monic irreducible polynomials

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.

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.

def AlgebraicClosure.toSplittingField (k : Type u) [Field k] (s : Finset (AlgebraicClosure.MonicIrreducible k)) : MvPolynomial (AlgebraicClosure.MonicIrreducible k) k →ₐ[k] Polynomial.SplittingField (Finset.prod s fun x => ↑x)

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.

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

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

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

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

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

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

The canonical ring homomorphism to AdjoinMonic k.

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

theorem AlgebraicClosure.AdjoinMonic.algebraMap (k : Type u) [Field k] : algebraMap k (AlgebraicClosure.AdjoinMonic k) = RingHom.comp (Ideal.Quotient.mk (AlgebraicClosure.maxIdeal k)) 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 : Polynomial.Monic f) (hfi : Irreducible f) : ∃ x, 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.

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

The nth step of constructing AlgebraicClosure.

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)

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)

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

The canonical inclusion to the 0th step.

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.

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

theorem AlgebraicClosure.toStepSucc.exists_root (k : Type u) [Field k] {n : ℕ} {f : Polynomial (AlgebraicClosure.Step k n)} (hfm : Polynomial.Monic f) (hfi : Irreducible f) : ∃ x, 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.

@[simp]

theorem AlgebraicClosure.coe_toStepOfLE (k : Type u) [Field k] (m : ℕ) (n : ℕ) (h : m ≤ n) : ↑(AlgebraicClosure.toStepOfLE k m n h) = fun a => 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)

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

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 => ↑(AlgebraicClosure.toStepOfLE k i j h)

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.

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

AlgebraicClosureAux k is a Field

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

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.

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

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

theorem AlgebraicClosureAux.exists_root (k : Type u) [Field k] {f : Polynomial (AlgebraicClosureAux k)} (hfm : Polynomial.Monic f) (hfi : Irreducible f) : ∃ x, 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

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.

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

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.

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

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

instance AlgebraicClosure.instSMulAlgebraicClosure (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.instIsScalarTowerAlgebraicClosureToSMulToSemiringInstSMulAlgebraicClosureToDistribSMulToMonoidToMonoidWithZeroToAddMonoidToAddMonoidWithOneToAddGroupWithOneToRingToDivisionRingToDistribMulActionToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToModuleToSemiringToDivisionSemiringToSemifieldRightInstSMulAlgebraicClosureToDistribSMulToMonoidToMonoidWithZeroToSemiringToDistribMulActionToModuleRight (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)

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

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

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

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

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

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

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