Algebraically Closed Field #
In this file we define the typeclass for algebraically closed fields and algebraic closures, and prove some of their properties.
Main Definitions #
IsAlgClosed k
is the typeclass sayingk
is an algebraically closed field, i.e. every polynomial ink
splits.IsAlgClosure R K
is the typeclass sayingK
is an algebraic closure ofR
, whereR
is a commutative ring. This means that the map fromR
toK
is injective, andK
is algebraically closed and algebraic overR
IsAlgClosed.lift
is a map from an algebraic extensionL
ofR
, into any algebraically closed extension ofR
.IsAlgClosure.equiv
is a proof that any two algebraic closures of the same field are isomorphic.
Tags #
algebraic closure, algebraically closed
Main reults #
IsAlgClosure.of_splits
: ifK / k
is algebraic, and every monic irreducible polynomial overk
splits inK
, thenK
is algebraically closed (in fact an algebraic closure ofk
). For the stronger fact that only requires every such polynomial has a root inK
, seeIsAlgClosure.of_exist_roots
.Reference: https://kconrad.math.uconn.edu/blurbs/galoistheory/algclosure.pdf, Theorem 2
Typeclass for algebraically closed fields.
To show Polynomial.Splits p f
for an arbitrary ring homomorphism f
,
see IsAlgClosed.splits_codomain
and IsAlgClosed.splits_domain
.
Stacks Tag 09GR (The definition of IsAlgClosed
in mathlib is 09GR (4))
- splits : ∀ (p : Polynomial k), Polynomial.Splits (RingHom.id k) p
Instances
Every polynomial splits in the field extension f : K →+* k
if k
is algebraically closed.
See also IsAlgClosed.splits_domain
for the case where K
is algebraically closed.
Every polynomial splits in the field extension f : K →+* k
if K
is algebraically closed.
See also IsAlgClosed.splits_codomain
for the case where k
is algebraically closed.
If k
is algebraically closed, then every nonconstant polynomial has a root.
Stacks Tag 09GR ((4) ⟹ (3))
If every nonconstant polynomial over k
has a root, then k
is algebraically closed.
Stacks Tag 09GR ((3) ⟹ (4))
If k
is algebraically closed, then every irreducible polynomial over k
is linear.
Stacks Tag 09GR ((4) ⟹ (2))
Deprecated: algebraMap_surjective_of_isIntegral
is identical apart from the IsIntegral
argument,
which can be found by instance synthesis
If k
is algebraically closed, K / k
is a field extension, L / k
is an intermediate field
which is algebraic, then L
is equal to k
. A corollary of
IsAlgClosed.algebraMap_surjective_of_isAlgebraic
.
Stacks Tag 09GQ (The result is the definition of algebraically closedness in Stacks Project. This statement is 09GR (4) ⟹ (1).)
Typeclass for an extension being an algebraic closure.
- isAlgClosed : IsAlgClosed K
- isAlgebraic : Algebra.IsAlgebraic R K
Instances
Alias of IsAlgClosure.isAlgClosed
.
Alias of IsAlgClosure.isAlgebraic
.
If E/L/K is a tower of field extensions with E/L algebraic, and if M is an algebraically closed extension of K, then any embedding of L/K into M/K extends to an embedding of E/K. Known as the extension lemma in https://math.stackexchange.com/a/687914.
Alias of IsAlgClosed.surjective_restrictDomain_of_isAlgebraic
.
If E/L/K is a tower of field extensions with E/L algebraic, and if M is an algebraically closed extension of K, then any embedding of L/K into M/K extends to an embedding of E/K. Known as the extension lemma in https://math.stackexchange.com/a/687914.
A (random) homomorphism from an algebraic extension of R into an algebraically closed extension of R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Algebraically closed fields are infinite since Xⁿ⁺¹ - 1
is separable when #K = n
A (random) isomorphism between two algebraic closures of R
.
Equations
- IsAlgClosure.equiv R L M = AlgEquiv.ofBijective IsAlgClosed.lift ⋯
Instances For
If J
is an algebraic extension of K
and L
is an algebraic closure of J
, then it is
also an algebraic closure of K
.
A (random) isomorphism between an algebraic closure of R
and an algebraic closure of
an algebraic extension of R
Equations
- IsAlgClosure.equivOfAlgebraic' R S L M = IsAlgClosure.equiv R L M
Instances For
A (random) isomorphism between an algebraic closure of K
and an algebraic closure
of an algebraic extension of K
Equations
- IsAlgClosure.equivOfAlgebraic K J L M = IsAlgClosure.equivOfAlgebraic' K J L M
Instances For
Used in the definition of equivOfEquiv
Equations
- IsAlgClosure.equivOfEquivAux L M hSR = ⟨↑(IsAlgClosure.equivOfAlgebraic' R S L M), ⋯⟩
Instances For
Algebraic closure of isomorphic fields are isomorphic
Equations
- IsAlgClosure.equivOfEquiv L M hSR = ↑(IsAlgClosure.equivOfEquivAux L M hSR)
Instances For
Let A
be an algebraically closed field and let x ∈ K
, with K/F
an algebraic extension
of fields. Then the images of x
by the F
-algebra morphisms from K
to A
are exactly
the roots in A
of the minimal polynomial of x
over F
.
All F
-embeddings of a field K
into another field A
factor through any intermediate
field of A/F
in which the minimal polynomial of elements of K
splits.
Equations
- IntermediateField.algHomEquivAlgHomOfSplits A L hL = { toFun := L.val.comp, invFun := fun (f : K →ₐ[F] A) => f.codRestrict L.toSubalgebra ⋯, left_inv := ⋯, right_inv := ⋯ }
Instances For
All F
-embeddings of a field K
into another field A
factor through any subextension
of A/F
in which the minimal polynomial of elements of K
splits.
Equations
- One or more equations did not get rendered due to their size.