exists_algHom_of_adjoin_splits_of_aeval

English

For given S and f, there exists φ: adjoin_F S →_F K with φ ∘ inclusion = f whenever all elements of S satisfy IsIntegral and minpoly splits in K.

Русский

Для данного S и f существует φ: adjoin_F S →_F K, удовлетворяющий φ ∘ inclusion = f, если для каждого s ∈ S выполнено IsIntegral и minpoly распадается в K.

LaTeX

$$$(\forall s ∈ S)\ IsIntegral F s \wedge (minpoly F s).Splits (algebraMap F K) \Rightarrow ∃ φ : adjoin F S →_F K, φ \circ (inclusion hL) = f$$$

Lean4

theorem exists_algHom_of_adjoin_splits_of_aeval : ∃ φ : E →ₐ[F] K, φ x = y :=
  have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits_of_aeval hK (hS ▸ mem_top) hy
  ⟨φ.comp ((equivOfEq hS).trans topEquiv).symm.toAlgHom, hφ⟩

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