Algebraic Closure #
In this file we construct the algebraic closure of a field
Main Definitions #
AlgebraicClosure k
is an algebraic closure ofk
(in the same universe). It is constructed by taking the polynomial ring generated by indeterminatesx_f
corresponding to monic irreducible polynomialsf
with coefficients ink
, and quotienting out by a maximal ideal containing everyf(x_f)
, and then repeating this step countably many times. See Exercise 1.13 in Atiyah--Macdonald.
Tags #
algebraic closure, algebraically closed
The subtype of monic irreducible polynomials
Equations
- AlgebraicClosure.MonicIrreducible k = { f : Polynomial k // f.Monic ∧ Irreducible f }
Instances For
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
Instances For
The span of f(x_f)
across monic irreducible polynomials f
where x_f
is an
indeterminate.
Equations
Instances For
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.
Instances For
A random maximal ideal that contains spanEval k
Equations
Instances For
Equations
- ⋯ = ⋯
The first step of constructing AlgebraicClosure
: adjoin a root of all monic polynomials
Equations
Instances For
Equations
- AlgebraicClosure.AdjoinMonic.inhabited k = { default := 37 }
The canonical ring homomorphism to AdjoinMonic k
.
Equations
- AlgebraicClosure.toAdjoinMonic k = (Ideal.Quotient.mk (AlgebraicClosure.maxIdeal k)).comp MvPolynomial.C
Instances For
Equations
- AlgebraicClosure.AdjoinMonic.algebra k = (AlgebraicClosure.toAdjoinMonic k).toAlgebra
The n
th 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⟩
Instances For
The n
th step of constructing AlgebraicClosure
.
Equations
- AlgebraicClosure.Step k n = (AlgebraicClosure.stepAux k n).fst
Instances For
Equations
- AlgebraicClosure.Step.field k n = (AlgebraicClosure.stepAux k n).snd
Equations
- AlgebraicClosure.Step.inhabited k n = { default := 37 }
The canonical inclusion to the 0
th step.
Equations
Instances For
The canonical ring homomorphism to the next step.
Equations
Instances For
Equations
- AlgebraicClosure.Step.algebraSucc k n = (AlgebraicClosure.toStepSucc k n).toAlgebra
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' := ⋯ }
Instances For
Equations
- AlgebraicClosure.Step.algebra k n = (AlgebraicClosure.toStepOfLE k 0 n ⋯).toAlgebra
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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)
Instances For
Equations
- AlgebraicClosureAux.instInhabited k = { default := 37 }
The canonical ring embedding from the n
th 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
Instances For
AlgebraicClosureAux k
is a k
-Algebra
Equations
- AlgebraicClosureAux.instAlgebra k = (AlgebraicClosureAux.ofStep k 0).toAlgebra
Instances For
Canonical algebra embedding from the n
th step to the algebraic closure.
Equations
- AlgebraicClosureAux.ofStepHom k n = { toRingHom := AlgebraicClosureAux.ofStep k n, commutes' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
The canonical algebraic closure of a field, the direct limit of adding roots to the field for each polynomial over the field.
Equations
- AlgebraicClosure k = (MvPolynomial (AlgebraicClosureAux k) k ⧸ RingHom.ker (MvPolynomial.aeval id).toRingHom)
Instances For
Equations
- AlgebraicClosure.instCommRing k = Ideal.Quotient.commRing (RingHom.ker (MvPolynomial.aeval id).toRingHom)
Equations
- AlgebraicClosure.instInhabited k = { default := 37 }
Equations
Equations
Equations
- ⋯ = ⋯
The equivalence between AlgebraicClosure
and AlgebraicClosureAux
, which we use to transfer
properties of AlgebraicClosureAux
to AlgebraicClosure
Equations
Instances For
Equations
- AlgebraicClosure.instGroupWithZero k = GroupWithZero.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- AlgebraicClosure.instField k = Field.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x1 : ℚ≥0) (x2 : AlgebraicClosure k) => x1 • x2) ⋯ ⋯ (fun (x1 : ℚ) (x2 : AlgebraicClosure k) => x1 • x2) ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