English
If g is distinguished at I and g divides f.map, then there exists g' ∈ R[X] with g'.map * C(leadingCoeff g) = g.
Русский
Если g отличимо по I и делит отображение f.map, существует g' ∈ R[X] такое, что g'.map * C(leadingCoeff g) = g.
LaTeX
$$$\\exists g' : R[X], g'.map (algebraMap R K) * (C\\; leadingCoeff g) = g$$$
Lean4
theorem mem_lifts_of_monic_of_dvd_map {f : R[X]} (hf : f.Monic) {g : K[X]} (hg : g.Monic)
(hd : g ∣ f.map (algebraMap R K)) : g ∈ lifts (algebraMap (integralClosure R K) K) :=
by
have :=
mem_lift_of_splits_of_roots_mem_range (integralClosure R g.SplittingField)
((splits_id_iff_splits _).2 <| SplittingField.splits g) (hg.map _) fun a ha =>
(SetLike.ext_iff.mp (integralClosure R g.SplittingField).range_algebraMap _).mpr <|
roots_mem_integralClosure hf ?_
· rw [lifts_iff_coeff_lifts, ← RingHom.coe_range, Subalgebra.range_algebraMap] at this
refine (lifts_iff_coeff_lifts _).2 fun n => ?_
rw [← RingHom.coe_range, Subalgebra.range_algebraMap]
obtain ⟨p, hp, he⟩ := SetLike.mem_coe.mp (this n); use p, hp
rw [IsScalarTower.algebraMap_eq R K, coeff_map, ← eval₂_map, eval₂_at_apply] at he
rw [eval₂_eq_eval_map]; apply (injective_iff_map_eq_zero _).1 _ _ he
apply RingHom.injective
rw [aroots_def, IsScalarTower.algebraMap_eq R K _, ← map_map]
refine Multiset.mem_of_le (roots.le_of_dvd ((hf.map _).map _).ne_zero ?_) ha
exact map_dvd (algebraMap K g.SplittingField) hd
