Cardinalities of free constructions

This file shows that all the free constructions over α have cardinality max #α ℵ₀, and are thus infinite, and specifically countable over countable generators.

Combined with the ring Fin n for the finite cases, this lets us show that there is a CommRing of any cardinality.

instance instInfiniteFreeMonoidOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeMonoid α)

instance instInfiniteFreeAddMonoidOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeAddMonoid α)

instance instInfiniteFreeGroupOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeGroup α)

instance instInfiniteFreeAddGroupOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeAddGroup α)

instance instInfiniteFreeAbelianGroupOfNonempty (α : Type u) [Nonempty α] : Infinite (FreeAbelianGroup α)

instance instInfiniteFreeRing (α : Type u) : Infinite (FreeRing α)

instance instInfiniteFreeCommRing (α : Type u) : Infinite (FreeCommRing α)

instance instCountableFreeMonoid (α : Type u) [Countable α] : Countable (FreeMonoid α)

instance instCountableFreeAddMonoid (α : Type u) [Countable α] : Countable (FreeAddMonoid α)

instance instCountableFreeGroup (α : Type u) [Countable α] : Countable (FreeGroup α)

instance instCountableFreeAddGroup (α : Type u) [Countable α] : Countable (FreeAddGroup α)

instance instCountableFreeAbelianGroup (α : Type u) [Countable α] : Countable (FreeAbelianGroup α)

instance instCountableFreeRing (α : Type u) [Countable α] : Countable (FreeRing α)

instance instCountableFreeCommRing (α : Type u) [Countable α] : Countable (FreeCommRing α)

theorem Cardinal.mk_abelianization_le (G : Type u) [Group G] : mk (Abelianization G) ≤ mk G

@[simp]

theorem Cardinal.mk_freeMonoid (α : Type u) [Nonempty α] : mk (FreeMonoid α) = max (mk α) aleph0

@[simp]

theorem Cardinal.mk_freeAddMonoid (α : Type u) [Nonempty α] : mk (FreeAddMonoid α) = max (mk α) aleph0

@[simp]

theorem Cardinal.mk_freeGroup (α : Type u) [Nonempty α] : mk (FreeGroup α) = max (mk α) aleph0

@[simp]

theorem Cardinal.mk_freeAddGroup (α : Type u) [Nonempty α] : mk (FreeAddGroup α) = max (mk α) aleph0

@[simp]

theorem Cardinal.mk_freeAbelianGroup (α : Type u) [Nonempty α] : mk (FreeAbelianGroup α) = max (mk α) aleph0

@[simp]

theorem Cardinal.mk_freeRing (α : Type u) : mk (FreeRing α) = max (mk α) aleph0

@[simp]

theorem Cardinal.mk_freeCommRing (α : Type u) : mk (FreeCommRing α) = max (mk α) aleph0

instance nonempty_commRing (α : Type u) [Nonempty α] : Nonempty (CommRing α)

A commutative ring can be constructed on any non-empty type.

See also Infinite.nonempty_field.

@[simp]

theorem nonempty_commRing_iff (α : Type u) : Nonempty (CommRing α) ↔ Nonempty α

@[simp]

theorem nonempty_ring_iff (α : Type u) : Nonempty (Ring α) ↔ Nonempty α

@[simp]

theorem nonempty_commSemiring_iff (α : Type u) : Nonempty (CommSemiring α) ↔ Nonempty α

@[simp]

theorem nonempty_semiring_iff (α : Type u) : Nonempty (Semiring α) ↔ Nonempty α