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) = Cardinal.lift.{v, u} (Cardinal.mk R) ⊔ Cardinal.lift.{u, v} (Cardinal.mk X) ⊔ Cardinal.aleph0

@[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_le_max_lift (R : Type u) [CommSemiring R] (X : Type v) : Cardinal.mk (FreeAlgebra R X) ≤ 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] : 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) : Cardinal.lift.{u, v} (Cardinal.mk ↥(adjoin R s)) ≤ 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) : Cardinal.mk ↥(adjoin R s) ≤ Cardinal.mk R ⊔ Cardinal.mk ↑s ⊔ Cardinal.aleph0