English
The cardinality of an algebraically closed R-algebra is bounded by the maximum of the cardinalities of R, of a transcendence basis, and of the natural numbers.
Русский
Кардинал алгебраически замкнутое над R-алгебраическое поле не превосходит максимум кардиналов R, трансцендентной базы и ℵ0.
LaTeX
$$$\\#K \\le \\max(\\#R, \\#\\iota, \\aleph_0)$ (up to the appropriate lifts).$$
Lean4
/-- The cardinality of an algebraically closed `R`-algebra is less than or equal to
the maximum of the cardinality of `R`, the cardinality of a transcendence basis and
`ℵ₀`
For a simpler, but less universe-polymorphic statement, see
`IsAlgClosed.cardinal_le_max_transcendence_basis'` -/
theorem cardinal_le_max_transcendence_basis (hv : IsTranscendenceBasis R v) :
Cardinal.lift.{max u w} #K ≤ max (max (Cardinal.lift.{max v w} #R) (Cardinal.lift.{max u v} #ι)) ℵ₀ :=
calc
Cardinal.lift.{max u w} #K ≤ Cardinal.lift.{max u w} (max #(Algebra.adjoin R (Set.range v)) ℵ₀) :=
by
letI := isAlgClosure_of_transcendence_basis v hv
simpa using Algebra.IsAlgebraic.cardinalMk_le_max (Algebra.adjoin R (Set.range v)) K
_ = Cardinal.lift.{v} (max #(MvPolynomial ι R) ℵ₀) := by
rw [lift_max, ← Cardinal.lift_mk_eq.2 ⟨hv.1.aevalEquiv.toEquiv⟩, lift_aleph0, ← lift_aleph0.{max u v w, max u w},
← lift_max, lift_umax.{max u w, v}]
_ ≤ Cardinal.lift.{v} (max (max (max (Cardinal.lift #R) (Cardinal.lift #ι)) ℵ₀) ℵ₀) :=
(lift_le.2 (max_le_max MvPolynomial.cardinalMk_le_max_lift le_rfl))
_ = _ := by simp
