feat(field_theory/algebraic_closure): algebraically closed fields have no nontrivial algebraic extensions (#5537)

Author: dtumad

src/field_theory/algebraic_closure.lean

@@ -67,6 +67,25 @@ lemma degree_eq_one_of_irreducible [is_alg_closed k] {p : polynomial k} (h_nz :
   p.degree = 1 :=
 degree_eq_one_of_irreducible_of_splits h_nz hp (polynomial.splits' _)
 
+lemma algebra_map_surjective_of_is_integral {k K : Type*} [field k] [domain K]
+  [hk : is_alg_closed k] [algebra k K] (hf : algebra.is_integral k K) :
+  function.surjective (algebra_map k K) :=
+begin
+  refine λ x, ⟨-((minimal_polynomial (hf x)).coeff 0), _⟩,
+  have hq : (minimal_polynomial (hf x)).leading_coeff = 1 := minimal_polynomial.monic (hf x),
+  have h : (minimal_polynomial (hf x)).degree = 1 := degree_eq_one_of_irreducible k
+    (minimal_polynomial.ne_zero (hf x)) (minimal_polynomial.irreducible (hf x)),
+  have : (aeval x (minimal_polynomial (hf x))) = 0 := minimal_polynomial.aeval (hf x),
+  rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul,
+    aeval_add, aeval_X, aeval_C, add_eq_zero_iff_eq_neg] at this,
+  exact (ring_hom.map_neg (algebra_map k K) ((minimal_polynomial (hf x)).coeff 0)).symm ▸ this.symm,
+end
+
+lemma algebra_map_surjective_of_is_algebraic {k K : Type*} [field k] [domain K]
+  [hk : is_alg_closed k] [algebra k K] (hf : algebra.is_algebraic k K) :
+  function.surjective (algebra_map k K) :=
+algebra_map_surjective_of_is_integral ((is_algebraic_iff_is_integral' k).mp hf)
+
 end is_alg_closed
 
 instance complex.is_alg_closed : is_alg_closed ℂ :=

src/ring_theory/algebraic.lean

@@ -23,7 +23,7 @@ open_locale classical
 open polynomial
 
 section
-variables (R : Type u) {A : Type v} [comm_ring R] [comm_ring A] [algebra R A]
+variables (R : Type u) {A : Type v} [comm_ring R] [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 :=
@@ -65,7 +65,7 @@ end
 end
 
 section zero_ne_one
-variables (R : Type u) {A : Type v} [comm_ring R] [nontrivial R] [comm_ring A] [algebra R A]
+variables (R : Type u) {A : Type v} [comm_ring R] [nontrivial R] [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 :=
@@ -74,7 +74,7 @@ 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} [field K] [comm_ring A] [algebra K A]
+variables (K : Type u) {A : Type v} [field K] [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} :
@@ -86,6 +86,11 @@ begin
   rw [← aeval_def, alg_hom.map_mul, hpx, zero_mul],
 end
 
+lemma is_algebraic_iff_is_integral' :
+  algebra.is_algebraic K A ↔ algebra.is_integral K A :=
+⟨λ h x, (is_algebraic_iff_is_integral K).mp (h x),
+  λ h x, (is_algebraic_iff_is_integral K).mpr (h x)⟩
+
 end field
 
 namespace algebra