feat(ring_theory/algebraic): if L / K is algebraic, then the subalg…

…ebras are fields (#4903)

src/field_theory/intermediate_field.lean

@@ -6,6 +6,7 @@ Authors: Anne Baanen
 
 import field_theory.subfield
 import field_theory.tower
+import ring_theory.algebraic
 
 /-!
 # Intermediate fields
@@ -32,12 +33,6 @@ i.e. it is a `subfield L` and a `subalgebra K L`.
 Intermediate fields are defined with a structure extending `subfield` and `subalgebra`.
 A `subalgebra` is closed under all operations except `⁻¹`,
 
-## TODO
-
- * `field.adjoin` currently returns a `subalgebra`, this should become an
-   `intermediate_field`. The lattice structure on `intermediate_field` will
-   follow from the adjunction given by `field.adjoin`.
-
 ## Tags
 intermediate field, field extension
 -/
@@ -185,6 +180,17 @@ def subalgebra.to_intermediate_field (S : subalgebra K L) (inv_mem : ∀ x ∈ S
   inv_mem' := inv_mem,
   .. S }
 
+@[simp] lemma to_subalgebra_to_intermediate_field
+  (S : subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) :
+  (S.to_intermediate_field inv_mem).to_subalgebra = S :=
+by { ext, refl }
+
+@[simp] lemma to_intermediate_field_to_subalgebra
+  (S : intermediate_field K L) (inv_mem : ∀ x ∈ S.to_subalgebra, x⁻¹ ∈ S) :
+  S.to_subalgebra.to_intermediate_field inv_mem = S :=
+by { ext, refl }
+
+
 /-- Turn a subfield of `L` containing the image of `K` into an intermediate field -/
 def subfield.to_intermediate_field (S : subfield L)
   (algebra_map_mem : ∀ x, algebra_map K L x ∈ S) :
@@ -323,3 +329,22 @@ eq_of_le_of_findim_le' h_le h_findim.le
 end finite_dimensional
 
 end intermediate_field
+
+/-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields.  -/
+def subalgebra_equiv_intermediate_field (alg : algebra.is_algebraic K L) :
+  subalgebra K L ≃o intermediate_field K L :=
+{ to_fun := λ S, S.to_intermediate_field (λ x hx, S.inv_mem_of_algebraic (alg (⟨x, hx⟩ : S))),
+  inv_fun := λ S, S.to_subalgebra,
+  left_inv := λ S, to_subalgebra_to_intermediate_field _ _,
+  right_inv := λ S, to_intermediate_field_to_subalgebra _ _,
+  map_rel_iff' := λ S S', iff.rfl }
+
+@[simp] lemma mem_subalgebra_equiv_intermediate_field (alg : algebra.is_algebraic K L)
+  {S : subalgebra K L} {x : L} :
+  x ∈ subalgebra_equiv_intermediate_field alg S ↔ x ∈ S :=
+iff.rfl
+
+@[simp] lemma mem_subalgebra_equiv_intermediate_field_symm (alg : algebra.is_algebraic K L)
+  {S : intermediate_field K L} {x : L} :
+  x ∈ (subalgebra_equiv_intermediate_field alg).symm S ↔ x ∈ S :=
+iff.rfl

src/ring_theory/algebra_tower.lean

@@ -232,6 +232,8 @@ namespace subalgebra
 
 open is_scalar_tower
 
+section semiring
+
 variables (R) {S A} [comm_semiring R] [comm_semiring S] [semiring A]
 variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
 
@@ -255,6 +257,19 @@ def of_under {R A B : Type*} [comm_semiring R] [comm_semiring A] [semiring B]
 { commutes' := λ r, (f.commutes (algebra_map R S r)).trans (algebra_map_apply R S B r).symm,
   .. f }
 
+end semiring
+
+section comm_semiring
+
+variables (R) {S A} [comm_semiring R] [comm_semiring S] [comm_semiring A]
+variables [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
+
+@[simp] lemma aeval_coe {S : subalgebra R A} {x : S} {p : polynomial R} :
+  polynomial.aeval (x : A) p = polynomial.aeval x p :=
+(algebra_map_aeval R S A x p).symm
+
+end comm_semiring
+
 end subalgebra
 
 namespace is_scalar_tower

src/ring_theory/algebraic.lean

@@ -128,3 +128,72 @@ begin
   refine ⟨⟨_, x_integral⟩, ⟨_, y_integral⟩, _, rfl⟩,
   exact λ h, a_ne_zero (inj _ (subtype.ext_iff_val.mp h))
 end
+section field
+
+variables {K L : Type*} [field K] [field L] [algebra K L] (A : subalgebra K L)
+
+lemma inv_eq_of_aeval_div_X_ne_zero {x : L} {p : polynomial K}
+  (aeval_ne : aeval x (div_X p) ≠ 0) :
+  x⁻¹ = aeval x (div_X p) / (aeval x p - algebra_map _ _ (p.coeff 0)) :=
+begin
+  rw [inv_eq_iff, inv_div, div_eq_iff, sub_eq_iff_eq_add, mul_comm],
+  conv_lhs { rw ← div_X_mul_X_add p },
+  rw [alg_hom.map_add, alg_hom.map_mul, aeval_X, aeval_C],
+  exact aeval_ne
+end
+
+lemma inv_eq_of_root_of_coeff_zero_ne_zero {x : L} {p : polynomial K}
+  (aeval_eq : aeval x p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) :
+  x⁻¹ = - (aeval x (div_X p) / algebra_map _ _ (p.coeff 0)) :=
+begin
+  convert inv_eq_of_aeval_div_X_ne_zero (mt (λ h, (algebra_map K L).injective _) coeff_zero_ne),
+  { rw [aeval_eq, zero_sub, div_neg] },
+  rw ring_hom.map_zero,
+  convert aeval_eq,
+  conv_rhs { rw ← div_X_mul_X_add p },
+  rw [alg_hom.map_add, alg_hom.map_mul, h, zero_mul, zero_add, aeval_C]
+end
+
+lemma subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {x : A} {p : polynomial K}
+  (aeval_eq : aeval x p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) : (x⁻¹ : L) ∈ A :=
+begin
+  have : (x⁻¹ : L) = aeval x (div_X p) / (aeval x p - algebra_map _ _ (p.coeff 0)),
+  { rw [aeval_eq, submodule.coe_zero, zero_sub, div_neg],
+    convert inv_eq_of_root_of_coeff_zero_ne_zero _ coeff_zero_ne,
+    { rw subalgebra.aeval_coe },
+    { simpa using aeval_eq } },
+  rw [this, div_eq_mul_inv, aeval_eq, submodule.coe_zero, zero_sub, ← ring_hom.map_neg,
+      ← ring_hom.map_inv],
+  exact A.mul_mem (aeval x p.div_X).2 (A.algebra_map_mem _),
+end
+
+lemma subalgebra.inv_mem_of_algebraic {x : A} (hx : is_algebraic K (x : L)) : (x⁻¹ : L) ∈ A :=
+begin
+  obtain ⟨p, ne_zero, aeval_eq⟩ := hx,
+  replace aeval_eq : aeval x p = 0,
+  { rw ← submodule.coe_eq_zero,
+    convert aeval_eq,
+    exact is_scalar_tower.algebra_map_aeval K A L _ _ },
+  revert ne_zero aeval_eq,
+  refine p.rec_on_horner _ _ _,
+  { intro h,
+    contradiction },
+  { intros p a hp ha ih ne_zero aeval_eq,
+    refine A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq _,
+    rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl] },
+  { intros p hp ih ne_zero aeval_eq,
+    rw [alg_hom.map_mul, aeval_X, mul_eq_zero] at aeval_eq,
+    cases aeval_eq with aeval_eq x_eq,
+    { exact ih hp aeval_eq },
+    { rw [x_eq, submodule.coe_zero, inv_zero],
+      exact A.zero_mem } }
+end
+
+/-- In an algebraic extension L/K, an intermediate subalgebra is a field. -/
+lemma subalgebra.is_field_of_algebraic (hKL : algebra.is_algebraic K L) : is_field A :=
+{ mul_inv_cancel := λ a ha, ⟨
+        ⟨a⁻¹, A.inv_mem_of_algebraic (hKL a)⟩,
+        subtype.ext (mul_inv_cancel (mt submodule.coe_eq_zero.mp ha))⟩,
+  .. subalgebra.integral_domain A }
+
+end field