Algebraically Closed Field #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define the typeclass for algebraically closed fields and algebraic closures, and prove some of their properties.
Main Definitions #
-
is_alg_closed kis the typeclass sayingkis an algebraically closed field, i.e. every polynomial inksplits. -
is_alg_closure R Kis the typeclass sayingKis an algebraic closure ofR, whereRis a commutative ring. This means that the map fromRtoKis injective, andKis algebraically closed and algebraic overR -
is_alg_closed.liftis a map from an algebraic extensionLofR, into any algebraically closed extension ofR. -
is_alg_closure.equivis a proof that any two algebraic closures of the same field are isomorphic.
Tags #
algebraic closure, algebraically closed
@[class]
- splits : ∀ (p : polynomial k), polynomial.splits (ring_hom.id k) p
Typeclass for algebraically closed fields.
To show polynomial.splits p f for an arbitrary ring homomorphism f,
see is_alg_closed.splits_codomain and is_alg_closed.splits_domain.
Instances of this typeclass
theorem
is_alg_closed.splits_codomain
{k : Type u_1}
{K : Type u_2}
[field k]
[is_alg_closed k]
[field K]
{f : K →+* k}
(p : polynomial K) :
Every polynomial splits in the field extension f : K →+* k if k is algebraically closed.
See also is_alg_closed.splits_domain for the case where K is algebraically closed.
theorem
is_alg_closed.splits_domain
{k : Type u_1}
{K : Type u_2}
[field k]
[is_alg_closed k]
[field K]
{f : k →+* K}
(p : polynomial k) :
Every polynomial splits in the field extension f : K →+* k if K is algebraically closed.
See also is_alg_closed.splits_codomain for the case where k is algebraically closed.
theorem
is_alg_closed.exists_root
{k : Type u}
[field k]
[is_alg_closed k]
(p : polynomial k)
(hp : p.degree ≠ 0) :
theorem
is_alg_closed.roots_eq_zero_iff
{k : Type u}
[field k]
[is_alg_closed k]
{p : polynomial k} :
theorem
is_alg_closed.exists_eval₂_eq_zero_of_injective
{k : Type u}
[field k]
{R : Type u_1}
[ring R]
[is_alg_closed k]
(f : R →+* k)
(hf : function.injective ⇑f)
(p : polynomial R)
(hp : p.degree ≠ 0) :
∃ (x : k), polynomial.eval₂ f x p = 0
theorem
is_alg_closed.exists_eval₂_eq_zero
{k : Type u}
[field k]
{R : Type u_1}
[field R]
[is_alg_closed k]
(f : R →+* k)
(p : polynomial R)
(hp : p.degree ≠ 0) :
∃ (x : k), polynomial.eval₂ f x p = 0
theorem
is_alg_closed.exists_aeval_eq_zero_of_injective
(k : Type u)
[field k]
{R : Type u_1}
[comm_ring R]
[is_alg_closed k]
[algebra R k]
(hinj : function.injective ⇑(algebra_map R k))
(p : polynomial R)
(hp : p.degree ≠ 0) :
∃ (x : k), ⇑(polynomial.aeval x) p = 0
theorem
is_alg_closed.exists_aeval_eq_zero
(k : Type u)
[field k]
{R : Type u_1}
[field R]
[is_alg_closed k]
[algebra R k]
(p : polynomial R)
(hp : p.degree ≠ 0) :
∃ (x : k), ⇑(polynomial.aeval x) p = 0
theorem
is_alg_closed.of_exists_root
(k : Type u)
[field k]
(H : ∀ (p : polynomial k), p.monic → irreducible p → (∃ (x : k), polynomial.eval x p = 0)) :
theorem
is_alg_closed.degree_eq_one_of_irreducible
(k : Type u)
[field k]
[is_alg_closed k]
{p : polynomial k}
(hp : irreducible p) :
theorem
is_alg_closed.algebra_map_surjective_of_is_integral
{k : Type u_1}
{K : Type u_2}
[field k]
[ring K]
[is_domain K]
[hk : is_alg_closed k]
[algebra k K]
(hf : algebra.is_integral k K) :
theorem
is_alg_closed.algebra_map_surjective_of_is_integral'
{k : Type u_1}
{K : Type u_2}
[field k]
[comm_ring K]
[is_domain K]
[hk : is_alg_closed k]
(f : k →+* K)
(hf : f.is_integral) :
theorem
is_alg_closed.algebra_map_surjective_of_is_algebraic
{k : Type u_1}
{K : Type u_2}
[field k]
[ring K]
[is_domain K]
[hk : is_alg_closed k]
[algebra k K]
(hf : algebra.is_algebraic k K) :
@[class]
structure
is_alg_closure
(R : Type u)
(K : Type v)
[comm_ring R]
[field K]
[algebra R K]
[no_zero_smul_divisors R K] :
Prop
- alg_closed : is_alg_closed K
- algebraic : algebra.is_algebraic R K
Typeclass for an extension being an algebraic closure.
Instances of this typeclass
theorem
is_alg_closure_iff
(k : Type u)
[field k]
(K : Type v)
[field K]
[algebra k K] :
is_alg_closure k K ↔ is_alg_closed K ∧ algebra.is_algebraic k K
@[protected, instance]
def
is_alg_closure.normal
(R : Type u_1)
(K : Type u_2)
[field R]
[field K]
[algebra R K]
[is_alg_closure R K] :
normal R K
@[protected, instance]
def
is_alg_closure.separable
(R : Type u_1)
(K : Type u_2)
[field R]
[field K]
[algebra R K]
[is_alg_closure R K]
[char_zero R] :
is_separable R K
structure
lift.subfield_with_hom
(K : Type u)
(L : Type v)
(M : Type w)
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
(hL : algebra.is_algebraic K L) :
Type (max v w)
- carrier : subalgebra K L
- emb : ↥(self.carrier) →ₐ[K] M
This structure is used to prove the existence of a homomorphism from any algebraic extension into an algebraic closure
Instances for lift.subfield_with_hom
- lift.subfield_with_hom.has_sizeof_inst
- lift.subfield_with_hom.has_le
- lift.subfield_with_hom.inhabited
- lift.subfield_with_hom.preorder
@[protected, instance]
def
lift.subfield_with_hom.has_le
{K : Type u}
{L : Type v}
{M : Type w}
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
{hL : algebra.is_algebraic K L} :
has_le (lift.subfield_with_hom K L M hL)
@[protected, instance]
noncomputable
def
lift.subfield_with_hom.inhabited
{K : Type u}
{L : Type v}
{M : Type w}
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
{hL : algebra.is_algebraic K L} :
inhabited (lift.subfield_with_hom K L M hL)
Equations
- lift.subfield_with_hom.inhabited = {default := {carrier := ⊥, emb := (algebra.of_id K M).comp (algebra.bot_equiv K L).to_alg_hom}}
theorem
lift.subfield_with_hom.le_def
{K : Type u}
{L : Type v}
{M : Type w}
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
{hL : algebra.is_algebraic K L}
{E₁ E₂ : lift.subfield_with_hom K L M hL} :
theorem
lift.subfield_with_hom.compat
{K : Type u}
{L : Type v}
{M : Type w}
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
{hL : algebra.is_algebraic K L}
{E₁ E₂ : lift.subfield_with_hom K L M hL}
(h : E₁ ≤ E₂)
(x : ↥(E₁.carrier)) :
@[protected, instance]
def
lift.subfield_with_hom.preorder
{K : Type u}
{L : Type v}
{M : Type w}
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
{hL : algebra.is_algebraic K L} :
preorder (lift.subfield_with_hom K L M hL)
Equations
- lift.subfield_with_hom.preorder = {le := has_le.le lift.subfield_with_hom.has_le, lt := λ (a b : lift.subfield_with_hom K L M hL), a ≤ b ∧ ¬b ≤ a, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
theorem
lift.subfield_with_hom.maximal_subfield_with_hom_chain_bounded
{K : Type u}
{L : Type v}
{M : Type w}
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
{hL : algebra.is_algebraic K L}
(c : set (lift.subfield_with_hom K L M hL))
(hc : is_chain has_le.le c) :
∃ (ub : lift.subfield_with_hom K L M hL), ∀ (N : lift.subfield_with_hom K L M hL), N ∈ c → N ≤ ub
theorem
lift.subfield_with_hom.exists_maximal_subfield_with_hom
{K : Type u}
{L : Type v}
(M : Type w)
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
(hL : algebra.is_algebraic K L) :
∃ (E : lift.subfield_with_hom K L M hL), ∀ (N : lift.subfield_with_hom K L M hL), E ≤ N → N ≤ E
noncomputable
def
lift.subfield_with_hom.maximal_subfield_with_hom
{K : Type u}
{L : Type v}
(M : Type w)
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
(hL : algebra.is_algebraic K L) :
lift.subfield_with_hom K L M hL
The maximal subfield_with_hom. We later prove that this is equal to ⊤.
Equations
theorem
lift.subfield_with_hom.maximal_subfield_with_hom_is_maximal
{K : Type u}
{L : Type v}
(M : Type w)
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
(hL : algebra.is_algebraic K L)
(N : lift.subfield_with_hom K L M hL) :
theorem
lift.subfield_with_hom.maximal_subfield_with_hom_eq_top
{K : Type u}
{L : Type v}
(M : Type w)
[field K]
[field L]
[algebra K L]
[field M]
[algebra K M]
[is_alg_closed M]
(hL : algebra.is_algebraic K L) :
@[irreducible]
noncomputable
def
is_alg_closed.lift
{M : Type w}
[field M]
[is_alg_closed M]
{R : Type u}
[comm_ring R]
{S : Type v}
[comm_ring S]
[is_domain S]
[algebra R S]
[algebra R M]
[no_zero_smul_divisors R S]
[no_zero_smul_divisors R M]
(hS : algebra.is_algebraic R S) :
A (random) homomorphism from an algebraic extension of R into an algebraically closed extension of R.
Equations
- is_alg_closed.lift hS = let _inst : is_domain R := is_alg_closed.lift._proof_1, f : fraction_ring S →ₐ[fraction_ring R] M := lift_aux (fraction_ring R) (fraction_ring S) M _ in (alg_hom.restrict_scalars R f).comp (alg_hom.restrict_scalars R (algebra.of_id S (fraction_ring S)))
@[protected, instance]
noncomputable
def
is_alg_closed.perfect_ring
(k : Type u)
[field k]
(p : ℕ)
[fact (nat.prime p)]
[char_p k p]
[is_alg_closed k] :
perfect_ring k p
Equations
@[protected, instance]
Algebraically closed fields are infinite since Xⁿ⁺¹ - 1 is separable when #K = n
noncomputable
def
is_alg_closure.equiv
(R : Type u)
[comm_ring R]
(L : Type v)
(M : Type w)
[field L]
[field M]
[algebra R M]
[no_zero_smul_divisors R M]
[is_alg_closure R M]
[algebra R L]
[no_zero_smul_divisors R L]
[is_alg_closure R L] :
A (random) isomorphism between two algebraic closures of R.
Equations
- is_alg_closure.equiv R L M = let f : L →ₐ[R] M := is_alg_closed.lift is_alg_closure.algebraic in alg_equiv.of_bijective f _
theorem
is_alg_closure.of_algebraic
(K : Type u_1)
(J : Type u_2)
[field K]
[field J]
(L : Type v)
[field L]
[algebra K J]
[algebra J L]
[is_alg_closure J L]
[algebra K L]
[is_scalar_tower K J L]
(hKJ : algebra.is_algebraic K J) :
is_alg_closure 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.
noncomputable
def
is_alg_closure.equiv_of_algebraic'
(R : Type u)
(S : Type u_3)
[comm_ring R]
(L : Type v)
(M : Type w)
[field L]
[field M]
[algebra R M]
[no_zero_smul_divisors R M]
[is_alg_closure R M]
[comm_ring S]
[algebra S L]
[no_zero_smul_divisors S L]
[is_alg_closure S L]
[algebra R S]
[algebra R L]
[is_scalar_tower R S L]
[nontrivial S]
[no_zero_smul_divisors R S]
(hRL : algebra.is_algebraic R L) :
A (random) isomorphism between an algebraic closure of R and an algebraic closure of
an algebraic extension of R
Equations
- is_alg_closure.equiv_of_algebraic' R S L M hRL = let _inst : no_zero_smul_divisors R L := _, _inst_1 : is_alg_closure R L := _ in is_alg_closure.equiv R L M
noncomputable
def
is_alg_closure.equiv_of_algebraic
(K : Type u_1)
(J : Type u_2)
[field K]
[field J]
(L : Type v)
(M : Type w)
[field L]
[field M]
[algebra K M]
[is_alg_closure K M]
[algebra K J]
[algebra J L]
[is_alg_closure J L]
[algebra K L]
[is_scalar_tower K J L]
(hKJ : algebra.is_algebraic K J) :
A (random) isomorphism between an algebraic closure of K and an algebraic closure
of an algebraic extension of K
Equations
- is_alg_closure.equiv_of_algebraic K J L M hKJ = is_alg_closure.equiv_of_algebraic' K J L M _
noncomputable
def
is_alg_closure.equiv_of_equiv_aux
{R : Type u}
{S : Type u_3}
[comm_ring R]
(L : Type v)
(M : Type w)
[field L]
[field M]
[algebra R M]
[no_zero_smul_divisors R M]
[is_alg_closure R M]
[comm_ring S]
[algebra S L]
[no_zero_smul_divisors S L]
[is_alg_closure S L]
(hSR : S ≃+* R) :
{e // e.to_ring_hom.comp (algebra_map S L) = (algebra_map R M).comp hSR.to_ring_hom}
Used in the definition of equiv_of_equiv
Equations
- is_alg_closure.equiv_of_equiv_aux L M hSR = let _inst : algebra R S := hSR.symm.to_ring_hom.to_algebra, _inst_1 : algebra S R := hSR.to_ring_hom.to_algebra, _inst_2 : is_domain R := _, _inst_3 : is_domain S := _, _inst_10 : algebra R L := ((algebra_map S L).comp (algebra_map R S)).to_algebra in ⟨↑(is_alg_closure.equiv_of_algebraic' R S L M _), _⟩
noncomputable
def
is_alg_closure.equiv_of_equiv
{R : Type u}
{S : Type u_3}
[comm_ring R]
(L : Type v)
(M : Type w)
[field L]
[field M]
[algebra R M]
[no_zero_smul_divisors R M]
[is_alg_closure R M]
[comm_ring S]
[algebra S L]
[no_zero_smul_divisors S L]
[is_alg_closure S L]
(hSR : S ≃+* R) :
L ≃+* M
Algebraic closure of isomorphic fields are isomorphic
Equations
- is_alg_closure.equiv_of_equiv L M hSR = ↑(is_alg_closure.equiv_of_equiv_aux L M hSR)
@[simp]
theorem
is_alg_closure.equiv_of_equiv_comp_algebra_map
{R : Type u}
{S : Type u_3}
[comm_ring R]
(L : Type v)
(M : Type w)
[field L]
[field M]
[algebra R M]
[no_zero_smul_divisors R M]
[is_alg_closure R M]
[comm_ring S]
[algebra S L]
[no_zero_smul_divisors S L]
[is_alg_closure S L]
(hSR : S ≃+* R) :
↑(is_alg_closure.equiv_of_equiv L M hSR).comp (algebra_map S L) = (algebra_map R M).comp ↑hSR
@[simp]
theorem
is_alg_closure.equiv_of_equiv_algebra_map
{R : Type u}
{S : Type u_3}
[comm_ring R]
(L : Type v)
(M : Type w)
[field L]
[field M]
[algebra R M]
[no_zero_smul_divisors R M]
[is_alg_closure R M]
[comm_ring S]
[algebra S L]
[no_zero_smul_divisors S L]
[is_alg_closure S L]
(hSR : S ≃+* R)
(s : S) :
⇑(is_alg_closure.equiv_of_equiv L M hSR) (⇑(algebra_map S L) s) = ⇑(algebra_map R M) (⇑hSR s)
@[simp]
theorem
is_alg_closure.equiv_of_equiv_symm_algebra_map
{R : Type u}
{S : Type u_3}
[comm_ring R]
(L : Type v)
(M : Type w)
[field L]
[field M]
[algebra R M]
[no_zero_smul_divisors R M]
[is_alg_closure R M]
[comm_ring S]
[algebra S L]
[no_zero_smul_divisors S L]
[is_alg_closure S L]
(hSR : S ≃+* R)
(r : R) :
⇑((is_alg_closure.equiv_of_equiv L M hSR).symm) (⇑(algebra_map R M) r) = ⇑(algebra_map S L) (⇑(hSR.symm) r)
@[simp]
theorem
is_alg_closure.equiv_of_equiv_symm_comp_algebra_map
{R : Type u}
{S : Type u_3}
[comm_ring R]
(L : Type v)
(M : Type w)
[field L]
[field M]
[algebra R M]
[no_zero_smul_divisors R M]
[is_alg_closure R M]
[comm_ring S]
[algebra S L]
[no_zero_smul_divisors S L]
[is_alg_closure S L]
(hSR : S ≃+* R) :
↑((is_alg_closure.equiv_of_equiv L M hSR).symm).comp (algebra_map R M) = (algebra_map S L).comp ↑(hSR.symm)
theorem
algebra.is_algebraic.range_eval_eq_root_set_minpoly
{F : Type u_1}
{K : Type u_2}
(A : Type u_3)
[field F]
[field K]
[field A]
[is_alg_closed A]
[algebra F K]
(hK : algebra.is_algebraic F K)
[algebra F A]
(x : K) :
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.