mathlib documentation

field_theory.is_alg_closed.basic

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 #

Tags #

algebraic closure, algebraically closed

@[class]
structure is_alg_closed (k : Type u) [field k] :
Prop

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
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 : K[X]) :

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 : k[X]) :

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 : k[X]) (hp : p.degree 0) :
∃ (x : k), p.is_root x
theorem is_alg_closed.exists_pow_nat_eq {k : Type u} [field k] [is_alg_closed k] (x : k) {n : } (hn : 0 < n) :
∃ (z : k), z ^ n = x
theorem is_alg_closed.exists_eq_mul_self {k : Type u} [field k] [is_alg_closed k] (x : k) :
∃ (z : k), x = z * z
theorem is_alg_closed.roots_eq_zero_iff {k : Type u} [field k] [is_alg_closed k] {p : k[X]} :
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 : R[X]) (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 : R[X]) (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 : R[X]) (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 : R[X]) (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 : k[X]), p.monicirreducible 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 : k[X]} (hp : irreducible p) :
p.degree = 1
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) :
@[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

Typeclass for an extension being an algebraic closure.

Instances
theorem is_alg_closure_iff (k : Type u) [field k] (K : Type v) [field K] [algebra k 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)

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

@[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} :
Equations
@[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} :
Equations
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} :
E₁ E₂ ∃ (h : E₁.carrier E₂.carrier), ∀ (x : (E₁.carrier)), (E₂.emb) ((subalgebra.inclusion h) x) = (E₁.emb) x
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)) :
(E₂.emb) ((subalgebra.inclusion _) x) = (E₁.emb) x
@[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} :
Equations
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 cN 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 NN 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) :

The maximal subfield_with_hom. We later prove that this is equal to .

Equations
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
@[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] :
Equations
@[protected, instance]
def is_alg_closed.infinite {K : Type u_1} [field K] [is_alg_closed K] :

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
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
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
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) :

Used in the definition of equiv_of_equiv

Equations
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
@[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) :
@[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) :
@[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) :
@[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) :