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.

Instances
theorem polynomial.splits' {k : Type u_1} {K : Type u_2} [field k] [is_alg_closed k] [field K] {f : k →+* K} (p : polynomial k) :

theorem is_alg_closed.of_exists_root (k : Type u) [field k] :
(∀ (p : polynomial k), p.monicirreducible p(∃ (x : k), polynomial.eval x p = 0))is_alg_closed k

theorem is_alg_closed.degree_eq_one_of_irreducible (k : Type u) [field k] [is_alg_closed k] {p : polynomial k} :
p 0irreducible pp.degree = 1

@[class]
def 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.

Equations
Instances
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] :
(Σ (α : 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] :
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)} :
f.monicirreducible f(∃ (x : algebraic_closure k), polynomial.eval x f = 0)

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

Equations