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 saying k is an algebraically closed field, i.e. every polynomial in k splits.
IsAlgClosure R K is the typeclass saying K is an algebraic closure of R, where R is a commutative ring. This means that the map from R to K is injective, and K is algebraically closed and algebraic over R
IsAlgClosed.lift is a map from an algebraic extension L of R, into any algebraically closed extension of R.
IsAlgClosure.equiv is a proof that any two algebraic closures of the same field are isomorphic.

Tags #

algebraic closure, algebraically closed

source

class IsAlgClosed (k : Type u) [Field k] :

Prop

splits : ∀ (p : Polynomial k), Polynomial.Splits (RingHom.id k) p

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.

Instances

source

theorem IsAlgClosed.splits_codomain {k : Type u_1} {K : Type u_2} [Field k] [IsAlgClosed k] [Field K] {f : K →+* k} (p : Polynomial K) :

Polynomial.Splits f p

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.

source

theorem IsAlgClosed.splits_domain {k : Type u_1} {K : Type u_2} [Field k] [IsAlgClosed k] [Field K] {f : k →+* K} (p : Polynomial k) :

Polynomial.Splits f p

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.

source

theorem IsAlgClosed.exists_root {k : Type u} [Field k] [IsAlgClosed k] (p : Polynomial k) (hp : Polynomial.degree p ≠ 0) :

∃ x, Polynomial.IsRoot p x

source

theorem IsAlgClosed.exists_pow_nat_eq {k : Type u} [Field k] [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) :

∃ z, z ^ n = x

source

theorem IsAlgClosed.exists_eq_mul_self {k : Type u} [Field k] [IsAlgClosed k] (x : k) :

∃ z, x = z * z

source

theorem IsAlgClosed.roots_eq_zero_iff {k : Type u} [Field k] [IsAlgClosed k] {p : Polynomial k} :

Polynomial.roots p = 0 ↔ p = ↑Polynomial.C (Polynomial.coeff p 0)

source

theorem IsAlgClosed.exists_eval₂_eq_zero_of_injective {k : Type u} [Field k] {R : Type u_1} [Ring R] [IsAlgClosed k] (f : R →+* k) (hf : Function.Injective ↑f) (p : Polynomial R) (hp : Polynomial.degree p ≠ 0) :

∃ x, Polynomial.eval₂ f x p = 0

source

theorem IsAlgClosed.exists_eval₂_eq_zero {k : Type u} [Field k] {R : Type u_1} [Field R] [IsAlgClosed k] (f : R →+* k) (p : Polynomial R) (hp : Polynomial.degree p ≠ 0) :

∃ x, Polynomial.eval₂ f x p = 0

source

theorem IsAlgClosed.exists_aeval_eq_zero_of_injective (k : Type u) [Field k] {R : Type u_1} [CommRing R] [IsAlgClosed k] [Algebra R k] (hinj : Function.Injective ↑(algebraMap R k)) (p : Polynomial R) (hp : Polynomial.degree p ≠ 0) :

∃ x, ↑(Polynomial.aeval x) p = 0

source

theorem IsAlgClosed.exists_aeval_eq_zero (k : Type u) [Field k] {R : Type u_1} [Field R] [IsAlgClosed k] [Algebra R k] (p : Polynomial R) (hp : Polynomial.degree p ≠ 0) :

∃ x, ↑(Polynomial.aeval x) p = 0

source

theorem IsAlgClosed.of_exists_root (k : Type u) [Field k] (H : ∀ (p : Polynomial k), Polynomial.Monic p → Irreducible p → ∃ x, Polynomial.eval x p = 0) :

IsAlgClosed k

source

