feat(field_theory.intermediate_field): intermediate_field.inclusion (#…

…12596)




Co-authored-by: Sebastian-Monnet <54352341+Sebastian-Monnet@users.noreply.github.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/field_theory/intermediate_field.lean

@@ -327,6 +327,27 @@ begin
     rw [← aeval_def, aeval_coe, aeval_def, hProot, add_submonoid_class.coe_zero] },
 end
 
+/-- The map `E → F` when `E` is an intermediate field contained in the intermediate field `F`.
+
+This is the intermediate field version of `subalgebra.inclusion`. -/
+def inclusion {E F : intermediate_field K L} (hEF : E ≤ F) : E →ₐ[K] F :=
+subalgebra.inclusion hEF
+
+lemma inclusion_injective {E F : intermediate_field K L} (hEF : E ≤ F) :
+  function.injective (inclusion hEF) :=
+subalgebra.inclusion_injective hEF
+
+@[simp] lemma inclusion_self {E : intermediate_field K L}:
+  inclusion (le_refl E) = alg_hom.id K E :=
+subalgebra.inclusion_self
+
+@[simp] lemma inclusion_inclusion {E F G : intermediate_field K L} (hEF : E ≤ F) (hFG : F ≤ G)
+  (x : E) : inclusion hFG (inclusion hEF x) = inclusion (le_trans hEF hFG) x :=
+subalgebra.inclusion_inclusion hEF hFG x
+
+@[simp] lemma coe_inclusion {E F : intermediate_field K L} (hEF : E ≤ F) (e : E) :
+  (inclusion hEF e : L) = e := rfl
+
 variables {S}
 
 lemma to_subalgebra_injective {S S' : intermediate_field K L}