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 kis the typeclass sayingkis an algebraically closed field, i.e. every polynomial inksplits.is_alg_closure k Kis the typeclass sayingKis an algebraic closure ofk.algebraic_closure kis an algebraic closure ofk(in the same universe). It is constructed by taking the polynomial ring generated by indeterminatesx_fcorresponding to monic irreducible polynomialsfwith coefficients ink, and quotienting out by a maximal ideal containing everyf(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
- splits : ∀ (p : polynomial k), polynomial.splits (ring_hom.id k) p
Typeclass for algebraically closed fields.
Typeclass for an extension being an algebraic closure.
Equations
- is_alg_closure k K = (is_alg_closed K ∧ algebra.is_algebraic k K)
Instances
The subtype of monic irreducible polynomials
Equations
- algebraic_closure.monic_irreducible k = {f // f.monic ∧ irreducible f}
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
- 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 (s.prod (λ (x : algebraic_closure.monic_irreducible k), ↑x)).splitting_field) _ _) (λ (hf : f ∉ s), 37))
A random maximal ideal that contains span_eval k
Equations
The first step of constructing algebraic_closure: adjoin a root of all monic polynomials
Equations
The canonical ring homomorphism to adjoin_monic k.
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⟩)
The nth step of constructing algebraic_closure.
Equations
- algebraic_closure.step k n = (algebraic_closure.step_aux k n).fst
Equations
Equations
- algebraic_closure.step.inhabited k n = {default := 37}
The canonical inclusion to the 0th step.
Equations
The canonical ring homomorphism to the next step.
Equations
Equations
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' := _}
Equations
Equations
- _ = _
Equations
- _ = _
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))
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))
Equations
- algebraic_closure.inhabited k = {default := 37}
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)
Equations
Equations
- _ = _
Equations
Canonical algebra embedding from the nth step to the algebraic closure.