English
If there exists a lift φ from L to K that extends f on a subfield and the conjugates split, then there exists an AlgHom extending the given map with adjusted domain.
Русский
Если существует отображение φ из L в K, которое продолжает f на подполе и согласовано с разложением, тогда существует AlgHom, расширяющий заданную карту.
LaTeX
$$$\\forall {f: L \\to K}, (\\forall s,\\; s\\in S \\to \\text{Splits}) \\Rightarrow \\exists φ, AlgHom.restrictDomain L φ = f$$$
Lean4
/-- Given a lift `x` and an integral element `s : E` over `x.carrier` whose conjugates over
`x.carrier` are all in `K`, we can extend the lift to a lift whose carrier contains `s`. -/
theorem exists_lift_of_splits' (x : Lifts F E K) {s : E} (h1 : IsIntegral x.carrier s)
(h2 : (minpoly x.carrier s).Splits x.emb.toRingHom) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
have I2 := (minpoly.degree_pos h1).ne'
letI : Algebra x.carrier K := x.emb.toRingHom.toAlgebra
let carrier := x.carrier⟮s⟯.restrictScalars F
letI : Algebra x.carrier carrier := x.carrier⟮s⟯.toSubalgebra.algebra
let φ : carrier →ₐ[x.carrier] K :=
((algHomAdjoinIntegralEquiv x.carrier h1).symm
⟨rootOfSplits x.emb.toRingHom h2 I2,
by
rw [mem_aroots, and_iff_right (minpoly.ne_zero h1)]
exact map_rootOfSplits x.emb.toRingHom h2 I2⟩)
⟨⟨carrier,
(@algHomEquivSigma F x.carrier carrier K _ _ _ _ _ _ _ _ (IsScalarTower.of_algebraMap_eq fun _ ↦ rfl)).symm
⟨x.emb, φ⟩⟩,
⟨fun z hz ↦ algebraMap_mem x.carrier⟮s⟯ ⟨z, hz⟩, φ.commutes⟩, mem_adjoin_simple_self x.carrier s⟩
