English
Given a normal closure, and a target L' with suitable splits, there is an algebra homomorphism from L to L' extending the embedding used to construct the lift.
Русский
С учетом нормального замыкания и целевого L' с подходящими распадами существует алгебраический гомоморфизм от L к L', расширяющий заданное вложение, используемое при построении lift.
LaTeX
$$$\forall L',\ (splits\ :\ \forall x:K, (minpoly F x).Splits (algebraMap F L'))\Rightarrow\exists \varphi: L\to_F L'\;\text{ such that }$$
Lean4
/-- `normalClosure F K L` is a valid normal closure if `K/F` is algebraic
and all minimal polynomials of `K/F` splits in `L/F`. -/
theorem isNormalClosure_normalClosure : IsNormalClosure F K (normalClosure F K L) :=
by
rw [isNormalClosure_iff]; constructor
· rw [normalClosure_eq_iSup_adjoin_of_splits splits]
exact fun x ↦
splits_of_splits (splits x)
((IntermediateField.subset_adjoin F _).trans <| SetLike.coe_subset_coe.mpr <| by apply le_iSup _ x)
simp_rw [normalClosure, ← top_le_iff]
refine fun x _ ↦ ((⨆ f : K →ₐ[F] L, f.fieldRange).val).injective.mem_set_image |>.mp ?_
rw [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, coe_val, ← IntermediateField.coe_val, ← IntermediateField.coe_map,
IntermediateField.map_iSup]
refine (iSup_le fun f ↦ ?_ : normalClosure F K L ≤ _) x.2
refine le_iSup_of_le (f.codRestrict _ fun x ↦ f.fieldRange_le_normalClosure ⟨x, rfl⟩) ?_
rw [AlgHom.map_fieldRange, val, AlgHom.val_comp_codRestrict]