theorem IsAlgClosed.of_ringEquiv (k : Type u) [Field k] (k' : Type u) [Field k'] (e : k ≃+* k') [IsAlgClosed k] :

IsAlgClosed k'

source

theorem IsAlgClosed.degree_eq_one_of_irreducible (k : Type u) [Field k] [IsAlgClosed k] {p : Polynomial k} (hp : Irreducible p) :

Polynomial.degree p = 1

source

theorem IsAlgClosed.algebraMap_surjective_of_isIntegral {k : Type u_1} {K : Type u_2} [Field k] [Ring K] [IsDomain K] [hk : IsAlgClosed k] [Algebra k K] (hf : Algebra.IsIntegral k K) :

Function.Surjective ↑(algebraMap k K)

source

theorem IsAlgClosed.algebraMap_surjective_of_isIntegral' {k : Type u_1} {K : Type u_2} [Field k] [CommRing K] [IsDomain K] [IsAlgClosed k] (f : k →+* K) (hf : RingHom.IsIntegral f) :

Function.Surjective ↑f

source

theorem IsAlgClosed.algebraMap_surjective_of_isAlgebraic {k : Type u_1} {K : Type u_2} [Field k] [Ring K] [IsDomain K] [IsAlgClosed k] [Algebra k K] (hf : Algebra.IsAlgebraic k K) :

Function.Surjective ↑(algebraMap k K)

source

class IsAlgClosure (R : Type u) (K : Type v) [CommRing R] [Field K] [Algebra R K] [NoZeroSMulDivisors R K] :

Prop

alg_closed : IsAlgClosed K
algebraic : Algebra.IsAlgebraic R K

Typeclass for an extension being an algebraic closure.

Instances

source

theorem isAlgClosure_iff (k : Type u) [Field k] (K : Type v) [Field K] [Algebra k K] :

IsAlgClosure k K ↔ IsAlgClosed K ∧ Algebra.IsAlgebraic k K

source

instance IsAlgClosure.normal (R : Type u_1) (K : Type u_2) [Field R] [Field K] [Algebra R K] [IsAlgClosure R K] :

Normal R K

Equations

IsAlgClosure.normal = IsAlgClosure.normal.proof_1

source

instance IsAlgClosure.separable (R : Type u_1) (K : Type u_2) [Field R] [Field K] [Algebra R K] [IsAlgClosure R K] [CharZero R] :

IsSeparable R K

Equations

IsAlgClosure.separable = IsAlgClosure.separable.proof_1

source

structure IsAlgClosed.lift.SubfieldWithHom (K : Type u) (L : Type v) (M : Type w) [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] :

Type (max v w)

carrier : Subalgebra K L
The corresponding Subalgebra
emb : { x // x ∈ s.carrier } →ₐ[K] M
The embedding into the algebraically closed field

This structure is used to prove the existence of a homomorphism from any algebraic extension into an algebraic closure

Instances For

source

instance IsAlgClosed.lift.SubfieldWithHom.instLESubfieldWithHom {K : Type u} {L : Type v} {M : Type w} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] :

LE (IsAlgClosed.lift.SubfieldWithHom K L M)

Equations

IsAlgClosed.lift.SubfieldWithHom.instLESubfieldWithHom = { le := fun E₁ E₂ => ∃ h, ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(Subalgebra.inclusion h) x) = ↑E₁.emb x }

source

noncomputable instance IsAlgClosed.lift.SubfieldWithHom.instInhabitedSubfieldWithHom {K : Type u} {L : Type v} {M : Type w} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] :

Inhabited (IsAlgClosed.lift.SubfieldWithHom K L M)

Equations

IsAlgClosed.lift.SubfieldWithHom.instInhabitedSubfieldWithHom = { default := { carrier := ⊥, emb := AlgHom.comp (Algebra.ofId K M) ↑(Algebra.botEquiv K L) } }

source

theorem IsAlgClosed.lift.SubfieldWithHom.le_def {K : Type u} {L : Type v} {M : Type w} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] {E₁ : IsAlgClosed.lift.SubfieldWithHom K L M} {E₂ : IsAlgClosed.lift.SubfieldWithHom K L M} :

