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 #

is_alg_closed k is the typeclass saying k is an algebraically closed field, i.e. every polynomial in k splits.
is_alg_closure k K is the typeclass saying K is an algebraic closure of k.
algebraic_closure k is an algebraic closure of k (in the same universe). It is constructed by taking the polynomial ring generated by indeterminates x_f corresponding to monic irreducible polynomials f with coefficients in k, and quotienting out by a maximal ideal containing every f(x_f), and then repeating this step countably many times. See Exercise 1.13 in Atiyah--Macdonald.

TODO #

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

Tags #

algebraic closure, algebraically closed

source

@[class]

structure is_alg_closed (k : Type u) [field k] :

Prop

splits : ∀ (p : polynomial k), polynomial.splits (ring_hom.id k) p

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

source

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) :

polynomial.splits f p

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.

source

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) :

polynomial.splits f p

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.

source

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

is_alg_closed k

source

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

source

theorem is_alg_closed.algebra_map_surjective_of_is_integral {k : Type u_1} {K : Type u_2} [field k] [domain K] [hk : is_alg_closed k] [algebra k K] (hf : algebra.is_integral k K) :

function.surjective ⇑(algebra_map k K)

source

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) :

function.surjective ⇑f

source

theorem is_alg_closed.algebra_map_surjective_of_is_algebraic {k : Type u_1} {K : Type u_2} [field k] [domain K] [hk : is_alg_closed k] [algebra k K] (hf : algebra.is_algebraic k K) :

function.surjective ⇑(algebra_map k K)

source

@[class]

structure is_alg_closure (k : Type u) [field k] (K : Type v) [field K] [algebra k K] :

Prop

alg_closed : is_alg_closed K
algebraic : algebra.is_algebraic k K

Typeclass for an extension being an algebraic closure.

Instances

algebraic_closure.is_alg_closure

source

theorem is_alg_closure_iff (k : Type u) [field k] (K : Type v) [field K] [algebra k K] :

is_alg_closure k K ↔ is_alg_closed K ∧ algebra.is_algebraic k K

source

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

Type u

The subtype of monic irreducible polynomials

Equations

