Documentation

Mathlib.FieldTheory.Extension

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.

Instances For
    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] :
    Equations
    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] :
    Equations
    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] :
    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 (x x_1 : IntermediateField.Lifts F E K) => x x_1) c) :
    ∃ (ub : IntermediateField.Lifts F E K), 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} [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 : sS, IsIntegral L s Polynomial.Splits f.toRingHom (minpoly L s)) :
    ∃ (φ : (IntermediateField.adjoin L S) →ₐ[F] K), φ.comp (IsScalarTower.toAlgHom F L (IntermediateField.adjoin L S)) = 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 : sS, IsIntegral L s Polynomial.Splits f.toRingHom (minpoly L s)) (hS : IntermediateField.adjoin L S = ) :
    ∃ (φ : E →ₐ[F] K), φ.comp (IsScalarTower.toAlgHom F L E) = 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), φ.comp (IsScalarTower.toAlgHom F L E) = 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 : sS, 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 : sS, IsIntegral F s Polynomial.Splits (algebraMap F K) (minpoly F s)) :
    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 : sS, 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 : sS, IsIntegral F s Polynomial.Splits (algebraMap F K) (minpoly F s)) (hS : IntermediateField.adjoin F S = ) :
    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 : sS, IsIntegral F s Polynomial.Splits (algebraMap F K) (minpoly F s)) {x : E} (hx : x IntermediateField.adjoin F S) {y : K} (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 : sS, IsIntegral F s Polynomial.Splits (algebraMap F K) (minpoly F s)) (hS : IntermediateField.adjoin F S = ) {x : E} {y : K} (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)) :
    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.