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]
:
@[simp]
theorem
FreeAlgebra.cardinalMk_eq_lift
(R : Type u)
[CommSemiring R]
(X : Type v)
[IsEmpty X]
:
Cardinal.mk (FreeAlgebra R X) = Cardinal.lift.{v, u} (Cardinal.mk R)
theorem
FreeAlgebra.cardinalMk_eq_one
(R : Type u)
[CommSemiring R]
(X : Type v)
[Subsingleton R]
:
Cardinal.mk (FreeAlgebra R X) = 1
theorem
FreeAlgebra.cardinalMk_eq_max
(R : Type u)
[CommSemiring R]
(X : Type u)
[Nonempty X]
[Nontrivial R]
:
Cardinal.mk (FreeAlgebra R X) = Cardinal.mk R ⊔ Cardinal.mk X ⊔ Cardinal.aleph0
theorem
FreeAlgebra.cardinalMk_eq
(R : Type u)
[CommSemiring R]
(X : Type u)
[IsEmpty X]
:
Cardinal.mk (FreeAlgebra R X) = Cardinal.mk R
theorem
FreeAlgebra.cardinalMk_le_max
(R : Type u)
[CommSemiring R]
(X : Type u)
:
Cardinal.mk (FreeAlgebra R X) ≤ Cardinal.mk R ⊔ Cardinal.mk X ⊔ Cardinal.aleph0
theorem
Algebra.lift_cardinalMk_adjoin_le
(R : Type u)
[CommSemiring R]
{A : Type v}
[Semiring A]
[Algebra R A]
(s : Set A)
:
theorem
Algebra.cardinalMk_adjoin_le
(R : Type u)
[CommSemiring R]
{A : Type u}
[Semiring A]
[Algebra R A]
(s : Set A)
:
Cardinal.mk ↥(Algebra.adjoin R s) ≤ Cardinal.mk R ⊔ Cardinal.mk ↑s ⊔ Cardinal.aleph0