E₁ ≤ E₂ ↔ ∃ h, ∀ (x : { x // x ∈ E₁.carrier }), ↑E₂.emb (↑(Subalgebra.inclusion h) x) = ↑E₁.emb x

source

theorem IsAlgClosed.lift.SubfieldWithHom.compat {K : Type u} {L : Type v} {M : Type w} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] {E₁ : IsAlgClosed.lift.SubfieldWithHom K L M} {E₂ : IsAlgClosed.lift.SubfieldWithHom K L M} (h : E₁ ≤ E₂) (x : { x // x ∈ E₁.carrier }) :

↑E₂.emb (↑(Subalgebra.inclusion (_ : E₁.carrier ≤ E₂.carrier)) x) = ↑E₁.emb x

source

instance IsAlgClosed.lift.SubfieldWithHom.instPreorderSubfieldWithHom {K : Type u} {L : Type v} {M : Type w} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] :

Preorder (IsAlgClosed.lift.SubfieldWithHom K L M)

Equations

One or more equations did not get rendered due to their size.

source

theorem IsAlgClosed.lift.SubfieldWithHom.maximal_subfieldWithHom_chain_bounded {K : Type u} {L : Type v} {M : Type w} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] (c : Set (IsAlgClosed.lift.SubfieldWithHom K L M)) (hc : IsChain (fun x x_1 => x ≤ x_1) c) :

∃ ub, ∀ (N : IsAlgClosed.lift.SubfieldWithHom K L M), N ∈ c → N ≤ ub

source

theorem IsAlgClosed.lift.SubfieldWithHom.exists_maximal_subfieldWithHom (K : Type u) (L : Type v) (M : Type w) [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] :

∃ E, ∀ (N : IsAlgClosed.lift.SubfieldWithHom K L M), E ≤ N → N ≤ E

source

noncomputable def IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom (K : Type u) (L : Type v) (M : Type w) [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] :

IsAlgClosed.lift.SubfieldWithHom K L M

The maximal SubfieldWithHom. We later prove that this is equal to ⊤.

Equations

IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom K L M = Classical.choose (_ : ∃ E, ∀ (N : IsAlgClosed.lift.SubfieldWithHom K L M), E ≤ N → N ≤ E)

Instances For

source

theorem IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_is_maximal (K : Type u) (L : Type v) (M : Type w) [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] (N : IsAlgClosed.lift.SubfieldWithHom K L M) :

IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom K L M ≤ N → N ≤ IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom K L M

source

noncomputable def Algebra.adjoin.liftSingleton (R : Type u_1) [Field R] {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (x : S) (y : T) (h : ↑(Polynomial.aeval y) (minpoly R x) = 0) :

{ x_1 // x_1 ∈ Algebra.adjoin R {x} } →ₐ[R] T

Produce an algebra homomorphism Adjoin R {x} →ₐ[R] T sending x to a root of x's minimal polynomial in T.

Equations

Algebra.adjoin.liftSingleton R x y h = AlgHom.comp (AdjoinRoot.liftHom (minpoly R x) y h) ↑(AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly R x)

Instances For

source

theorem IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom_eq_top (K : Type u) (L : Type v) (M : Type w) [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [IsAlgClosed M] {hL : Algebra.IsAlgebraic K L} :

(IsAlgClosed.lift.SubfieldWithHom.maximalSubfieldWithHom K L M).carrier = ⊤

source

@[irreducible]

noncomputable def IsAlgClosed.lift {M : Type u_1} [Field M] [IsAlgClosed M] {R : Type u_2} [CommRing R] {S : Type u_3} [CommRing S] [IsDomain S] [Algebra R S] [Algebra R M] [NoZeroSMulDivisors R S] [NoZeroSMulDivisors R M] (hS : Algebra.IsAlgebraic R S) :

S →ₐ[R] M

A (random) homomorphism from an algebraic extension of R into an algebraically closed extension of R.

Equations

@IsAlgClosed.lift = IsAlgClosed.wrapped✝.1

Instances For

source

theorem IsAlgClosed.lift_def {M : Type u_1} [Field M] [IsAlgClosed M] {R : Type u_2} [CommRing R] {S : Type u_3} [CommRing S] [IsDomain S] [Algebra R S] [Algebra R M] [NoZeroSMulDivisors R S] [NoZeroSMulDivisors R M] (hS : Algebra.IsAlgebraic R S) :

IsAlgClosed.lift hS = let_fun this := (_ : IsScalarTower R (FractionRing R) M); let_fun this_1 := (_ : IsScalarTower R (FractionRing R) (FractionRing S)); let_fun this_2 := (_ : Algebra.IsAlgebraic (FractionRing R) (FractionRing S)); let f := IsAlgClosed.lift_aux (FractionRing R) (FractionRing S) M this_2; AlgHom.comp (AlgHom.restrictScalars R f) (AlgHom.restrictScalars R (Algebra.ofId S (FractionRing S)))

source

noncomputable instance IsAlgClosed.perfectRing (k : Type u) [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] [IsAlgClosed k] :

PerfectRing k p

Equations

IsAlgClosed.perfectRing = IsAlgClosed.perfectRing.proof_1

source

instance IsAlgClosed.instInfinite {K : Type u_1} [Field K] [IsAlgClosed K] :

Infinite K

Algebraically closed fields are infinite since Xⁿ⁺¹ - 1 is separable when #K = n

Equations

@IsAlgClosed.instInfinite = @IsAlgClosed.instInfinite.proof_1

source

noncomputable def IsAlgClosure.equiv (R : Type u) [CommRing R] (L : Type v) (M : Type w) [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra R L] [NoZeroSMulDivisors R L] [IsAlgClosure R L] :

L ≃ₐ[R] M

A (random) isomorphism between two algebraic closures of R.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem IsAlgClosure.ofAlgebraic (K : Type u_1) (J : Type u_2) (L : Type v) [Field K] [Field J] [Field L] [Algebra K J] [Algebra J L] [IsAlgClosure J L] [Algebra K L] [IsScalarTower K J L] (hKJ : Algebra.IsAlgebraic K J) :

IsAlgClosure K L

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.

source

noncomputable def IsAlgClosure.equivOfAlgebraic' (R : Type u) (S : Type u_3) (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] [Algebra R S] [Algebra R L] [IsScalarTower R S L] [Nontrivial S] [NoZeroSMulDivisors R S] (hRL : Algebra.IsAlgebraic R L) :

L ≃ₐ[R] M

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 hRL = IsAlgClosure.equiv R L M

Instances For

source

noncomputable def IsAlgClosure.equivOfAlgebraic (K : Type u_1) (J : Type u_2) (L : Type v) (M : Type w) [Field K] [Field J] [Field L] [Field M] [Algebra K M] [IsAlgClosure K M] [Algebra K J] [Algebra J L] [IsAlgClosure J L] [Algebra K L] [IsScalarTower K J L] (hKJ : Algebra.IsAlgebraic K J) :

L ≃ₐ[K] M

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 hKJ = IsAlgClosure.equivOfAlgebraic' K J L M (_ : Algebra.IsAlgebraic K L)

Instances For

source

noncomputable def IsAlgClosure.equivOfEquivAux {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) :

{ e // RingHom.comp (RingEquiv.toRingHom e) (algebraMap S L) = RingHom.comp (algebraMap R M) (RingEquiv.toRingHom hSR) }

Used in the definition of equivOfEquiv

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def IsAlgClosure.equivOfEquiv {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) :

L ≃+* M

Algebraic closure of isomorphic fields are isomorphic

Equations

IsAlgClosure.equivOfEquiv L M hSR = ↑(IsAlgClosure.equivOfEquivAux L M hSR)

Instances For

source

@[simp]

theorem IsAlgClosure.equivOfEquiv_comp_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) :

RingHom.comp (↑(IsAlgClosure.equivOfEquiv L M hSR)) (algebraMap S L) = RingHom.comp (algebraMap R M) ↑hSR

source

@[simp]

theorem IsAlgClosure.equivOfEquiv_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) (s : S) :

↑(IsAlgClosure.equivOfEquiv L M hSR) (↑(algebraMap S L) s) = ↑(algebraMap R M) (↑hSR s)

source

@[simp]

theorem IsAlgClosure.equivOfEquiv_symm_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) (r : R) :

↑(RingEquiv.symm (IsAlgClosure.equivOfEquiv L M hSR)) (↑(algebraMap R M) r) = ↑(algebraMap S L) (↑(RingEquiv.symm hSR) r)

source

@[simp]

theorem IsAlgClosure.equivOfEquiv_symm_comp_algebraMap {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [CommRing R] [CommRing S] [Field L] [Field M] [Algebra R M] [NoZeroSMulDivisors R M] [IsAlgClosure R M] [Algebra S L] [NoZeroSMulDivisors S L] [IsAlgClosure S L] (hSR : S ≃+* R) :

RingHom.comp (↑(RingEquiv.symm (IsAlgClosure.equivOfEquiv L M hSR))) (algebraMap R M) = RingHom.comp (algebraMap S L) ↑(RingEquiv.symm hSR)

source

theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly {F : Type u_1} {K : Type u_2} (A : Type u_3) [Field F] [Field K] [Field A] [IsAlgClosed A] [Algebra F K] (hK : Algebra.IsAlgebraic F K) [Algebra F A] (x : K) :

(Set.range fun ψ => ↑ψ x) = Polynomial.rootSet (minpoly F x) A

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.