Cardinality of algebraic numbers

In this file, we prove variants of the following result: the cardinality of algebraic numbers under an R-algebra is at most #R[X] * ℵ₀.

Although this can be used to prove that real or complex transcendental numbers exist, a more direct proof is given by Liouville.transcendental.

theorem Algebraic.infinite_of_charZero (R : Type u_1) (A : Type u_2) [CommRing R] [Ring A] [Algebra R A] [CharZero A] : {x : A | IsAlgebraic R x}.Infinite

theorem Algebraic.aleph0_le_cardinalMk_of_charZero (R : Type u_1) (A : Type u_2) [CommRing R] [Ring A] [Algebra R A] [CharZero A] : Cardinal.aleph0 ≤ Cardinal.mk { x : A // IsAlgebraic R x }

theorem Algebraic.cardinalMk_lift_le_mul (R : Type u) (A : Type v) [CommRing R] [IsDomain R] [CommRing A] [IsDomain A] [Algebra R A] [Module.IsTorsionFree R A] : Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) ≤ Cardinal.lift.{v, u} (Cardinal.mk (Polynomial R)) * Cardinal.aleph0

theorem Algebraic.cardinalMk_lift_le_max (R : Type u) (A : Type v) [CommRing R] [IsDomain R] [CommRing A] [IsDomain A] [Algebra R A] [Module.IsTorsionFree R A] : Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk R)) Cardinal.aleph0

@[simp]

theorem Algebraic.cardinalMk_lift_of_infinite (R : Type u) (A : Type v) [CommRing R] [IsDomain R] [CommRing A] [IsDomain A] [Algebra R A] [Module.IsTorsionFree R A] [Infinite R] : Cardinal.lift.{u, v} (Cardinal.mk { x : A // IsAlgebraic R x }) = Cardinal.lift.{v, u} (Cardinal.mk R)

@[simp]

theorem Algebraic.countable (R : Type u) (A : Type v) [CommRing R] [IsDomain R] [CommRing A] [IsDomain A] [Algebra R A] [Module.IsTorsionFree R A] [Countable R] : {x : A | IsAlgebraic R x}.Countable

@[simp]

theorem Algebraic.cardinalMk_of_countable_of_charZero (R : Type u) (A : Type v) [CommRing R] [IsDomain R] [CommRing A] [IsDomain A] [Algebra R A] [Module.IsTorsionFree R A] [Countable R] [CharZero A] : Cardinal.mk { x : A // IsAlgebraic R x } = Cardinal.aleph0

theorem Algebraic.cardinalMk_le_mul (R A : Type u) [CommRing R] [IsDomain R] [CommRing A] [IsDomain A] [Algebra R A] [Module.IsTorsionFree R A] : Cardinal.mk { x : A // IsAlgebraic R x } ≤ Cardinal.mk (Polynomial R) * Cardinal.aleph0

theorem Algebraic.cardinalMk_le_max (R A : Type u) [CommRing R] [IsDomain R] [CommRing A] [IsDomain A] [Algebra R A] [Module.IsTorsionFree R A] : Cardinal.mk { x : A // IsAlgebraic R x } ≤ max (Cardinal.mk R) Cardinal.aleph0

Stacks Tag 09GK

@[simp]

theorem Algebraic.cardinalMk_of_infinite (R A : Type u) [CommRing R] [IsDomain R] [CommRing A] [IsDomain A] [Algebra R A] [Module.IsTorsionFree R A] [Infinite R] : Cardinal.mk { x : A // IsAlgebraic R x } = Cardinal.mk R