English
Under suitable generating set S of E and splitting conditions in K, there is a bijection between F-embeddings of E into E and algebra F-homomorphisms from E to K.
Русский
При подходящей генерации S поля E и условии расщепления в K существует биекция между вложениями F в E и F-алгоморфизмами из E в K.
LaTeX
$$$\operatorname{Emb}_F(E) \cong (E \to_{F} K)\,$$
Lean4
/-- A random bijection between `Field.Emb F E` and `E →ₐ[F] K` if `E = F(S)` such that every
element `s` of `S` is integral (= algebraic) over `F` and whose minimal polynomial splits in `K`.
Combined with `Field.instInhabitedEmb`, it can be viewed as a stronger version of
`IntermediateField.nonempty_algHom_of_adjoin_splits`. -/
def embEquivOfAdjoinSplits {S : Set E} (hS : adjoin F S = ⊤)
(hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)) : Emb F E ≃ (E →ₐ[F] K) :=
have : Algebra.IsAlgebraic F (⊤ : IntermediateField F E) := (hS ▸ isAlgebraic_adjoin (S := S) fun x hx ↦ (hK x hx).1)
have halg := (topEquiv (F := F) (E := E)).isAlgebraic
Classical.choice <|
Function.Embedding.antisymm
(halg.algHomEmbeddingOfSplits (fun _ ↦ splits_of_mem_adjoin F E (S := S) hK (hS ▸ mem_top)) _)
(halg.algHomEmbeddingOfSplits (fun _ ↦ IsAlgClosed.splits_codomain _) _)
