Cardinality of free algebras #
This file contains some results about the cardinality of FreeAlgebra
,
parallel to that of MvPolynomial
.
@[simp]
theorem
FreeAlgebra.cardinalMk_eq_max_lift
(R : Type u)
[CommSemiring R]
(X : Type v)
[Nonempty X]
[Nontrivial R]
:
Cardinal.mk (FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk X))) Cardinal.aleph0
@[simp]
theorem
FreeAlgebra.cardinalMk_le_max_lift
(R : Type u)
[CommSemiring R]
(X : Type v)
:
Cardinal.mk (FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk X))) Cardinal.aleph0
theorem
FreeAlgebra.cardinalMk_eq_max
(R : Type u)
[CommSemiring R]
(X : Type u)
[Nonempty X]
[Nontrivial R]
:
theorem
Algebra.lift_cardinalMk_adjoin_le
(R : Type u)
[CommSemiring R]
{A : Type v}
[Semiring A]
[Algebra R A]
(s : Set A)
:
Cardinal.lift.{u, v} (Cardinal.mk ↥(adjoin R s)) ≤ max (max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk ↑s))) Cardinal.aleph0
theorem
Algebra.cardinalMk_adjoin_le
(R : Type u)
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
(s : Set A)
: