feat: cardinalities of free constructions and Nonempty (CommRing α) (#18364)

[Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Does.20every.20type.20permit.20a.20semiring.3F/near/479347521)

Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>

Author: eric-wieser

Mathlib.lean

@@ -4300,6 +4300,7 @@ import Mathlib.SetTheory.Cardinal.Divisibility
 import Mathlib.SetTheory.Cardinal.ENat
 import Mathlib.SetTheory.Cardinal.Finite
 import Mathlib.SetTheory.Cardinal.Finsupp
+import Mathlib.SetTheory.Cardinal.Free
 import Mathlib.SetTheory.Cardinal.PartENat
 import Mathlib.SetTheory.Cardinal.SchroederBernstein
 import Mathlib.SetTheory.Cardinal.Subfield

Mathlib/FieldTheory/Cardinality.lean

@@ -59,16 +59,9 @@ theorem Fintype.not_isField_of_card_not_prime_pow {α} [Fintype α] [Ring α] :
 
 /-- Any infinite type can be endowed a field structure. -/
 theorem Infinite.nonempty_field {α : Type u} [Infinite α] : Nonempty (Field α) := by
-  letI K := FractionRing (MvPolynomial α <| ULift.{u} ℚ)
-  suffices #α = #K by
-    obtain ⟨e⟩ := Cardinal.eq.1 this
-    exact ⟨e.field⟩
-  rw [← IsLocalization.card K (MvPolynomial α <| ULift.{u} ℚ)⁰ le_rfl]
-  apply le_antisymm
-  · refine
-      ⟨⟨fun a => MvPolynomial.monomial (Finsupp.single a 1) (1 : ULift.{u} ℚ), fun x y h => ?_⟩⟩
-    simpa [MvPolynomial.monomial_eq_monomial_iff, Finsupp.single_eq_single_iff] using h
-  · simp
+  suffices #α = #(FractionRing (MvPolynomial α <| ULift.{u} ℚ)) from
+    (Cardinal.eq.1 this).map (·.field)
+  simp
 
 /-- There is a field structure on type if and only if its cardinality is a prime power. -/
 theorem Field.nonempty_iff {α : Type u} : Nonempty (Field α) ↔ IsPrimePow #α := by

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -528,6 +528,12 @@ instance : Group (FreeGroup α) where
       List.recOn L rfl fun ⟨x, b⟩ tl ih =>
           Eq.trans (Quot.sound <| by simp [invRev, one_eq_mk]) ih
 
+@[to_additive (attr := simp)]
+theorem pow_mk (n : ℕ) : mk L ^ n = mk (List.join <| List.replicate n L) :=
+  match n with
+  | 0 => rfl
+  | n + 1 => by rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.join_cons]
+
 /-- `of` is the canonical injection from the type to the free group over that type by sending each
 element to the equivalence class of the letter that is the element. -/
 @[to_additive "`of` is the canonical injection from the type to the free group over that type
@@ -908,6 +914,17 @@ theorem reduce.cons (x) :
         if x.1 = hd.1 ∧ x.2 = not hd.2 then tl else x :: hd :: tl :=
   rfl
 
+@[to_additive (attr := simp)]
+theorem reduce_replicate (n : ℕ) (x : α × Bool) :
+    reduce (.replicate n x) = .replicate n x := by
+  induction n with
+  | zero => simp [reduce]
+  | succ n ih =>
+    rw [List.replicate_succ, reduce.cons, ih]
+    cases n with
+    | zero => simp
+    | succ n => simp [List.replicate_succ]
+
 /-- The first theorem that characterises the function `reduce`: a word reduces to its maximal
   reduction. -/
 @[to_additive "The first theorem that characterises the function `reduce`: a word reduces to its
@@ -1066,6 +1083,11 @@ theorem reduce_toWord : ∀ x : FreeGroup α, reduce (toWord x) = toWord x := by
 theorem toWord_one : (1 : FreeGroup α).toWord = [] :=
   rfl
 
+@[to_additive (attr := simp)]
+theorem toWord_of_pow (a : α) (n : ℕ) : (of a ^ n).toWord = List.replicate n (a, true) := by
+  rw [of, pow_mk, List.join_replicate_singleton, toWord]
+  exact reduce_replicate _ _
+
 @[to_additive (attr := simp)]
 theorem toWord_eq_nil_iff {x : FreeGroup α} : x.toWord = [] ↔ x = 1 :=
   toWord_injective.eq_iff' toWord_one
@@ -1174,6 +1196,15 @@ theorem norm_mul_le (x y : FreeGroup α) : norm (x * y) ≤ norm x + norm y :=
     _ ≤ (x.toWord ++ y.toWord).length := norm_mk_le
     _ = norm x + norm y := List.length_append _ _
 
+@[to_additive (attr := simp)]
+theorem norm_of_pow (a : α) (n : ℕ) : norm (of a ^ n) = n := by
+  rw [norm, toWord_of_pow, List.length_replicate]
+
+@[to_additive]
+theorem norm_surjective [Nonempty α] : Function.Surjective (norm (α := α)) := by
+  let ⟨a⟩ := ‹Nonempty α›
+  exact Function.RightInverse.surjective <| norm_of_pow a
+
 end Metric
 
 end FreeGroup

Mathlib/RingTheory/Localization/Cardinality.lean

@@ -51,3 +51,7 @@ theorem card (S : Submonoid R) [IsLocalization S L] (hS : S ≤ R⁰) : #R = #L
   (Cardinal.mk_le_of_injective (IsLocalization.injective L hS)).antisymm (card_le S)
 
 end IsLocalization
+
+@[simp]
+theorem Cardinal.mk_fractionRing (R : Type u) [CommRing R] : #(FractionRing R) = #R :=
+  IsLocalization.card (FractionRing R) R⁰ le_rfl |>.symm

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -1477,6 +1477,7 @@ theorem nat_lt_aleph0 (n : ℕ) : (n : Cardinal.{u}) < ℵ₀ :=
 @[simp]
 theorem one_lt_aleph0 : 1 < ℵ₀ := by simpa using nat_lt_aleph0 1
 
+@[simp]
 theorem one_le_aleph0 : 1 ≤ ℵ₀ :=
   one_lt_aleph0.le
 
@@ -1761,6 +1762,13 @@ theorem mk_punit : #PUnit = 1 :=
 theorem mk_unit : #Unit = 1 :=
   mk_punit
 
+@[simp] theorem mk_additive : #(Additive α) = #α := rfl
+
+@[simp] theorem mk_multiplicative : #(Multiplicative α) = #α := rfl
+
+@[to_additive (attr := simp)] theorem mk_mulOpposite : #(MulOpposite α) = #α :=
+  mk_congr MulOpposite.opEquiv.symm
+
 theorem mk_singleton {α : Type u} (x : α) : #({x} : Set α) = 1 :=
   mk_eq_one _
 

Mathlib/SetTheory/Cardinal/Free.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2024 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser, Daniel Weber
+-/
+import Mathlib.Data.Finsupp.Fintype
+import Mathlib.GroupTheory.FreeAbelianGroupFinsupp
+import Mathlib.RingTheory.FreeCommRing
+import Mathlib.SetTheory.Cardinal.Arithmetic
+import Mathlib.SetTheory.Cardinal.Finsupp
+
+/-!
+# Cardinalities of free constructions
+
+This file shows that all the free constructions over `α` have cardinality `max #α ℵ₀`,
+and are thus infinite.
+
+Combined with the ring `Fin n` for the finite cases, this lets us show that there is a `CommRing` of
+any cardinality.
+-/
+
+universe u
+variable (α : Type u)
+
+section Infinite
+
+@[to_additive]
+instance [Nonempty α] : Infinite (FreeMonoid α) := inferInstanceAs <| Infinite (List α)
+
+@[to_additive]
+instance [Nonempty α] : Infinite (FreeGroup α) := by
+  classical
+  exact Infinite.of_surjective FreeGroup.norm FreeGroup.norm_surjective
+
+instance [Nonempty α] : Infinite (FreeAbelianGroup α) :=
+  (FreeAbelianGroup.equivFinsupp α).toEquiv.infinite_iff.2 inferInstance
+
+instance : Infinite (FreeRing α) := by unfold FreeRing; infer_instance
+
+instance : Infinite (FreeCommRing α) := by unfold FreeCommRing; infer_instance
+
+end Infinite
+
+namespace Cardinal
+
+theorem mk_abelianization_le (G : Type u) [Group G] :
+    #(Abelianization G) ≤ #G := Cardinal.mk_le_of_surjective <| surjective_quotient_mk _
+
+@[to_additive (attr := simp)]
+theorem mk_freeMonoid [Nonempty α] : #(FreeMonoid α) = max #α ℵ₀ :=
+    Cardinal.mk_list_eq_max_mk_aleph0 _
+
+@[to_additive (attr := simp)]
+theorem mk_freeGroup [Nonempty α] : #(FreeGroup α) = max #α ℵ₀ := by
+  classical
+  apply le_antisymm
+  · apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq
+    simp [Cardinal.mk_list_eq_max_mk_aleph0]
+    obtain hα | hα := lt_or_le #α ℵ₀
+    · simp only [hα.le, max_eq_right, max_eq_right_iff]
+      exact (mul_lt_aleph0 hα (nat_lt_aleph0 2)).le
+    · rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
+        Cardinal.mul_eq_left hα _ (by simp)]
+      exact (nat_lt_aleph0 2).le.trans hα
+  · apply max_le
+    · exact mk_le_of_injective FreeGroup.of_injective
+    · simp
+
+@[simp]
+theorem mk_freeAbelianGroup [Nonempty α] : #(FreeAbelianGroup α) = max #α ℵ₀ := by
+  rw [Cardinal.mk_congr (FreeAbelianGroup.equivFinsupp α).toEquiv]
+  simp
+
+@[simp]
+theorem mk_freeRing : #(FreeRing α) = max #α ℵ₀ := by
+  cases isEmpty_or_nonempty α <;> simp [FreeRing]
+
+@[simp]
+theorem mk_freeCommRing : #(FreeCommRing α) = max #α ℵ₀ := by
+  cases isEmpty_or_nonempty α <;> simp [FreeCommRing]
+
+end Cardinal
+
+section Nonempty
+
+/-- A commutative ring can be constructed on any non-empty type.
+
+See also `Infinite.nonempty_field`. -/
+instance nonempty_commRing [Nonempty α] : Nonempty (CommRing α) := by
+  obtain hR | hR := finite_or_infinite α
+  · obtain ⟨x⟩ := nonempty_fintype α
+    have : NeZero (Fintype.card α) := ⟨by inhabit α; simp⟩
+    classical
+    obtain ⟨e⟩ := Fintype.truncEquivFin α
+    exact ⟨e.commRing⟩
+  · have ⟨e⟩ : Nonempty (α ≃ FreeCommRing α) := by simp [← Cardinal.eq]
+    exact ⟨e.commRing⟩
+
+@[simp]
+theorem nonempty_commRing_iff : Nonempty (CommRing α) ↔ Nonempty α :=
+  ⟨Nonempty.map (·.zero), fun _ => nonempty_commRing _⟩
+
+@[simp]
+theorem nonempty_ring_iff : Nonempty (Ring α) ↔ Nonempty α :=
+  ⟨Nonempty.map (·.zero), fun _ => (nonempty_commRing _).map (·.toRing)⟩
+
+@[simp]
+theorem nonempty_commSemiring_iff : Nonempty (CommSemiring α) ↔ Nonempty α :=
+  ⟨Nonempty.map (·.zero), fun _ => (nonempty_commRing _).map (·.toCommSemiring)⟩
+
+@[simp]
+theorem nonempty_semiring_iff : Nonempty (Semiring α) ↔ Nonempty α :=
+  ⟨Nonempty.map (·.zero), fun _ => (nonempty_commRing _).map (·.toSemiring)⟩
+
+end Nonempty