mathlib documentation

field_theory.is_alg_closed.algebraic_closure

Algebraic Closure #

In this file we construct the algebraic closure of a field

Main Definitions #

Tags #

algebraic closure, algebraically closed

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) :
@[instance]
def algebraic_closure.algebra (k : Type u) [field k] {R : Type u_1} [comm_semiring R] [alg : algebra R k] :
Equations
theorem algebraic_closure.algebra_map_def (k : Type u) [field k] {R : Type u_1} [comm_semiring R] [alg : algebra R k] :
@[instance]
def algebraic_closure.is_scalar_tower (k : Type u) [field k] {R : Type u_1} {S : Type u_2} [comm_semiring R] [comm_semiring S] [algebra R S] [algebra S k] [algebra R k] [is_scalar_tower R S k] :

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

Equations