mathlib3 documentation

field_theory.is_alg_closed.algebraic_closure

Algebraic Closure #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we construct the algebraic closure of a field

Main Definitions #

Tags #

algebraic closure, algebraically closed

@[reducible]

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
Instances for algebraic_closure.max_ideal
noncomputable 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
@[protected, instance]
noncomputable def algebraic_closure.step.field (k : Type u) [field k] (n : ) :
Equations
@[protected, instance]
noncomputable def algebraic_closure.step.inhabited (k : Type u) [field k] (n : ) :
Equations

The canonical inclusion to the 0th step.

Equations

The canonical ring homomorphism to the next step.

Equations
noncomputable def algebraic_closure.to_step_of_le (k : Type u) [field k] (m n : ) (h : m n) :

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

Equations
@[protected, instance]
noncomputable def algebraic_closure.step.algebra (k : Type u) [field k] (n : ) :
Equations
@[protected, instance]
def algebraic_closure (k : Type u) [field k] :

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

Equations
Instances for algebraic_closure
@[protected, instance]
noncomputable def algebraic_closure.field (k : Type u) [field k] :
Equations
@[protected, instance]
noncomputable def algebraic_closure.inhabited (k : Type u) [field k] :
Equations

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

Equations
@[protected, instance]
@[protected, instance]
noncomputable def algebraic_closure.algebra (k : Type u) [field k] {R : Type u_1} [comm_semiring R] [alg : algebra R k] :
Equations
@[protected, instance]

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

Equations
@[protected, instance]