English
The lifted cardinality of L is bounded by the cardinality of a certain sigma-polynomial construction over R, i.e., lift #L ≤ #(Σ p ∈ R[X], { x ∈ L | x is a root of p }).
Русский
Поднятая кардинальность L ограничена кардинальностью множества пар (p,x) с p ∈ R[X] и x корень p.
LaTeX
$$$\\operatorname{lift} \\#L \\le \\#\\Bigl\\{ (p,x) : p \\in R[X], x \\in L, x \\in p^{\\text{aroots}}(L) \\Bigr\\}$$$
Lean4
theorem lift_cardinalMk_le_sigma_polynomial : lift.{u} #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) :=
by
have :=
@lift_mk_le_lift_mk_of_injective L (Σ p : R[X], {x : L | x ∈ p.aroots L})
(fun x : L =>
let p := Classical.indefiniteDescription _ (Algebra.IsAlgebraic.isAlgebraic x)
⟨p.1, x, by
dsimp
have := (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective R L)).2 p.2.1
rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map, ← Polynomial.aeval_def, p.2.2]⟩)
fun x y => by
intro h
simp only [Set.coe_setOf, ne_eq, Set.mem_setOf_eq, Sigma.mk.inj_iff] at h
refine (Subtype.heq_iff_coe_eq ?_).1 h.2
simp only [h.1, forall_true_iff]
rwa [lift_umax, lift_id'.{v}] at this
