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.
Reference #
[Isa80] Roots of Polynomials in Algebraic Extensions of Fields, The American Mathematical Monthly
instance
IntermediateField.Lifts.instPartialOrder
{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.Lifts.instPartialOrder = PartialOrder.mk ⋯
noncomputable instance
IntermediateField.Lifts.instOrderBot
{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.Lifts.instOrderBot = OrderBot.mk ⋯
theorem
IntermediateField.Lifts.le_of_carrier_le_iSup
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[Field F]
[Field E]
[Field K]
[Algebra F E]
[Algebra F K]
{ι : Sort u_4}
{ρ : ι → IntermediateField.Lifts F E K}
{σ τ : IntermediateField.Lifts F E K}
(hσ : ∀ (i : ι), ρ i ≤ σ)
(hτ : ∀ (i : ι), ρ i ≤ τ)
(carrier_le : σ.carrier ≤ ⨆ (i : ι), (ρ i).carrier)
:
σ ≤ τ
def
IntermediateField.Lifts.IsExtendible
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[Field F]
[Field E]
[Field K]
[Algebra F E]
[Algebra F K]
(σ : IntermediateField.Lifts F E K)
:
σ : L →ₐ[F] K is an extendible lift ("extendible pair" in [Isa80]) if for every
intermediate field M that is finite-dimensional over L, σ extends to some M →ₐ[F] K.
In our definition we only require M to be finitely generated over L, which is equivalent
if the ambient field E is algebraic over F (which is the case in our main application).
We also allow the domain of the extension to be an intermediate field that properly contains M,
since one can always restrict the domain to M.
Instances For
noncomputable def
IntermediateField.Lifts.union
{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)
:
IntermediateField.Lifts F E K
The union of a chain of lifts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
IntermediateField.Lifts.le_union
{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)
⦃σ : IntermediateField.Lifts F E K⦄
(hσ : σ ∈ c)
:
σ ≤ IntermediateField.Lifts.union c hc
theorem
IntermediateField.Lifts.carrier_union
{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)
:
(IntermediateField.Lifts.union c hc).carrier = ⨆ (i : ↑c), (↑i).carrier
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.union_isExtendible
{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)
[alg : Algebra.IsAlgebraic F E]
[Nonempty ↑c]
(hext : ∀ σ ∈ c, σ.IsExtendible)
:
(IntermediateField.Lifts.union c hc).IsExtendible
theorem
IntermediateField.Lifts.nonempty_algHom_of_exist_lifts_finset
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[Field F]
[Field E]
[Field K]
[Algebra F E]
[Algebra F K]
[alg : Algebra.IsAlgebraic F E]
(h : ∀ (S : Finset E), ∃ (σ : IntermediateField.Lifts F E K), ↑S ⊆ ↑σ.carrier)
:
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 = ⊤)
:
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 = ⊤)
:
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)
:
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)
:
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)
:
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)
:
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.