English
Given L with R-algebra structure and a splitting condition for minpoly of every x ∈ K, there is an equivalence between K→ₐ[F] L and K→ₐ[F] A.
Русский
При наличии условия разрыва минимального многочлена на каждом x ∈ K существует эквивалентность между гомоморфизмами K→ₐ[F] L и K→ₐ[F] A.
LaTeX
$$Equiv (K →ₐ[F] L) (K →ₐ[F] A)$$
Lean4
/-- All `F`-embeddings of a field `K` into another field `A` factor through any intermediate
field of `A/F` in which the minimal polynomial of elements of `K` splits. -/
@[simps]
def algHomEquivAlgHomOfSplits (L : IntermediateField F A) (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) :
(K →ₐ[F] L) ≃ (K →ₐ[F] A) where
toFun := L.val.comp
invFun
f :=
f.codRestrict _ fun x ↦
((Algebra.IsIntegral.isIntegral x).map f).mem_intermediateField_of_minpoly_splits <| by
rw [minpoly.algHom_eq f f.injective]; exact hL x
