Adjoining elements to a field

Some lemmas on the ring generated by adjoining an element to a field.

Main statements

• lift_of_splits: If K and L are field extensions of F and we have s : Finset K such that the minimal polynomial of each x ∈ s splits in L then Algebra.adjoin F s embeds in L.

def AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly (F : Type u_1) [Field F] {R : Type u_2} [CommRing R] [Algebra F R] (x : R) : { x // x ∈ Algebra.adjoin F {x} } ≃ₐ[F] AdjoinRoot (minpoly F x)

If p is the minimal polynomial of a over F then F[a] ≃ₐ[F] F[x]/(p)

Equations

• One or more equations did not get rendered due to their size.

theorem lift_of_splits {F : Type u_2} {K : Type u_3} {L : Type u_4} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (s : Finset K) : (∀ (x : K), x ∈ s → IsIntegral F x ∧ Polynomial.Splits (algebraMap F L) (minpoly F x)) → Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)

If K and L are field extensions of F and we have s : Finset K such that the minimal polynomial of each x ∈ s splits in L then Algebra.adjoin F s embeds in L.