exists_algHom_of_adjoin_splits' — Mathlib

English

Under a framework of towers and split conditions, there exists an AlgHom extending f after adjoin operations.

Русский

В рамках башен и условий разложения существует AlgHom, удлиняющий f после операций присоединения.

LaTeX

$$$\\exists φ : E \\to_F K, \\; φ|_L = f$$$

Lean4

theorem exists_algHom_of_adjoin_splits' (hS : adjoin L S = ⊤) : ∃ φ : E →ₐ[F] K, φ.restrictDomain L = f :=
  have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits' f hK
  ⟨φ.comp (((equivOfEq hS).trans topEquiv).symm.toAlgHom.restrictScalars F), hφ⟩

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