Extension of field embeddings #

IntermediateField.exists_algHom_of_adjoin_splits' is the main result: if E/L/F is a tower of field extensions, K is another extension of F, and f is an embedding of L/F into K/F, such that the minimal polynomials of a set of generators of E/L splits in K (via f), then f extends to an embedding of E/F into K/F.

structure IntermediateField.Lifts (F : Type u_1) (E : Type u_2) (K : Type u_3) [] [] [] [Algebra F E] [Algebra F K] :
Type (max u_2 u_3)

Lifts L → K of F → K

• carrier :

The domain of a lift.

• emb : self.carrier →ₐ[F] K

The lifted RingHom, expressed as an AlgHom.

Instances For
instance IntermediateField.instPartialOrderLifts {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] :
Equations
• IntermediateField.instPartialOrderLifts =
noncomputable instance IntermediateField.instOrderBotLifts {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] :
Equations
• IntermediateField.instOrderBotLifts =
noncomputable instance IntermediateField.instInhabitedLifts {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] :
Equations
• IntermediateField.instInhabitedLifts = { default := }
theorem IntermediateField.Lifts.exists_upper_bound {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] (c : Set ()) (hc : IsChain (fun (x x_1 : ) => x x_1) c) :
∃ (ub : ), ac, a ub

A chain of lifts has an upper bound.

theorem IntermediateField.Lifts.exists_lift_of_splits' {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] (x : ) {s : E} (h1 : IsIntegral (x.carrier) s) (h2 : Polynomial.Splits x.emb.toRingHom (minpoly (x.carrier) s)) :
∃ (y : ), x y s y.carrier

Given a lift x and an integral element s : E over x.carrier whose conjugates over x.carrier are all in K, we can extend the lift to a lift whose carrier contains s.

theorem IntermediateField.Lifts.exists_lift_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] (x : ) {s : E} (h1 : ) (h2 : Polynomial.Splits () (minpoly F s)) :
∃ (y : ), x y s y.carrier

Given an integral element s : E over F whose F-conjugates are all in K, any lift can be extended to one whose carrier contains s.

theorem IntermediateField.exists_algHom_adjoin_of_splits' {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] {S : Set E} {L : Type u_4} [] [Algebra F L] [Algebra L E] [] (f : L →ₐ[F] K) (hK : sS, Polynomial.Splits f.toRingHom (minpoly L s)) :
∃ (φ : () →ₐ[F] K), φ.comp () = f
theorem IntermediateField.exists_algHom_of_adjoin_splits' {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] {S : Set E} {L : Type u_4} [] [Algebra F L] [Algebra L E] [] (f : L →ₐ[F] K) (hK : sS, Polynomial.Splits f.toRingHom (minpoly L s)) (hS : ) :
∃ (φ : E →ₐ[F] K), φ.comp () = f
theorem IntermediateField.exists_algHom_of_splits' {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] {L : Type u_4} [] [Algebra F L] [Algebra L E] [] (f : L →ₐ[F] K) (hK : ∀ (s : E), Polynomial.Splits f.toRingHom (minpoly L s)) :
∃ (φ : E →ₐ[F] K), φ.comp () = f
theorem IntermediateField.exists_algHom_adjoin_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] {S : Set E} (hK : sS, Polynomial.Splits () (minpoly F s)) {L : } (f : L →ₐ[F] K) (hL : ) :
∃ (φ : () →ₐ[F] K), φ.comp = f
theorem IntermediateField.nonempty_algHom_adjoin_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] {S : Set E} (hK : sS, Polynomial.Splits () (minpoly F s)) :
Nonempty (() →ₐ[F] K)
theorem IntermediateField.exists_algHom_of_adjoin_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] {S : Set E} (hK : sS, Polynomial.Splits () (minpoly F s)) {L : } (f : L →ₐ[F] K) (hS : ) :
∃ (φ : E →ₐ[F] K), φ.comp L.val = f
theorem IntermediateField.nonempty_algHom_of_adjoin_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] {S : Set E} (hK : sS, Polynomial.Splits () (minpoly F s)) (hS : ) :
theorem IntermediateField.exists_algHom_adjoin_of_splits_of_aeval {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] {S : Set E} (hK : sS, Polynomial.Splits () (minpoly F s)) {x : E} (hx : ) {y : K} (hy : () (minpoly F x) = 0) :
∃ (φ : () →ₐ[F] K), φ x, hx = y
theorem IntermediateField.exists_algHom_of_adjoin_splits_of_aeval {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] {S : Set E} (hK : sS, Polynomial.Splits () (minpoly F s)) (hS : ) {x : E} {y : K} (hy : () (minpoly F x) = 0) :
∃ (φ : E →ₐ[F] K), φ x = y
theorem IntermediateField.exists_algHom_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] (hK' : ∀ (s : E), Polynomial.Splits () (minpoly F s)) {L : } (f : L →ₐ[F] K) :
∃ (φ : E →ₐ[F] K), φ.comp L.val = f
theorem IntermediateField.nonempty_algHom_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] (hK' : ∀ (s : E), Polynomial.Splits () (minpoly F s)) :
theorem IntermediateField.exists_algHom_of_splits_of_aeval {F : Type u_1} {E : Type u_2} {K : Type u_3} [] [] [] [Algebra F E] [Algebra F K] (hK' : ∀ (s : E), Polynomial.Splits () (minpoly F s)) {x : E} {y : K} (hy : () (minpoly F x) = 0) :
∃ (φ : E →ₐ[F] K), φ x = y
theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits {F : Type u_1} {K : Type u_2} (L : Type u_3) [] [] [] [Algebra F L] [Algebra F K] (hA : ∀ (x : K), Polynomial.Splits () (minpoly F x)) [] (x : K) :
(Set.range fun (ψ : K →ₐ[F] L) => ψ x) = (minpoly F x).rootSet L

Let K/F be an algebraic extension of fields and L a field in which all the minimal polynomial over F of elements of K splits. Then, for x ∈ K, the images of x by the F-algebra morphisms from K to L are exactly the roots in L of the minimal polynomial of x over F.