embEquivOfIsAlgClosed — Mathlib

English

For a field tower F ⊆ E ⊆ K with E/K algebraic, there is a natural equivalence between Emb F E × Emb E K and Emb F K.

Русский

Для поля F ⊆ E ⊆ K, где E ⊆ K зто алгебраично, существует естественная эквивалентность между вложениями F→E и E→K и вложениями F→K.

LaTeX

$$$\mathrm{Emb}_F(E) \times \mathrm{Emb}_E(K) \simeq \mathrm{Emb}_F(K)$$$

Lean4

/-- A random bijection between `Field.Emb F E` and `E →ₐ[F] K` when `E / F` is algebraic
and `K / F` is algebraically closed. -/
def embEquivOfIsAlgClosed [Algebra.IsAlgebraic F E] [IsAlgClosed K] : Emb F E ≃ (E →ₐ[F] K) :=
  embEquivOfAdjoinSplits F E K (adjoin_univ F E) fun s _ ↦
    ⟨Algebra.IsIntegral.isIntegral s, IsAlgClosed.splits_codomain _⟩

Похожие утверждения