feat(field_theory/intermediate_field): Produce an intermediate field …

…from a subalgebra satisfying `is_field`. (#15659)

This construction came up when proving that if `p` splits in `L/K`, then `p.is_splitting_field K (adjoin K (p.root_set L))`.

src/field_theory/intermediate_field.lean

@@ -190,11 +190,30 @@ def subalgebra.to_intermediate_field (S : subalgebra K L) (inv_mem : ∀ 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 :=
+@[simp] lemma to_intermediate_field_to_subalgebra (S : intermediate_field K L) :
+  S.to_subalgebra.to_intermediate_field (λ x, S.inv_mem) = S :=
 by { ext, refl }
 
+/-- Turn a subalgebra satisfying `is_field` into an intermediate_field -/
+def subalgebra.to_intermediate_field' (S : subalgebra K L) (hS : is_field S) :
+  intermediate_field K L :=
+S.to_intermediate_field $ λ x hx, begin
+  by_cases hx0 : x = 0,
+  { rw [hx0, inv_zero],
+    exact S.zero_mem },
+  letI hS' := hS.to_field,
+  obtain ⟨y, hy⟩ := hS.mul_inv_cancel (show (⟨x, hx⟩ : S) ≠ 0, from subtype.ne_of_val_ne hx0),
+  rw [subtype.ext_iff, S.coe_mul, S.coe_one, subtype.coe_mk, mul_eq_one_iff_inv_eq₀ hx0] at hy,
+  exact hy.symm ▸ y.2,
+end
+
+@[simp] lemma to_subalgebra_to_intermediate_field' (S : subalgebra K L) (hS : is_field S) :
+  (S.to_intermediate_field' hS).to_subalgebra = S :=
+by { ext, refl }
+
+@[simp] lemma to_intermediate_field'_to_subalgebra (S : intermediate_field K L) :
+  S.to_subalgebra.to_intermediate_field' (field.to_is_field S) = 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)
@@ -476,7 +495,7 @@ def subalgebra_equiv_intermediate_field (alg : algebra.is_algebraic 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 _ _,
+  right_inv := 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)