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 #
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.
Tags #
algebraic closure, algebraically closed
@[reducible]
The subtype of monic irreducible polynomials
Equations
- algebraic_closure.monic_irreducible k = {f // f.monic ∧ irreducible f}
noncomputable
def
algebraic_closure.eval_X_self
(k : Type u)
[field k]
(f : algebraic_closure.monic_irreducible k) :
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
noncomputable
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] (s.prod (λ (x : algebraic_closure.monic_irreducible k), ↑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 (s.prod (λ (x : algebraic_closure.monic_irreducible k), ↑x)).splitting_field) _ _) (λ (hf : f ∉ s), 37))
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) :
A random maximal ideal that contains span_eval k
Equations
Instances for algebraic_closure.max_ideal
@[protected, instance]
The first step of constructing algebraic_closure: adjoin a root of all monic polynomials
Equations
Instances for algebraic_closure.adjoin_monic
@[protected, instance]
@[protected, instance]
Equations
The canonical ring homomorphism to adjoin_monic k.
@[protected, instance]
theorem
algebraic_closure.adjoin_monic.is_integral
(k : Type u)
[field k]
(z : algebraic_closure.adjoin_monic k) :
is_integral k z
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
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
@[protected, instance]
noncomputable
def
algebraic_closure.step.field
(k : Type u)
[field k]
(n : ℕ) :
field (algebraic_closure.step k n)
Equations
@[protected, instance]
Equations
- algebraic_closure.step.inhabited k n = {default := 37}
The canonical inclusion to the 0th step.
Equations
noncomputable
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
@[protected, instance]
noncomputable
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
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
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' := _}
@[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))
@[protected, instance]
noncomputable
def
algebraic_closure.step.algebra
(k : Type u)
[field k]
(n : ℕ) :
algebra k (algebraic_closure.step k n)
Equations
@[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))
theorem
algebraic_closure.step.is_integral
(k : Type u)
[field k]
(n : ℕ)
(z : algebraic_closure.step k n) :
is_integral k z
@[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))
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))
@[protected, instance]
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)
@[protected, instance]
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.direct_limit.of (algebraic_closure.step k) (λ (i j : ℕ) (h : i ≤ j), ⇑(algebraic_closure.to_step_of_le k i j h)) n
@[protected, instance]
noncomputable
def
algebraic_closure.algebra_of_step
(k : Type u)
[field k]
(n : ℕ) :
algebra (algebraic_closure.step k n) (algebraic_closure k)
Equations
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
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
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
@[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] :
algebra R (algebraic_closure k)
Equations
- algebraic_closure.algebra k = ((algebraic_closure.of_step k 0).comp (algebra_map R k)).to_algebra
theorem
algebraic_closure.algebra_map_def
(k : Type u)
[field k]
{R : Type u_1}
[comm_semiring R]
[alg : algebra R k] :
algebra_map R (algebraic_closure k) = (algebraic_closure.of_step k 0).comp (algebra_map R k)
@[protected, 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] :
is_scalar_tower R S (algebraic_closure k)
Canonical algebra embedding from the nth step to the algebraic closure.
@[protected, instance]