# 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) [] {R : Type u_2} [] [Algebra F R] (x : R) :

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

Equations
Instances For
noncomputable def Algebra.adjoin.liftSingleton (F : Type u_1) [] {S : Type u_2} {T : Type u_3} [] [] [Algebra F S] [Algebra F T] (x : S) (y : T) (h : () (minpoly F x) = 0) :

Produce an algebra homomorphism Adjoin R {x} →ₐ[R] T sending x to a root of x's minimal polynomial in T.

Equations
Instances For
theorem Polynomial.lift_of_splits {F : Type u_2} {K : Type u_3} {L : Type u_4} [] [] [] [Algebra F K] [Algebra F L] (s : ) :
(xs, Polynomial.Splits () (minpoly F x))Nonempty (() →ₐ[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.

theorem IsIntegral.mem_range_algHom_of_minpoly_splits {R : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra R K] [Algebra R L] {x : L} (int : ) (h : Polynomial.Splits () (minpoly R x)) (f : K →ₐ[R] L) :
x f.range
theorem IsIntegral.mem_range_algebraMap_of_minpoly_splits {R : Type u_1} {K : Type u_2} {L : Type u_3} [] [] [] [Algebra R K] [Algebra R L] {x : L} (int : ) (h : Polynomial.Splits () (minpoly R x)) [Algebra K L] [] :
x ().range
theorem IsIntegral.minpoly_splits_tower_top' {R : Type u_1} {K : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [Algebra R K] [Algebra R M] [Algebra K M] [] {x : M} (int : ) {f : K →+* L} (h : Polynomial.Splits (f.comp ()) (minpoly R x)) :
theorem IsIntegral.minpoly_splits_tower_top {R : Type u_1} {K : Type u_2} {L : Type u_3} {M : Type u_4} [] [] [] [] [Algebra R K] [Algebra R L] [Algebra R M] [Algebra K M] [] {x : M} (int : ) [Algebra K L] [] (h : Polynomial.Splits () (minpoly R x)) :
theorem Subalgebra.adjoin_rank_le {F : Type u_5} (E : Type u_6) {K : Type u_7} [] [] [Ring K] [SMul F E] [Algebra E K] [Algebra F K] [] (L : ) [Module.Free F L] :
Module.rank E () Module.rank F L

If K / E / F is a ring extension tower, L is a subalgebra of K / F, then [E[L] : E] ≤ [L : F].