Adjoining elements to a field #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Some lemmas on the ring generating by adjoining an element to a field.
Main statements #
lift_of_splits: IfKandLare field extensions ofFand we haves : finset Ksuch that the minimal polynomial of eachx ∈ ssplits inLthenalgebra.adjoin F sembeds inL.
noncomputable
def
alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly
(F : Type u_1)
[field F]
{R : Type u_2}
[comm_ring R]
[algebra F R]
(x : R) :
↥(algebra.adjoin F {x}) ≃ₐ[F] adjoin_root (minpoly F x)
If p is the minimal polynomial of a over F then F[a] ≃ₐ[F] F[x]/(p)
Equations
- alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly F x = (alg_equiv.of_bijective ((adjoin_root.lift_hom (minpoly F x) x _).cod_restrict (algebra.adjoin F {x}) _) _).symm
theorem
lift_of_splits
{F : Type u_1}
{K : Type u_2}
{L : Type u_3}
[field F]
[field K]
[field L]
[algebra F K]
[algebra F L]
(s : finset K) :
(∀ (x : K), x ∈ s → is_integral F x ∧ polynomial.splits (algebra_map F L) (minpoly F x)) → nonempty (↥(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.