algebraic_closure.monic_irreducible k = {f // f.monic ∧ irreducible f}

source

def algebraic_closure.eval_X_self (k : Type u) [field k] (f : algebraic_closure.monic_irreducible k) :

mv_polynomial (algebraic_closure.monic_irreducible k) k

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

Equations

algebraic_closure.eval_X_self k f = polynomial.eval₂ mv_polynomial.C (mv_polynomial.X f) ↑f

source

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

ideal (mv_polynomial (algebraic_closure.monic_irreducible k) k)

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

Equations

algebraic_closure.span_eval k = ideal.span (set.range (algebraic_closure.eval_X_self k))

source

def algebraic_closure.to_splitting_field (k : Type u) [field k] (s : finset (algebraic_closure.monic_irreducible k)) :

mv_polynomial (algebraic_closure.monic_irreducible k) k →ₐ[k] (∏ (x : algebraic_closure.monic_irreducible k) in s, ↑x).splitting_field

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

algebraic_closure.to_splitting_field k s = mv_polynomial.aeval (λ (f : algebraic_closure.monic_irreducible k), dite (f ∈ s) (λ (hf : f ∈ s), polynomial.root_of_splits (algebra_map k (∏ (x : algebraic_closure.monic_irreducible k) in s, ↑x).splitting_field) _ _) (λ (hf : f ∉ s), 37))

source

theorem algebraic_closure.to_splitting_field_eval_X_self (k : Type u) [field k] {s : finset (algebraic_closure.monic_irreducible k)} {f : algebraic_closure.monic_irreducible k} (hf : f ∈ s) :

⇑(algebraic_closure.to_splitting_field k s) (algebraic_closure.eval_X_self k f) = 0

source

theorem algebraic_closure.span_eval_ne_top (k : Type u) [field k] :

algebraic_closure.span_eval k ≠ ⊤

source

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

ideal (mv_polynomial (algebraic_closure.monic_irreducible k) k)

A random maximal ideal that contains span_eval k

Equations

algebraic_closure.max_ideal k = classical.some _

source

@[protected, instance]

def algebraic_closure.max_ideal.is_maximal (k : Type u) [field k] :

(algebraic_closure.max_ideal k).is_maximal

source

theorem algebraic_closure.le_max_ideal (k : Type u) [field k] :

algebraic_closure.span_eval k ≤ algebraic_closure.max_ideal k

source

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

algebraic_closure.adjoin_monic k = (algebraic_closure.max_ideal k).quotient

source

@[protected, instance]

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

field (algebraic_closure.adjoin_monic k)

Equations

algebraic_closure.adjoin_monic.field k = ideal.quotient.field (algebraic_closure.max_ideal k)

source

@[protected, instance]

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

inhabited (algebraic_closure.adjoin_monic k)

Equations

algebraic_closure.adjoin_monic.inhabited k = {default := 37}

source

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

k →+* algebraic_closure.adjoin_monic k

The canonical ring homomorphism to adjoin_monic k.

Equations

algebraic_closure.to_adjoin_monic k = (ideal.quotient.mk (algebraic_closure.max_ideal k)).comp mv_polynomial.C

source

@[protected, instance]

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

algebra k (algebraic_closure.adjoin_monic k)

Equations

algebraic_closure.adjoin_monic.algebra k = (algebraic_closure.to_adjoin_monic k).to_algebra

source

theorem algebraic_closure.adjoin_monic.algebra_map (k : Type u) [field k] :

algebra_map k (algebraic_closure.adjoin_monic k) = (ideal.quotient.mk (algebraic_closure.max_ideal k)).comp mv_polynomial.C

source

theorem algebraic_closure.adjoin_monic.is_integral (k : Type u) [field k] (z : algebraic_closure.adjoin_monic k) :

is_integral k z

source

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

∃ (x : algebraic_closure.adjoin_monic k), polynomial.eval₂ (algebraic_closure.to_adjoin_monic k) x f = 0

source

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

algebraic_closure.step_aux k n = n.rec_on ⟨k, infer_instance _inst_1⟩ (λ (n : ℕ) (ih : Σ (α : Type u), field α), ⟨algebraic_closure.adjoin_monic ih.fst ih.snd, algebraic_closure.adjoin_monic.field ih.fst ih.snd⟩)

source

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

Type u

The nth step of constructing algebraic_closure.

Equations

algebraic_closure.step k n = (algebraic_closure.step_aux k n).fst

source

@[protected, instance]

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

field (algebraic_closure.step k n)

Equations

algebraic_closure.step.field k n = (algebraic_closure.step_aux k n).snd

source

@[protected, instance]

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

inhabited (algebraic_closure.step k n)

Equations

algebraic_closure.step.inhabited k n = {default := 37}

source

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

k →+* algebraic_closure.step k 0

The canonical inclusion to the 0th step.

Equations

algebraic_closure.to_step_zero k = ring_hom.id k

source

def algebraic_closure.to_step_succ (k : Type u) [field k] (n : ℕ) :

algebraic_closure.step k n →+* algebraic_closure.step k (n + 1)

The canonical ring homomorphism to the next step.

Equations

algebraic_closure.to_step_succ k n = algebraic_closure.to_adjoin_monic (algebraic_closure.step k n)

source

@[protected, instance]

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

algebra (algebraic_closure.step k n) (algebraic_closure.step k (n + 1))

Equations

algebraic_closure.step.algebra_succ k n = (algebraic_closure.to_step_succ k n).to_algebra

source

theorem algebraic_closure.to_step_succ.exists_root (k : Type u) [field k] {n : ℕ} {f : polynomial (algebraic_closure.step k n)} (hfm : f.monic) (hfi : irreducible f) :

∃ (x : algebraic_closure.step k (n + 1)), polynomial.eval₂ (algebraic_closure.to_step_succ k n) x f = 0

source

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

algebraic_closure.step k m →+* algebraic_closure.step k n

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

Equations

algebraic_closure.to_step_of_le k m n h = {to_fun := nat.le_rec_on h (λ (n : ℕ), ⇑(algebraic_closure.to_step_succ k n)), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem algebraic_closure.coe_to_step_of_le (k : Type u) [field k] (m n : ℕ) (h : m ≤ n) :

⇑(algebraic_closure.to_step_of_le k m n h) = nat.le_rec_on h (λ (n : ℕ), ⇑(algebraic_closure.to_step_succ k n))

source

@[protected, instance]

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

algebra k (algebraic_closure.step k n)

Equations

algebraic_closure.step.algebra k n = (algebraic_closure.to_step_of_le k 0 n _).to_algebra

source

@[protected, instance]

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

is_scalar_tower k (algebraic_closure.step k n) (algebraic_closure.step k (n + 1))

source

theorem algebraic_closure.step.is_integral (k : Type u) [field k] (n : ℕ) (z : algebraic_closure.step k n) :

is_integral k z

source

@[protected, instance]

def algebraic_closure.to_step_of_le.directed_system (k : Type u) [field k] :

directed_system (algebraic_closure.step k) (λ (i j : ℕ) (h : i ≤ j), ⇑(algebraic_closure.to_step_of_le k i j h))

source

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

algebraic_closure k = ring.direct_limit (algebraic_closure.step k) (λ (i j : ℕ) (h : i ≤ j), ⇑(algebraic_closure.to_step_of_le k i j h))

source

@[protected, instance]

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

field (algebraic_closure k)

Equations

algebraic_closure.field k = field.direct_limit.field (algebraic_closure.step k) (λ (i j : ℕ) (h : i ≤ j), algebraic_closure.to_step_of_le k i j h)

source

@[protected, instance]

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

inhabited (algebraic_closure k)

Equations

algebraic_closure.inhabited k = {default := 37}

source

def algebraic_closure.of_step (k : Type u) [field k] (n : ℕ) :

algebraic_closure.step k n →+* algebraic_closure k

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

Equations

algebraic_closure.of_step k n = ring_hom.of ⇑(ring.direct_limit.of (algebraic_closure.step k) (λ (i j : ℕ) (h : i ≤ j), ⇑(algebraic_closure.to_step_of_le k i j h)) n)

source

@[protected, instance]

def algebraic_closure.algebra_of_step (k : Type u) [field k] (n : ℕ) :

algebra (algebraic_closure.step k n) (algebraic_closure k)

Equations

algebraic_closure.algebra_of_step k n = (algebraic_closure.of_step k n).to_algebra

source

theorem algebraic_closure.of_step_succ (k : Type u) [field k] (n : ℕ) :

(algebraic_closure.of_step k (n + 1)).comp (algebraic_closure.to_step_succ k n) = algebraic_closure.of_step k n

source

theorem algebraic_closure.exists_of_step (k : Type u) [field k] (z : algebraic_closure k) :

∃ (n : ℕ) (x : algebraic_closure.step k n), ⇑(algebraic_closure.of_step k n) x = z

source

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

∃ (x : algebraic_closure k), polynomial.eval x f = 0

source

@[protected, instance]

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

is_alg_closed (algebraic_closure k)

source

@[protected, instance]

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

algebra k (algebraic_closure k)

Equations

algebraic_closure.algebra k = (algebraic_closure.of_step k 0).to_algebra

source

def algebraic_closure.of_step_hom (k : Type u) [field k] (n : ℕ) :

algebraic_closure.step k n →ₐ[k] algebraic_closure k

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

Equations

algebraic_closure.of_step_hom k n = {to_fun := (algebraic_closure.of_step k n).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

theorem algebraic_closure.is_algebraic (k : Type u) [field k] :

algebra.is_algebraic k (algebraic_closure k)

source

@[protected, instance]

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

is_alg_closure k (algebraic_closure k)

source

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.