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) [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] : Type (max u_2 u_3)

Lifts L → K of F → K

• carrier : IntermediateField F E

  The domain of a lift.

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

  The lifted RingHom, expressed as an AlgHom.

instance IntermediateField.instPartialOrderLifts {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] : PartialOrder (IntermediateField.Lifts F E K)

Equations

• IntermediateField.instPartialOrderLifts = PartialOrder.mk ⋯

noncomputable instance IntermediateField.instOrderBotLifts {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] : OrderBot (IntermediateField.Lifts F E K)

Equations

• IntermediateField.instOrderBotLifts = OrderBot.mk ⋯

noncomputable instance IntermediateField.instInhabitedLifts {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] : Inhabited (IntermediateField.Lifts F E K)

Equations

• IntermediateField.instInhabitedLifts = { default := ⊥ }

theorem IntermediateField.Lifts.exists_upper_bound {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (c : Set (IntermediateField.Lifts F E K)) (hc : IsChain (fun (x1 x2 : IntermediateField.Lifts F E K) => x1 ≤ x2) c) : ∃ (ub : IntermediateField.Lifts F E K), ∀ a ∈ c, 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} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (x : IntermediateField.Lifts F E K) {s : E} (h1 : IsIntegral (↥x.carrier) s) (h2 : Polynomial.Splits x.emb.toRingHom (minpoly (↥x.carrier) s)) : ∃ (y : IntermediateField.Lifts F E K), 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} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (x : IntermediateField.Lifts F E K) {s : E} (h1 : IsIntegral F s) (h2 : Polynomial.Splits (algebraMap F K) (minpoly F s)) : ∃ (y : IntermediateField.Lifts F E K), 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} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} {L : Type u_4} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (f : L →ₐ[F] K) (hK : ∀ s ∈ S, IsIntegral L s ∧ Polynomial.Splits f.toRingHom (minpoly L s)) : ∃ (φ : ↥(IntermediateField.adjoin L S) →ₐ[F] K), AlgHom.restrictDomain L φ = f

theorem IntermediateField.exists_algHom_of_adjoin_splits' {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} {L : Type u_4} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (f : L →ₐ[F] K) (hK : ∀ s ∈ S, IsIntegral L s ∧ Polynomial.Splits f.toRingHom (minpoly L s)) (hS : IntermediateField.adjoin L S = ⊤) : ∃ (φ : E →ₐ[F] K), AlgHom.restrictDomain L φ = f

theorem IntermediateField.exists_algHom_of_splits' {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {L : Type u_4} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E] (f : L →ₐ[F] K) (hK : ∀ (s : E), IsIntegral L s ∧ Polynomial.Splits f.toRingHom (minpoly L s)) : ∃ (φ : E →ₐ[F] K), AlgHom.restrictDomain L φ = f

theorem IntermediateField.exists_algHom_adjoin_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) {L : IntermediateField F E} (f : ↥L →ₐ[F] K) (hL : L ≤ IntermediateField.adjoin F S) : ∃ (φ : ↥(IntermediateField.adjoin F S) →ₐ[F] K), φ.comp (IntermediateField.inclusion hL) = f

theorem IntermediateField.nonempty_algHom_adjoin_of_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) : Nonempty (↥(IntermediateField.adjoin F S) →ₐ[F] K)

theorem IntermediateField.exists_algHom_of_adjoin_splits {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) {L : IntermediateField F E} (f : ↥L →ₐ[F] K) (hS : IntermediateField.adjoin F S = ⊤) : ∃ (φ : 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} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) (hS : IntermediateField.adjoin F S = ⊤) : Nonempty (E →ₐ[F] K)

theorem IntermediateField.exists_algHom_adjoin_of_splits_of_aeval {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) {x : E} {y : K} (hx : x ∈ IntermediateField.adjoin F S) (hy : (Polynomial.aeval y) (minpoly F x) = 0) : ∃ (φ : ↥(IntermediateField.adjoin F S) →ₐ[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} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] {S : Set E} (hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) {x : E} {y : K} (hS : IntermediateField.adjoin F S = ⊤) (hy : (Polynomial.aeval y) (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} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (hK' : ∀ (s : E), IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) {L : IntermediateField F E} (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} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (hK' : ∀ (s : E), IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) : Nonempty (E →ₐ[F] K)

theorem IntermediateField.exists_algHom_of_splits_of_aeval {F : Type u_1} {E : Type u_2} {K : Type u_3} [Field F] [Field E] [Field K] [Algebra F E] [Algebra F K] (hK' : ∀ (s : E), IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) {x : E} {y : K} (hy : (Polynomial.aeval y) (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) [Field F] [Field K] [Field L] [Algebra F L] [Algebra F K] (hA : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) [Algebra.IsAlgebraic F K] (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.