English
Under algebraicity of K/F and the assumption that every minpoly of x ∈ K splits in L, there exists an embedding from K-algebras into L that, extended by normalClosure, yields a canonical inclusion.
Русский
При алгебраичности K/F и условии, что каждый minpoly x разделяется в L, существует вложение F-алгебр из K в L, которое вместе с нормальным замыканием образует каноническое включение.
LaTeX
$$$\text{AlgHomEmbeddingOfSplits}(F,K,L,h)(K\to_F L')\hookrightarrow (K\to_F L)$$$
Lean4
/-- An extension `L/F` in which every minimal polynomial of `K/F` splits is maximal with respect
to `F`-embeddings of `K`, in the sense that `K →ₐ[F] L` achieves maximal cardinality.
We construct an explicit injective function from an arbitrary `K →ₐ[F] L'` into `K →ₐ[F] L`,
using an embedding of `normalClosure F K L'` into `L`. -/
noncomputable def algHomEmbeddingOfSplits [Algebra.IsAlgebraic F K] (h : ∀ x : K, (minpoly F x).Splits (algebraMap F L))
(L' : Type*) [Field L'] [Algebra F L'] : (K →ₐ[F] L') ↪ (K →ₐ[F] L) :=
let φ : ↑(⨆ x : K, IntermediateField.adjoin F ((minpoly F x).rootSet L')) →ₐ[F] L :=
Nonempty.some <| by
rw [← gc.l_iSup]
refine nonempty_algHom_adjoin_of_splits fun x hx ↦ ?_
obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx
refine ⟨isAlgebraic_iff_isIntegral.mp (isAlgebraic_of_mem_rootSet hx), ?_⟩
by_cases iy : IsIntegral F y
· exact splits_of_splits_of_dvd _ (minpoly.ne_zero iy) (h y) (minpoly.dvd F x (mem_rootSet.mp hx).2)
· simp [minpoly.eq_zero iy] at hx
let φ' := (φ.comp <| inclusion normalClosure_le_iSup_adjoin)
{ toFun := φ'.comp ∘ (normalClosure.algHomEquiv F K L').symm
inj' := fun _ _ h ↦
(normalClosure.algHomEquiv F K L').symm.injective <|
by
rw [DFunLike.ext'_iff] at h ⊢
exact φ'.injective.comp_left h }
