mathlib documentation

field_theory.algebraic_closure

Algebraic Closure #

In this file we define the typeclass for algebraically closed fields and algebraic closures. We also construct an algebraic closure for any field.

Main Definitions #

TODO #

Show that any algebraic extension embeds into any algebraically closed extension (via Zorn's lemma).

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.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] [integral_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] :
def algebraic_closure.monic_irreducible (k : Type u) [field k] :
Type u

The subtype of monic irreducible polynomials

Equations

Sends a monic irreducible polynomial f to f(x_f) where x_f is a formal indeterminate.

Equations

The span of f(x_f) across monic irreducible polynomials f where x_f is an indeterminate.

Equations

Given a finset of monic irreducible polynomials, construct an algebra homomorphism to the splitting field of the product of the polynomials sending each indeterminate x_f represented by the polynomial f in the finset to a root of f.

Equations

A random maximal ideal that contains span_eval k

Equations
def algebraic_closure.adjoin_monic (k : Type u) [field k] :
Type u

The first step of constructing algebraic_closure: adjoin a root of all monic polynomials

Equations
def algebraic_closure.step_aux (k : Type u) [field k] (n : ) :
Σ (α : Type u), field α

The nth step of constructing algebraic_closure, together with its field instance.

Equations
def algebraic_closure.step (k : Type u) [field k] (n : ) :
Type u

The nth step of constructing algebraic_closure.

Equations
@[instance]
Equations

The canonical inclusion to the 0th step.

Equations

The canonical ring homomorphism to the next step.

Equations

The canonical ring homomorphism to a step with a greater index.

Equations
@[simp]
theorem algebraic_closure.step.is_integral (k : Type u) [field k] (n : ) (z : algebraic_closure.step k n) :
def algebraic_closure (k : Type u) [field k] :
Type u

The canonical algebraic closure of a field, the direct limit of adding roots to the field for each polynomial over the field.

Equations
@[instance]
Equations

The canonical ring embedding from the nth step to the algebraic closure.

Equations
theorem algebraic_closure.exists_of_step (k : Type u) [field k] (z : algebraic_closure k) :
theorem algebraic_closure.exists_root (k : Type u) [field k] {f : polynomial (algebraic_closure k)} (hfm : f.monic) (hfi : irreducible f) :

Canonical algebra embedding from the nth step to the algebraic closure.

Equations