[Merged by Bors] - feat(field_theory/algebraic_closure): algebraic closure

src/algebra/direct_limit.lean

@@ -324,6 +324,23 @@ quotient.induction_on' z $ λ x, free_abelian_group.induction_on x
   (λ p q ⟨i, x, ihx⟩ ⟨j, y, ihy⟩, let ⟨k, hik, hjk⟩ := directed_order.directed i j in
     ⟨k, f i k hik x + f j k hjk y, by rw [of_add, of_f, of_f, ihx, ihy]; refl⟩)
 
+section
+open_locale classical
+open polynomial
+
+theorem polynomial.exists_of (q : polynomial (direct_limit G f)) :
+  ∃ i p, polynomial.map (ring_hom.of $ of G f i) p = q :=
+polynomial.induction_on q
+  (λ z, let ⟨i, x, h⟩ := exists_of z in ⟨i, C x, by rw [map_C, ring_hom.coe_of, h]⟩)
+  (λ q₁ q₂ ⟨i₁, p₁, ih₁⟩ ⟨i₂, p₂, ih₂⟩, let ⟨i, h1, h2⟩ := directed_order.directed i₁ i₂ in
+    ⟨i, p₁.map (ring_hom.of $ f i₁ i h1) + p₂.map (ring_hom.of $ f i₂ i h2),
+     by { rw [polynomial.map_add, map_map, map_map, ← ih₁, ← ih₂],
+      congr' 2; ext x; simp_rw [ring_hom.comp_apply, ring_hom.coe_of, of_f] }⟩)
+  (λ n z ih, let ⟨i, x, h⟩ := exists_of z in ⟨i, C x * X ^ (n + 1),
+    by rw [polynomial.map_mul, map_C, ring_hom.coe_of, h, polynomial.map_pow, map_X]⟩)
+
+end
+
 @[elab_as_eliminator] theorem induction_on {C : direct_limit G f → Prop} (z : direct_limit G f)
   (ih : ∀ i x, C (of G f i x)) : C z :=
 let ⟨i, x, hx⟩ := exists_of z in hx ▸ ih i x

src/data/mv_polynomial.lean

@@ -136,6 +136,10 @@ def C : α →+* mv_polynomial σ α :=
   map_add' := λ a a', single_add,
   map_mul' := λ a a', by simp [monomial, single_mul_single] }
 
+variables (α σ)
+theorem algebra_map_eq : algebra_map α (mv_polynomial σ α) = C := rfl
+variables {α σ}
+
 /-- `X n` is the degree `1` monomial `1*n` -/
 def X (n : σ) : mv_polynomial σ α := monomial (single n 1) 1
 

src/data/polynomial/field_division.lean

@@ -173,6 +173,10 @@ nat_degree_eq_of_degree_eq (degree_map _ f)
   leading_coeff (p.map f) = f (leading_coeff p) :=
 by simp [leading_coeff, coeff_map f]
 
+theorem monic_map_iff [field k] {f : R →+* k} {p : polynomial R} :
+  (p.map f).monic ↔ p.monic :=
+by rw [monic, leading_coeff_map, ← f.map_one, function.injective.eq_iff f.injective, monic]
+
 theorem is_unit_map [field k] (f : R →+* k) :
   is_unit (p.map f) ↔ is_unit p :=
 by simp_rw [is_unit_iff_degree_eq_zero, degree_map]
@@ -284,6 +288,14 @@ prime_of_associated normalize_associated this
 lemma irreducible_of_degree_eq_one (hp1 : degree p = 1) : irreducible p :=
 irreducible_of_prime (prime_of_degree_eq_one hp1)
 
+theorem not_irreducible_C (x : R) : ¬irreducible (C x) :=
+if H : x = 0 then by { rw [H, C_0], exact not_irreducible_zero }
+else λ hx, irreducible.not_unit hx $ is_unit_C.2 $ is_unit_iff_ne_zero.2 H
+
+theorem degree_pos_of_irreducible (hp : irreducible p) : 0 < p.degree :=
+lt_of_not_ge $ λ hp0, have _ := eq_C_of_degree_le_zero hp0,
+  not_irreducible_C (p.coeff 0) $ this ▸ hp
+
 theorem pairwise_coprime_X_sub {α : Type u} [field α] {I : Type v}
   {s : I → α} (H : function.injective s) :
   pairwise (is_coprime on (λ i : I, polynomial.X - polynomial.C (s i))) :=

src/data/real/ennreal.lean

@@ -461,7 +461,7 @@ le_antisymm (Inf_le $ le_add_left h) (zero_le _)
 @[simp] lemma sub_self : a - a = 0 := sub_eq_zero_of_le $ le_refl _
 
 @[simp] lemma zero_sub : 0 - a = 0 :=
-le_antisymm (Inf_le $ zero_le _) (zero_le _)
+le_antisymm (Inf_le $ zero_le $ 0 + a) (zero_le _)
 
 @[simp] lemma sub_infty : a - ∞ = 0 :=
 le_antisymm (Inf_le $ by simp) (zero_le _)

src/field_theory/algebraic_closure.lean

@@ -0,0 +1,292 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+
+import algebra.direct_limit
+import field_theory.splitting_field
+import analysis.complex.polynomial
+
+/-!
+# 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
+
+-/
+
+universes u v w
+noncomputable theory
+open_locale classical big_operators
+open polynomial
+
+variables (k : Type u) [field k]
+
+/-- Typeclass for algebraically closed fields. -/
+class is_alg_closed : Prop :=
+(splits : ∀ p : polynomial k, p.splits $ ring_hom.id k)
+
+theorem polynomial.splits' {k K : Type*} [field k] [is_alg_closed k] [field K] {f : k →+* K}
+  (p : polynomial k) : p.splits f :=
+polynomial.splits_of_splits_id _ $ is_alg_closed.splits _
+
+namespace is_alg_closed
+
+theorem of_exists_root (H : ∀ p : polynomial k, p.monic → irreducible p → ∃ x, p.eval x = 0) :
+  is_alg_closed k :=
+⟨λ p, or.inr $ λ q hq hqp,
+ have irreducible (q * C (leading_coeff q)⁻¹),
+   by { rw ← coe_norm_unit hq.ne_zero, exact irreducible_of_associated associated_normalize hq },
+ let ⟨x, hx⟩ := H (q * C (leading_coeff q)⁻¹) (monic_mul_leading_coeff_inv hq.ne_zero) this in
+ degree_mul_leading_coeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx⟩
+
+end is_alg_closed
+
+instance complex.is_alg_closed : is_alg_closed ℂ :=
+is_alg_closed.of_exists_root _ $ λ p _ hp, complex.exists_root $ degree_pos_of_irreducible hp
+
+/-- Typeclass for an extension being an algebraic closure. -/
+@[class] def is_alg_closure (K : Type v) [field K] [algebra k K] : Prop :=
+is_alg_closed K ∧ algebra.is_algebraic k K
+
+namespace algebraic_closure
+
+open mv_polynomial
+
+/-- The subtype of monic irreducible polynomials -/
+@[reducible] def monic_irreducible : Type u :=
+{ f : polynomial k // monic f ∧ irreducible f }
+
+/-- Sends a monic irreducible polynomial `f` to `f(x_f)` where `x_f` is a formal indeterminate. -/
+def eval_X_self (f : monic_irreducible k) : mv_polynomial (monic_irreducible k) k :=
+polynomial.eval₂ mv_polynomial.C (X f) f
+
+/-- The span of `f(x_f)` across monic irreducible polynomials `f` where `x_f` is an indeterminate. -/
+def span_eval : ideal (mv_polynomial (monic_irreducible k) k) :=
+ideal.span $ set.range $ eval_X_self k
+
+/-- 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`. -/
+def to_splitting_field (s : finset (monic_irreducible k)) :
+  mv_polynomial (monic_irreducible k) k →ₐ[k] splitting_field (∏ x in s, x : polynomial k) :=
+mv_polynomial.aeval $ λ f,
+  if hf : f ∈ s
+  then root_of_splits _
+    ((splits_prod_iff _ $ λ (j : monic_irreducible k) _, j.2.2.ne_zero).1
+      (splitting_field.splits _) f hf)
+    (mt is_unit_iff_degree_eq_zero.2 f.2.2.not_unit)
+  else 37
+
+theorem to_splitting_field_eval_X_self {s : finset (monic_irreducible k)} {f} (hf : f ∈ s) :
+  to_splitting_field k s (eval_X_self k f) = 0 :=
+by { rw [to_splitting_field, eval_X_self, ← alg_hom.coe_to_ring_hom, hom_eval₂,
+         alg_hom.coe_to_ring_hom, mv_polynomial.aeval_X, dif_pos hf,
+         ← algebra_map_eq, alg_hom.comp_algebra_map],
+  exact map_root_of_splits _ _ _ }
+
+theorem span_eval_ne_top : span_eval k ≠ ⊤ :=
+begin
+  rw [ideal.ne_top_iff_one, span_eval, ideal.span, ← set.image_univ, finsupp.mem_span_iff_total],
+  rintros ⟨v, _, hv⟩,
+  replace hv := congr_arg (to_splitting_field k v.support) hv,
+  rw [alg_hom.map_one, finsupp.total_apply, finsupp.sum, alg_hom.map_sum, finset.sum_eq_zero] at hv,
+  { exact zero_ne_one hv },
+  intros j hj,
+  rw [smul_eq_mul, alg_hom.map_mul, to_splitting_field_eval_X_self k hj, mul_zero]
+end
+
+/-- A random maximal ideal that contains `span_eval k` -/
+def max_ideal : ideal (mv_polynomial (monic_irreducible k) k) :=
+classical.some $ ideal.exists_le_maximal _ $ span_eval_ne_top k
+
+instance max_ideal.is_maximal : (max_ideal k).is_maximal :=
+(classical.some_spec $ ideal.exists_le_maximal _ $ span_eval_ne_top k).1
+
+theorem le_max_ideal : span_eval k ≤ max_ideal k :=
+(classical.some_spec $ ideal.exists_le_maximal _ $ span_eval_ne_top k).2
+
+/-- The first step of constructing `algebraic_closure`: adjoin a root of all monic polynomials -/
+def adjoin_monic : Type u :=
+(max_ideal k).quotient
+
+instance adjoin_monic.field : field (adjoin_monic k) :=
+ideal.quotient.field _
+
+instance adjoin_monic.inhabited : inhabited (adjoin_monic k) := ⟨37⟩
+
+/-- The canonical ring homomorphism to `adjoin_monic k`. -/
+def to_adjoin_monic : k →+* adjoin_monic k :=
+(ideal.quotient.mk _).comp C
+
+instance adjoin_monic.algebra : algebra k (adjoin_monic k) :=
+(to_adjoin_monic k).to_algebra
+
+theorem adjoin_monic.algebra_map : algebra_map k (adjoin_monic k) = (ideal.quotient.mk _).comp C :=
+rfl
+
+theorem adjoin_monic.is_integral (z : adjoin_monic k) : is_integral k z :=
+let ⟨p, hp⟩ := ideal.quotient.mk_surjective z in hp ▸
+mv_polynomial.induction_on p (λ x, is_integral_algebra_map) (λ p q, is_integral_add)
+  (λ p f ih, @is_integral_mul _ _ _ _ _ _ (ideal.quotient.mk _ _) ih ⟨f, f.2.1,
+    by { erw [polynomial.aeval_def, adjoin_monic.algebra_map, ← hom_eval₂,
+              ideal.quotient.eq_zero_iff_mem],
+      exact le_max_ideal k (ideal.subset_span ⟨f, rfl⟩) }⟩)
+
+theorem adjoin_monic.exists_root {f : polynomial k} (hfm : f.monic) (hfi : irreducible f) :
+  ∃ x : adjoin_monic k, f.eval₂ (to_adjoin_monic k) x = 0 :=
+⟨ideal.quotient.mk _ $ X (⟨f, hfm, hfi⟩ : monic_irreducible k),
+ by { rw [to_adjoin_monic, ← hom_eval₂, ideal.quotient.eq_zero_iff_mem],
+      exact le_max_ideal k (ideal.subset_span $ ⟨_, rfl⟩) }⟩
+
+/-- The `n`th step of constructing `algebraic_closure`, together with its `field` instance. -/
+def step_aux (n : ℕ) : Σ α : Type u, field α :=
+nat.rec_on n ⟨k, infer_instance⟩ $ λ n ih, ⟨@adjoin_monic ih.1 ih.2, @adjoin_monic.field ih.1 ih.2⟩
+
+/-- The `n`th step of constructing `algebraic_closure`. -/
+def step (n : ℕ) : Type u :=
+(step_aux k n).1
+
+instance step.field (n : ℕ) : field (step k n) :=
+(step_aux k n).2
+
+instance step.inhabited (n) : inhabited (step k n) := ⟨37⟩
+
+/-- The canonical inclusion to the `0`th step. -/
+def to_step_zero : k →+* step k 0 :=
+ring_hom.id k
+
+/-- The canonical ring homomorphism to the next step. -/
+def to_step_succ (n : ℕ) : step k n →+* step k (n + 1) :=
+@to_adjoin_monic (step k n) (step.field k n)
+
+instance step.algebra_succ (n) : algebra (step k n) (step k (n + 1)) :=
+(to_step_succ k n).to_algebra
+
+theorem to_step_succ.exists_root {n} {f : polynomial (step k n)}
+  (hfm : f.monic) (hfi : irreducible f) :
+  ∃ x : step k (n + 1), f.eval₂ (to_step_succ k n) x = 0 :=
+@adjoin_monic.exists_root _ (step.field k n) _ hfm hfi
+
+/-- The canonical ring homomorphism to a step with a greater index. -/
+def to_step_of_le (m n : ℕ) (h : m ≤ n) : step k m →+* step k n :=
+{ to_fun := nat.le_rec_on h (λ n, to_step_succ k n),
+  map_one' := begin
+    induction h with n h ih, { exact nat.le_rec_on_self 1 },
+    rw [nat.le_rec_on_succ h, ih, ring_hom.map_one]
+  end,
+  map_mul' := λ x y, begin
+    induction h with n h ih, { simp_rw nat.le_rec_on_self },
+    simp_rw [nat.le_rec_on_succ h, ih, ring_hom.map_mul]
+  end,
+  map_zero' := begin
+    induction h with n h ih, { exact nat.le_rec_on_self 0 },
+    rw [nat.le_rec_on_succ h, ih, ring_hom.map_zero]
+  end,
+  map_add' := λ x y, begin
+    induction h with n h ih, { simp_rw nat.le_rec_on_self },
+    simp_rw [nat.le_rec_on_succ h, ih, ring_hom.map_add]
+  end }
+
+@[simp] lemma coe_to_step_of_le (m n : ℕ) (h : m ≤ n) :
+  (to_step_of_le k m n h : step k m → step k n) = nat.le_rec_on h (λ n, to_step_succ k n) :=
+rfl
+
+instance step.algebra (n) : algebra k (step k n) :=
+(to_step_of_le k 0 n n.zero_le).to_algebra
+
+instance step.algebra_tower (n) : is_algebra_tower k (step k n) (step k (n + 1)) :=
+is_algebra_tower.of_algebra_map_eq $ λ z,
+  @nat.le_rec_on_succ (step k) 0 n n.zero_le (n + 1).zero_le (λ n, to_step_succ k n) z
+
+theorem step.is_integral (n) : ∀ z : step k n, is_integral k z :=
+nat.rec_on n (λ z, is_integral_algebra_map) $ λ n ih z,
+  is_integral_trans ih _ (adjoin_monic.is_integral (step k n) z : _)
+
+instance to_step_of_le.directed_system :
+  directed_system (step k) (λ i j h, to_step_of_le k i j h) :=
+⟨λ i x h, nat.le_rec_on_self x, λ i₁ i₂ i₃ h₁₂ h₂₃ x, (nat.le_rec_on_trans h₁₂ h₂₃ x).symm⟩
+
+end algebraic_closure
+
+/-- The canonical algebraic closure of a field, the direct limit of adding roots to the field for each polynomial over the field. -/
+def algebraic_closure : Type u :=
+ring.direct_limit (algebraic_closure.step k) (λ i j h, algebraic_closure.to_step_of_le k i j h)
+
+namespace algebraic_closure
+
+instance : field (algebraic_closure k) :=
+field.direct_limit.field _ _
+
+instance : inhabited (algebraic_closure k) := ⟨37⟩
+
+/-- The canonical ring embedding from the `n`th step to the algebraic closure. -/
+def of_step (n : ℕ) : step k n →+* algebraic_closure k :=
+ring_hom.of $ ring.direct_limit.of _ _ _
+
+instance algebra_of_step (n) : algebra (step k n) (algebraic_closure k) :=
+(of_step k n).to_algebra
+
+theorem of_step_succ (n : ℕ) : (of_step k (n + 1)).comp (to_step_succ k n) = of_step k n :=
+ring_hom.ext $ λ x, show ring.direct_limit.of (step k) (λ i j h, to_step_of_le k i j h) _ _ = _,
+  by { convert ring.direct_limit.of_f n.le_succ x, ext x, exact (nat.le_rec_on_succ' x).symm }
+
+theorem exists_of_step (z : algebraic_closure k) : ∃ n x, of_step k n x = z :=
+ring.direct_limit.exists_of z
+
+-- slow
+theorem exists_root {f : polynomial (algebraic_closure k)}
+  (hfm : f.monic) (hfi : irreducible f) :
+  ∃ x : algebraic_closure k, f.eval x = 0 :=
+begin
+  have : ∃ n p, polynomial.map (of_step k n) p = f,
+  { convert ring.direct_limit.polynomial.exists_of f },
+  unfreezingI { obtain ⟨n, p, rfl⟩ := this },
+  rw monic_map_iff at hfm,
+  have := irreducible_of_irreducible_map (of_step k n) p hfm hfi,
+  obtain ⟨x, hx⟩ := to_step_succ.exists_root k hfm this,
+  refine ⟨of_step k (n + 1) x, _⟩,
+  rw [← of_step_succ k n, eval_map, ← hom_eval₂, hx, ring_hom.map_zero]
+end
+
+instance : is_alg_closed (algebraic_closure k) :=
+is_alg_closed.of_exists_root _ $ λ f, exists_root k
+
+instance : algebra k (algebraic_closure k) :=
+(of_step k 0).to_algebra
+
+/-- Canonical algebra embedding from the `n`th step to the algebraic closure. -/
+def of_step_hom (n) : step k n →ₐ[k] algebraic_closure k :=
+{ commutes' := λ x, ring.direct_limit.of_f n.zero_le x,
+  .. of_step k n }
+
+theorem is_algebraic : algebra.is_algebraic k (algebraic_closure k) :=
+λ z, (is_algebraic_iff_is_integral _).2 $ let ⟨n, x, hx⟩ := exists_of_step k z in
+hx ▸ is_integral_alg_hom (of_step_hom k n) (step.is_integral k n x)
+
+instance : is_alg_closure k (algebraic_closure k) :=
+⟨algebraic_closure.is_alg_closed k, is_algebraic k⟩
+
+end algebraic_closure

src/field_theory/splitting_field.lean

@@ -87,6 +87,9 @@ by simp [splits, polynomial.map_map]
 theorem splits_one : splits i 1 :=
 splits_C i 1
 
+theorem splits_of_is_unit {u : polynomial α} (hu : is_unit u) : u.splits i :=
+splits_of_splits_of_dvd i one_ne_zero (splits_one _) $ is_unit_iff_dvd_one.1 hu
+
 theorem splits_X_sub_C {x : α} : (X - C x).splits i :=
 splits_of_degree_eq_one _ $ degree_X_sub_C x
 
@@ -151,6 +154,14 @@ is_noetherian_ring.irreducible_induction_on (f.map i)
             hp.ne_zero), one_mul],
       end⟩)
 
+/-- Pick a root of a polynomial that splits. -/
+def root_of_splits {f : polynomial α} (hf : f.splits i) (hfd : f.degree ≠ 0) : β :=
+classical.some $ exists_root_of_splits i hf hfd
+
+theorem map_root_of_splits {f : polynomial α} (hf : f.splits i) (hfd) :
+  f.eval₂ i (root_of_splits i hf hfd) = 0 :=
+classical.some_spec $ exists_root_of_splits i hf hfd
+
 theorem roots_map {f : polynomial α} (hf : f.splits $ ring_hom.id α) :
   (f.map i).roots = (f.roots).image i :=
 if hf0 : f = 0 then by rw [hf0, map_zero, roots_zero, roots_zero, finset.image_empty] else

src/order/directed.lean

@@ -63,4 +63,7 @@ set_option default_priority 100 -- see Note [default priority]
 there is an element `k` such that `i ≤ k` and `j ≤ k`. -/
 class directed_order (α : Type u) extends preorder α :=
 (directed : ∀ i j : α, ∃ k, i ≤ k ∧ j ≤ k)
+
+instance linear_order.to_directed_order (α) [linear_order α] : directed_order α :=
+⟨λ i j, or.cases_on (le_total i j) (λ hij, ⟨j, hij, le_refl j⟩) (λ hji, ⟨i, le_refl i, hji⟩)⟩
 end prio