exists_lift_of_splits — Mathlib

English

Given an integral element s over the carrier and a splits condition, there exists a lift y with s in y.carrier and y extends x.

Русский

Для интегрального элемента s над носителем и условия разложения найдется лифт y, содержащий s в carrier и расширяющий x.

LaTeX

$$$\\exists y, x \\le y \\land s \\in y.carrier$$$

Lean4

/-- Given an integral element `s : E` over `F` whose `F`-conjugates are all in `K`,
any lift can be extended to one whose carrier contains `s`. -/
theorem exists_lift_of_splits (x : Lifts F E K) {s : E} (h1 : IsIntegral F s)
    (h2 : (minpoly F s).Splits (algebraMap F K)) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
  exists_lift_of_splits' x h1.tower_top <| h1.minpoly_splits_tower_top' <| by rwa [← x.emb.comp_algebraMap] at h2

Похожие утверждения