English
Let F, K, L be fields with F ⊆ K ⊆ L, and s a finite subset of K such that for every x ∈ s, x is integral over F and minpoly F x splits in L. Then there exists a nonempty F-algebra hom from the algebra generated by s to L.
Русский
Пусть F ⊆ K ⊆ L — поля, и s — конечный подмножество K such that для каждого x ∈ s есть интеграл над F и minpoly F x распадается в L. Тогда существует непустой F-алгебра-гомоморфизм от алгебры, сгенерированной s, в L.
LaTeX
$$$\\exists \\phi \\in \\mathrm{AlgHom}_F\\big(\\mathrm{adjoin}_F(s), L\\big)$$$
Lean4
/-- If `K` and `L` are field extensions of `F` and we have `s : Finset K` such that
the minimal polynomial of each `x ∈ s` splits in `L` then `Algebra.adjoin F s` embeds in `L`. -/
theorem lift_of_splits {F K L : Type*} [Field F] [Field K] [Field L] [Algebra F K] [Algebra F L] (s : Finset K) :
(∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
Nonempty (Algebra.adjoin F (s : Set K) →ₐ[F] L) :=
by
classical
refine Finset.induction_on s (fun _ ↦ ?_) fun a s _ ih H ↦ ?_
· rw [coe_empty, Algebra.adjoin_empty]
exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
rw [forall_mem_insert] at H
rcases H with ⟨⟨H1, H2⟩, H3⟩
obtain ⟨f⟩ := ih H3
choose H3 _ using H3
rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
set Ks := Algebra.adjoin F (s : Set K)
haveI : FiniteDimensional F Ks :=
((Submodule.fg_iff_finiteDimensional _).1 (fg_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
letI := fieldOfFiniteDimensional F Ks
letI := (f : Ks →+* L).toAlgebra
have H5 : IsIntegral Ks a := H1.tower_top
have H6 : (minpoly Ks a).Splits (algebraMap Ks L) :=
by
refine
splits_of_splits_of_dvd _ ((minpoly.monic H1).map (algebraMap F Ks)).ne_zero ((splits_map_iff _ _).2 ?_)
(minpoly.dvd _ _ ?_)
· rw [← IsScalarTower.algebraMap_eq]
exact H2
· rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]
obtain ⟨y, hy⟩ := Polynomial.exists_root_of_splits _ H6 (minpoly.degree_pos H5).ne'
exact ⟨Subalgebra.ofRestrictScalars F _ <| Algebra.adjoin.liftSingleton Ks a y hy⟩
