exists_algHom_of_adjoin_splits — Mathlib

English

There exists an algebra homomorphism from adjoin_F S to K extending f, under the splitting hypothesis for S.

Русский

Существует алгебраический гомоморфизм от adjoin_F S в K, который расширяет f, при условии разложения для S.

LaTeX

$$$\exists φ : adjoin F S \to_F K, φ.comp (inclusion hL) = f$$$

Lean4

theorem exists_algHom_of_adjoin_splits : ∃ φ : E →ₐ[F] K, φ.comp L.val = f :=
  have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits hK f (hS.symm ▸ le_top)
  ⟨φ.comp ((equivOfEq hS).trans topEquiv).symm.toAlgHom, hφ⟩

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