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 #

TODO #

Show that any two algebraic closures are isomorphic

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 : 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) :
∃ (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.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.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 : polynomial k} (h_nz : p 0) (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 (k : Type u) [field k] (K : Type v) [field K] [algebra k 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] :
theorem exists_spectrum_of_is_alg_closed_of_finite_dimensional (𝕜 : Type u_1) [field 𝕜] [is_alg_closed 𝕜] {A : Type u_2} [nontrivial A] [ring A] [algebra 𝕜 A] [I : finite_dimensional 𝕜 A] (f : A) :
∃ (c : 𝕜), ¬is_unit (f - (algebra_map 𝕜 A) c)

Every element f in a nontrivial finite-dimensional algebra A over an algebraically closed field K has non-empty spectrum: that is, there is some c : K so f - c • 1 is not invertible.

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

@[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
@[instance]
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
@[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 : zorn.chain has_le.le c) (hcn : c.nonempty) :
∃ (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
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
def is_alg_closed.lift (K : Type u) [field K] (L : Type v) (M : Type w) [field L] [algebra K L] [field M] [algebra K M] [is_alg_closed M] (hL : algebra.is_algebraic K L) :

A (random) hom from an algebraic extension of K into an algebraically closed extension of K

Equations
def is_alg_closure.equiv (K : Type u) [field K] (L : Type v) (M : Type w) [field L] [field M] [algebra K M] [is_alg_closure K M] [algebra K L] [is_alg_closure K L] :

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

Equations
def is_alg_closure.equiv_of_algebraic (J : Type u_1) (K : Type u) [field J] [field K] (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) :

An equiv between an algebraic closure of K and an algebraic closure of an algebraic extension of K

Equations
def is_alg_closure.equiv_of_equiv_aux {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [algebra K M] [is_alg_closure K M] [algebra J L] [is_alg_closure J L] (hJK : J ≃+* K) :

Used in the definition of equiv_of_equiv

Equations
def is_alg_closure.equiv_of_equiv {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [algebra K M] [is_alg_closure K M] [algebra J L] [is_alg_closure J L] (hJK : J ≃+* K) :
L ≃+* M

Algebraic closure of isomorphic fields are isomorphic

Equations
@[simp]
theorem is_alg_closure.equiv_of_equiv_comp_algebra_map {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [algebra K M] [is_alg_closure K M] [algebra J L] [is_alg_closure J L] (hJK : J ≃+* K) :
@[simp]
theorem is_alg_closure.equiv_of_equiv_algebra_map {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [algebra K M] [is_alg_closure K M] [algebra J L] [is_alg_closure J L] (hJK : J ≃+* K) (j : J) :
@[simp]
theorem is_alg_closure.equiv_of_equiv_symm_algebra_map {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [algebra K M] [is_alg_closure K M] [algebra J L] [is_alg_closure J L] (hJK : J ≃+* K) (k : K) :
@[simp]
theorem is_alg_closure.equiv_of_equiv_symm_comp_algebra_map {J : Type u_1} {K : Type u} [field J] [field K] (L : Type v) (M : Type w) [field L] [field M] [algebra K M] [is_alg_closure K M] [algebra J L] [is_alg_closure J L] (hJK : J ≃+* K) :