feat(field_theory/algebraic_closure): any two algebraic closures are …

…isomorphic (#9231)

src/field_theory/is_alg_closed/algebraic_closure.lean

@@ -5,32 +5,24 @@ Authors: Kenny Lau
 -/
 import algebra.direct_limit
 import field_theory.is_alg_closed.basic
-
 /-!
-# Algebraically Closed Field
+# Algebraic Closure
 
-In this file we define the typeclass for algebraically closed fields and algebraic closures,
-and prove some of their properties.
+In this file we construct the algebraic closure of a 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`.
-
-- `is_alg_closed.lift` is a map from an algebraic extension `L` of `K`, into any algebraically
-  closed extension of `K`.
-
-## TODO
-
-Show that any two algebraic closures are isomorphic
+- `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.
 
 ## Tags
 
 algebraic closure, algebraically closed
-
 -/
+
 universes u v w
 noncomputable theory
 open_locale classical big_operators

src/field_theory/is_alg_closed/basic.lean

@@ -5,23 +5,33 @@ Authors: Kenny Lau
 -/
 import field_theory.splitting_field
 /-!
-# Algebraic Closure
+# Algebraically Closed Field
 
-In this file we construct the algebraic closure of a field
+In this file we define the typeclass for algebraically closed fields and algebraic closures,
+and prove some of their properties.
 
 ## Main Definitions
 
-- `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.
+- `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`.
+
+- `is_alg_closed.lift` is a map from an algebraic extension `L` of `K`, into any algebraically
+  closed extension of `K`.
+
+- `is_alg_closure.equiv` is a proof that any two algebraic closures of the
+  same field are isomorphic.
+
+## TODO
+
+Show that any two algebraic closures are isomorphic
 
 ## Tags
 
 algebraic closure, algebraically closed
--/
 
+-/
 universes u v w
 
 open_locale classical big_operators
@@ -237,7 +247,8 @@ begin
   letI : algebra N M := (maximal_subfield_with_hom M hL).emb.to_ring_hom.to_algebra,
   cases is_alg_closed.exists_aeval_eq_zero M (minpoly N x)
     (ne_of_gt (minpoly.degree_pos
-      ((is_algebraic_iff_is_integral _).1 (algebra.is_algebraic_of_larger_field hL x)))) with y hy,
+      ((is_algebraic_iff_is_integral _).1
+        (algebra.is_algebraic_of_larger_base _ _ hL x)))) with y hy,
   let O : subalgebra N L := algebra.adjoin N {(x : L)},
   let larger_emb := ((adjoin_root.lift_hom (minpoly N x) y hy).comp
      (alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly N x).to_alg_hom),
@@ -274,3 +285,27 @@ include hL
   eq.rec_on (lift.subfield_with_hom.maximal_subfield_with_hom_eq_top M hL).symm algebra.to_top
 
 end is_alg_closed
+
+namespace is_alg_closure
+
+variables (K : Type u) [field K] (L : Type v) (M : Type w) [field L] [algebra K L]
+  [field M] [algebra K M]  [is_alg_closure K L] [is_alg_closure K M]
+
+local attribute [instance] is_alg_closure.alg_closed
+
+/-- A (random) isomorphism between two algebraic closures of `K`. -/
+noncomputable def equiv : L ≃ₐ[K] M :=
+let f : L →ₐ[K] M := is_alg_closed.lift K L M is_alg_closure.algebraic in
+alg_equiv.of_bijective f
+  ⟨ring_hom.injective f.to_ring_hom,
+    begin
+      letI : algebra L M := ring_hom.to_algebra f,
+      letI : is_scalar_tower K L M :=
+        is_scalar_tower.of_algebra_map_eq (by simp [ring_hom.algebra_map_to_algebra]),
+      show function.surjective (algebra_map L M),
+      exact is_alg_closed.algebra_map_surjective_of_is_algebraic
+        (algebra.is_algebraic_of_larger_base K L is_alg_closure.algebraic),
+    end⟩
+
+
+end is_alg_closure

src/ring_theory/algebraic.lean

@@ -116,11 +116,15 @@ begin
   exact is_integral_trans L_alg A_alg,
 end
 
+variables (K L)
+
 /-- If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K -/
-lemma is_algebraic_of_larger_field (A_alg : is_algebraic K A) : is_algebraic L A :=
+lemma is_algebraic_of_larger_base (A_alg : is_algebraic K A) : is_algebraic L A :=
 λ x, let ⟨p, hp⟩ := A_alg x in
 ⟨p.map (algebra_map _ _), map_ne_zero hp.1, by simp [hp.2]⟩
 
+variables {K L}
+
 /-- A field extension is algebraic if it is finite. -/
 lemma is_algebraic_of_finite [finite : finite_dimensional K L] : is_algebraic K L :=
 λ x, (is_algebraic_iff_is_integral _).mpr (is_integral_of_submodule_noetherian ⊤