English
A specialized form of the previous equivalence specialized to IsAlgebraic context.
Русский
Специализированная форма эквивелентности для контекста IsAlgebraic.
LaTeX
$$Algebra.IsAlgebraic.algHomEquivAlgHomOfSplits A L hL f x = algebraMap L A (f x)$$
Lean4
/-- All `F`-embeddings of a field `K` into another field `A` factor through any subextension
of `A/F` in which the minimal polynomial of elements of `K` splits. -/
noncomputable def algHomEquivAlgHomOfSplits (L : Type*) [Field L] [Algebra F L] [Algebra L A] [IsScalarTower F L A]
(hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) : (K →ₐ[F] L) ≃ (K →ₐ[F] A) :=
(AlgEquiv.refl.arrowCongr (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L A))).trans <|
IntermediateField.algHomEquivAlgHomOfSplits A (IsScalarTower.toAlgHom F L A).fieldRange fun x ↦
splits_of_algHom (hL x) (AlgHom.rangeRestrict _)
