feat(ring_theory/algebraic): algebraic extensions, algebraic elements (…

…#1519)

* chore(ring_theory/algebra): make first type argument explicit in alg_hom

Now this works, and it didn't work previously even with `@`
```lean
structure alg_equiv (α β γ : Type*) [comm_ring α] [ring β] [ring γ]
  [algebra α β] [algebra α γ] extends alg_hom α β γ :=
```

* Update algebra.lean

* feat(field_theory/algebraic_closure)

* Remove sorries about minimal polynomials

* Define alg_equiv.symm

* typo

* Remove another sorry, in base_extension

* Work in progress

* Remove a sorry in maximal_extension_chain

* Merge two sorries

* More sorries removed

* More work on transitivity of algebraicity

* WIP

* Sorry-free definition of algebraic closure

* More or less sorries

* Removing some sorries

* WIP

* Fix algebraic.lean

* Fix build, mostly

* Remove stuff about UMP of alg clos

* Prove transitivity of algebraic extensions

* Add some docstrings

* Remove files with stuff for future PRs

* Add a bit to the module docstring

* Fix module docstring

* Include assumption in section injective

* Aesthetic changes to is_integral_of_mem_of_fg

* Little improvements of proofs in algebraic.lean

* Improve some proofs in integral_closure.lean

* Make variable name explicit

* Process comments

src/data/polynomial.lean

@@ -398,76 +398,6 @@ by unfold comp; apply_instance
 
 end comp
 
-section map
-variables [comm_semiring β]
-variables (f : α → β)
-
-/-- `map f p` maps a polynomial `p` across a ring hom `f` -/
-def map : polynomial α → polynomial β := eval₂ (C ∘ f) X
-
-variables [is_semiring_hom f]
-
-@[simp] lemma map_C : (C a).map f = C (f a) := eval₂_C _ _
-
-@[simp] lemma map_X : X.map f = X := eval₂_X _ _
-
-@[simp] lemma map_zero : (0 : polynomial α).map f = 0 :=  eval₂_zero _ _
-
-@[simp] lemma map_add : (p + q).map f = p.map f + q.map f := eval₂_add _ _
-
-@[simp] lemma map_one : (1 : polynomial α).map f = 1 := eval₂_one _ _
-
-@[simp] lemma map_mul : (p * q).map f = p.map f * q.map f := eval₂_mul _ _
-
-instance map.is_semiring_hom : is_semiring_hom (map f) := eval₂.is_semiring_hom _ _
-
-lemma map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n := eval₂_pow _ _ _
-
-lemma coeff_map (n : ℕ) : coeff (p.map f) n = f (coeff p n) :=
-begin
-  rw [map, eval₂, coeff_sum],
-  conv_rhs { rw [← sum_C_mul_X_eq p, coeff_sum, finsupp.sum,
-    ← finset.sum_hom f], },
-  refine finset.sum_congr rfl (λ x hx, _),
-  simp [function.comp, coeff_C_mul_X, is_semiring_hom.map_mul f],
-  split_ifs; simp [is_semiring_hom.map_zero f],
-end
-
-lemma map_map {γ : Type*} [comm_semiring γ] (g : β → γ) [is_semiring_hom g]
-  (p : polynomial α) : (p.map f).map g = p.map (λ x, g (f x)) :=
-ext (by simp [coeff_map])
-
-lemma eval₂_map {γ : Type*} [comm_semiring γ] (g : β → γ) [is_semiring_hom g] (x : γ) :
-  (p.map f).eval₂ g x = p.eval₂ (λ y, g (f y)) x :=
-polynomial.induction_on p
-  (by simp)
-  (by simp [is_semiring_hom.map_add f] {contextual := tt})
-  (by simp [is_semiring_hom.map_mul f,
-    is_semiring_hom.map_pow f, pow_succ', (mul_assoc _ _ _).symm] {contextual := tt})
-
-lemma eval_map (x : β) : (p.map f).eval x = p.eval₂ f x := eval₂_map _ _ _
-
-@[simp] lemma map_id : p.map id = p := by simp [id, polynomial.ext_iff, coeff_map]
-
-end map
-
-section
-variables {γ : Type*} [comm_semiring β] [comm_semiring γ]
-variables (f : α → β) (g : β → γ) [is_semiring_hom f] [is_semiring_hom g] (p)
-
-lemma hom_eval₂ (x : β) : g (p.eval₂ f x) = p.eval₂ (g ∘ f) (g x) :=
-begin
-  apply polynomial.induction_on p; clear p,
-  { intros a, rw [eval₂_C, eval₂_C] },
-  { intros p q hp hq, simp only [hp, hq, eval₂_add, is_semiring_hom.map_add g] },
-  { intros n a ih,
-    replace ih := congr_arg (λ y, y * g x) ih,
-    simpa [pow_succ', is_semiring_hom.map_mul g, (mul_assoc _ _ _).symm,
-      eval₂_C, eval₂_mul, eval₂_X] using ih }
-end
-
-end
-
 /-- `leading_coeff p` gives the coefficient of the highest power of `X` in `p`-/
 def leading_coeff (p : polynomial α) : α := coeff p (nat_degree p)
 
@@ -609,6 +539,89 @@ begin
     finset.sum_mul_boole, finset_sum_coeff, ite_le_nat_degree_coeff],
 end
 
+section map
+variables [comm_semiring β]
+variables (f : α → β)
+
+/-- `map f p` maps a polynomial `p` across a ring hom `f` -/
+def map : polynomial α → polynomial β := eval₂ (C ∘ f) X
+
+variables [is_semiring_hom f]
+
+@[simp] lemma map_C : (C a).map f = C (f a) := eval₂_C _ _
+
+@[simp] lemma map_X : X.map f = X := eval₂_X _ _
+
+@[simp] lemma map_zero : (0 : polynomial α).map f = 0 :=  eval₂_zero _ _
+
+@[simp] lemma map_add : (p + q).map f = p.map f + q.map f := eval₂_add _ _
+
+@[simp] lemma map_one : (1 : polynomial α).map f = 1 := eval₂_one _ _
+
+@[simp] lemma map_mul : (p * q).map f = p.map f * q.map f := eval₂_mul _ _
+
+instance map.is_semiring_hom : is_semiring_hom (map f) := eval₂.is_semiring_hom _ _
+
+@[simp] lemma map_pow (n : ℕ) : (p ^ n).map f = p.map f ^ n := eval₂_pow _ _ _
+
+lemma coeff_map (n : ℕ) : coeff (p.map f) n = f (coeff p n) :=
+begin
+  rw [map, eval₂, coeff_sum],
+  conv_rhs { rw [← sum_C_mul_X_eq p, coeff_sum, finsupp.sum,
+    ← finset.sum_hom f], },
+  refine finset.sum_congr rfl (λ x hx, _),
+  simp [function.comp, coeff_C_mul_X, is_semiring_hom.map_mul f],
+  split_ifs; simp [is_semiring_hom.map_zero f],
+end
+
+lemma map_map {γ : Type*} [comm_semiring γ] (g : β → γ) [is_semiring_hom g]
+  (p : polynomial α) : (p.map f).map g = p.map (λ x, g (f x)) :=
+ext (by simp [coeff_map])
+
+lemma eval₂_map {γ : Type*} [comm_semiring γ] (g : β → γ) [is_semiring_hom g] (x : γ) :
+  (p.map f).eval₂ g x = p.eval₂ (λ y, g (f y)) x :=
+polynomial.induction_on p
+  (by simp)
+  (by simp [is_semiring_hom.map_add f] {contextual := tt})
+  (by simp [is_semiring_hom.map_mul f,
+    is_semiring_hom.map_pow f, pow_succ', (mul_assoc _ _ _).symm] {contextual := tt})
+
+lemma eval_map (x : β) : (p.map f).eval x = p.eval₂ f x := eval₂_map _ _ _
+
+@[simp] lemma map_id : p.map id = p := by simp [id, polynomial.ext_iff, coeff_map]
+
+lemma mem_map_range {p : polynomial β} :
+  p ∈ set.range (map f) ↔ ∀ n, p.coeff n ∈ (set.range f) :=
+begin
+  split,
+  { rintro ⟨p, rfl⟩ n, rw coeff_map, exact set.mem_range_self _ },
+  { intro h, rw p.as_sum,
+    apply is_add_submonoid.finset_sum_mem,
+    intros i hi,
+    rcases h i with ⟨c, hc⟩,
+    use [C c * X^i],
+    rw [map_mul, map_C, hc, map_pow, map_X] }
+end
+
+end map
+
+section
+variables {γ : Type*} [comm_semiring β] [comm_semiring γ]
+variables (f : α → β) (g : β → γ) [is_semiring_hom f] [is_semiring_hom g] (p)
+
+lemma hom_eval₂ (x : β) : g (p.eval₂ f x) = p.eval₂ (g ∘ f) (g x) :=
+begin
+  apply polynomial.induction_on p; clear p,
+  { intros a, rw [eval₂_C, eval₂_C] },
+  { intros p q hp hq, simp only [hp, hq, eval₂_add, is_semiring_hom.map_add g] },
+  { intros n a ih,
+    replace ih := congr_arg (λ y, y * g x) ih,
+    simpa [pow_succ', is_semiring_hom.map_mul g, (mul_assoc _ _ _).symm,
+      eval₂_C, eval₂_mul, eval₂_X] using ih }
+end
+
+end
+
 lemma coeff_nat_degree_eq_zero_of_degree_lt (h : degree p < degree q) : coeff p (nat_degree q) = 0 :=
 coeff_eq_zero_of_degree_lt (lt_of_lt_of_le h degree_le_nat_degree)
 
@@ -733,6 +746,14 @@ leading_coeff_monomial 1 0
 
 @[simp] lemma monic_one : monic (1 : polynomial α) := leading_coeff_C _
 
+lemma monic.ne_zero_of_zero_ne_one (h : (0:α) ≠ 1) {p : polynomial α} (hp : p.monic) :
+  p ≠ 0 :=
+by { contrapose! h, rwa [h] at hp }
+
+lemma monic.ne_zero {α : Type*} [nonzero_comm_ring α] {p : polynomial α} (hp : p.monic) :
+  p ≠ 0 :=
+hp.ne_zero_of_zero_ne_one $ zero_ne_one
+
 lemma leading_coeff_add_of_degree_lt (h : degree p < degree q) :
   leading_coeff (p + q) = leading_coeff q :=
 have coeff p (nat_degree q) = 0, from coeff_nat_degree_eq_zero_of_degree_lt h,
@@ -889,13 +910,6 @@ le_antisymm (degree_map_le f) $
     rw [coeff_map], exact hf
   end
 
-lemma degree_map_eq_of_injective [comm_semiring β] (f : α → β) [is_semiring_hom f]
-  (hf : function.injective f) : degree (p.map f) = degree p :=
-if h : p = 0 then by simp [h]
-else degree_map_eq_of_leading_coeff_ne_zero _
-  (by rw [← is_semiring_hom.map_zero f]; exact mt hf.eq_iff.1
-    (mt leading_coeff_eq_zero.1 h))
-
 lemma monic_map [comm_semiring β] (f : α → β)
   [is_semiring_hom f] (hp : monic p) : monic (p.map f) :=
 if h : (0 : β) = 1 then
@@ -955,15 +969,49 @@ by simpa only [C_1, one_mul] using degree_C_mul_X_pow_le (1:α) n
 theorem degree_X_le : degree (X : polynomial α) ≤ 1 :=
 by simpa only [C_1, one_mul, pow_one] using degree_C_mul_X_pow_le (1:α) 1
 
-lemma degree_map' [comm_semiring β] (p : polynomial α)
-  {f : α → β} [is_semiring_hom f] (hf : function.injective f) :
+section injective
+open function
+variables [comm_semiring β] {f : α → β} [is_semiring_hom f] (hf : function.injective f)
+include hf
+
+lemma degree_map_eq_of_injective (p : polynomial α) : degree (p.map f) = degree p :=
+if h : p = 0 then by simp [h]
+else degree_map_eq_of_leading_coeff_ne_zero _
+  (by rw [← is_semiring_hom.map_zero f]; exact mt hf.eq_iff.1
+    (mt leading_coeff_eq_zero.1 h))
+
+lemma degree_map' (p : polynomial α) :
   degree (p.map f) = degree p :=
-degree_map_eq_of_injective _ hf
+p.degree_map_eq_of_injective hf
 
-lemma nat_degree_map' [comm_semiring β] (p : polynomial α)
-  {f : α → β} [is_semiring_hom f] (hf : function.injective f) :
+lemma nat_degree_map' (p : polynomial α) :
   nat_degree (p.map f) = nat_degree p :=
-nat_degree_eq_of_degree_eq (degree_map' _ hf)
+nat_degree_eq_of_degree_eq (degree_map' hf p)
+
+lemma map_injective (p : polynomial α) :
+  injective (map f : polynomial α → polynomial β) :=
+λ p q h, ext $ λ m, hf $
+begin
+  rw ext_iff at h,
+  specialize h m,
+  rw [coeff_map f, coeff_map f] at h,
+  exact h
+end
+
+lemma leading_coeff_of_injective (p : polynomial α) :
+  leading_coeff (p.map f) = f (leading_coeff p) :=
+begin
+  delta leading_coeff,
+  rw [coeff_map f, nat_degree_map' hf p]
+end
+
+lemma monic_of_injective {p : polynomial α} (hp : (p.map f).monic) : p.monic :=
+begin
+  apply hf,
+  rw [← leading_coeff_of_injective hf, hp.leading_coeff, is_semiring_hom.map_one f]
+end
+
+end injective
 
 theorem monic_of_degree_le (n : ℕ) (H1 : degree p ≤ n) (H2 : coeff p n = 1) : monic p :=
 decidable.by_cases
@@ -2119,7 +2167,7 @@ by rw [div_def, mul_comm, degree_mul_leading_coeff_inv _ hq0];
 
 @[simp] lemma degree_map [discrete_field β] (p : polynomial α) (f : α → β) [is_field_hom f] :
   degree (p.map f) = degree p :=
-degree_map_eq_of_injective _ (is_field_hom.injective f)
+p.degree_map_eq_of_injective (is_field_hom.injective f)
 
 @[simp] lemma nat_degree_map [discrete_field β] (f : α → β) [is_field_hom f] :
   nat_degree (p.map f) = nat_degree p :=

src/field_theory/minimal_polynomial.lean

@@ -166,7 +166,7 @@ variable (β)
 /--If L/K is a field extension, and x is an element of L in the image of K,
 then the minimal polynomial of x is X - C x.-/
 lemma algebra_map' (a : α) :
-  minimal_polynomial (@is_integral_algebra_map α β _ _ _ _ _ a) =
+  minimal_polynomial (@is_integral_algebra_map α β _ _ _ a) =
   X - C a :=
 minimal_polynomial.algebra_map _ _
 variable {β}

src/ring_theory/algebraic.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2019 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import ring_theory.integral_closure
+
+/-!
+# Algebraic elements and algebraic extensions
+
+An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial.
+An R-algebra is algebraic over R if and only if all its elements are algebraic over R.
+The main result in this file proves transitivity of algebraicity:
+a tower of algebraic field extensions is algebraic.
+-/
+
+universe variables u v
+
+open_locale classical
+open polynomial
+
+section
+variables (R : Type u) {A : Type v} [comm_ring R] [comm_ring A] [algebra R A]
+
+/-- An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial. -/
+def is_algebraic (x : A) : Prop :=
+∃ p : polynomial R, p ≠ 0 ∧ aeval R A x p = 0
+
+variables {R}
+
+/-- A subalgebra is algebraic if all its elements are algebraic. -/
+def subalgebra.is_algebraic (S : subalgebra R A) : Prop := ∀ x ∈ S, is_algebraic R x
+
+variables (R A)
+
+/-- An algebra is algebraic if all its elements are algebraic. -/
+def algebra.is_algebraic : Prop := ∀ x : A, is_algebraic R x
+
+variables {R A}
+
+/-- A subalgebra is algebraic if and only if it is algebraic an algebra. -/
+def subalgebra.is_algebraic_iff (S : subalgebra R A) :
+  S.is_algebraic ↔ @algebra.is_algebraic R S _ _ (by convert S.algebra) :=
+begin
+  delta algebra.is_algebraic subalgebra.is_algebraic,
+  rw [subtype.forall'],
+  apply forall_congr, rintro ⟨x, hx⟩,
+  apply exists_congr, intro p,
+  apply and_congr iff.rfl,
+  have h : function.injective (S.val) := subtype.val_injective,
+  conv_rhs { rw [← h.eq_iff, alg_hom.map_zero], },
+  apply eq_iff_eq_cancel_right.mpr,
+  symmetry, apply hom_eval₂,
+end
+
+/-- An algebra is algebraic if and only if it is algebraic as a subalgebra. -/
+lemma algebra.is_algebraic_iff : algebra.is_algebraic R A ↔ (⊤ : subalgebra R A).is_algebraic :=
+begin
+  delta algebra.is_algebraic subalgebra.is_algebraic,
+  simp only [algebra.mem_top, forall_prop_of_true, iff_self],
+end
+
+end
+
+section zero_ne_one
+variables (R : Type u) {A : Type v} [nonzero_comm_ring R] [comm_ring A] [algebra R A]
+
+/-- An integral element of an algebra is algebraic.-/
+lemma is_integral.is_algebraic {x : A} (h : is_integral R x) : is_algebraic R x :=
+by { rcases h with ⟨p, hp, hpx⟩, exact ⟨p, hp.ne_zero, hpx⟩ }
+
+end zero_ne_one
+
+section field
+variables (K : Type u) {A : Type v} [discrete_field K] [comm_ring A] [algebra K A]
+
+/-- An element of an algebra over a field is algebraic if and only if it is integral.-/
+lemma is_algebraic_iff_is_integral {x : A} :
+  is_algebraic K x ↔ is_integral K x :=
+begin
+  refine ⟨_, is_integral.is_algebraic K⟩,
+  rintro ⟨p, hp, hpx⟩,
+  refine ⟨_, monic_mul_leading_coeff_inv hp, _⟩,
+  rw [alg_hom.map_mul, hpx, zero_mul],
+end
+
+end field
+
+namespace algebra
+variables {K : Type*} {L : Type*} {A : Type*}
+variables [discrete_field K] [discrete_field L] [comm_ring A]
+variables [algebra K L] [algebra L A]
+
+/-- If L is an algebraic field extension of K and A is an algebraic algebra over L,
+then A is algebraic over K. -/
+lemma is_algebraic_trans (L_alg : is_algebraic K L) (A_alg : is_algebraic L A) :
+  is_algebraic K (comap K L A) :=
+begin
+  simp only [is_algebraic, is_algebraic_iff_is_integral] at L_alg A_alg ⊢,
+  exact is_integral_trans L_alg A_alg,
+end
+
+end algebra