mathlib4/Mathlib/SetTheory/Cardinal/Free.lean at master · Stars1233/mathlib4 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
/-
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
-/
module

public import Mathlib.Algebra.FreeAbelianGroup.Finsupp
public import Mathlib.Algebra.Ring.TransferInstance
public import Mathlib.Data.Finsupp.Fintype
public import Mathlib.Data.ZMod.Defs
public import Mathlib.GroupTheory.FreeGroup.Reduce
public import Mathlib.RingTheory.FreeCommRing
public import Mathlib.SetTheory.Cardinal.Arithmetic
public 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, 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.
-/

@[expose] public section

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

section Countable

variable [Countable α]

@[to_additive]
instance : Countable (FreeMonoid α) := by unfold FreeMonoid; infer_instance

@[to_additive]
instance : Countable (FreeGroup α) := Quotient.countable

instance : Countable (FreeAbelianGroup α) := Quotient.countable

instance : Countable (FreeRing α) := Quotient.countable

instance : Countable (FreeCommRing α) := by
  unfold FreeCommRing Multiplicative
  infer_instance

end Countable

namespace Cardinal

theorem mk_abelianization_le (G : Type u) [Group G] :
    #(Abelianization G) ≤ #G := Cardinal.mk_le_of_surjective Quotient.mk_surjective

@[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 only [mk_list_eq_max_mk_aleph0, mk_prod, lift_uzero, mk_fintype, Fintype.card_bool,
      Nat.cast_ofNat, lift_ofNat]
    obtain hα | hα := lt_or_ge #α ℵ₀
    · simp only [hα.le, max_eq_right, max_eq_right_iff]
      exact (mul_lt_aleph0 hα natCast_lt_aleph0).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 natCast_le_aleph0.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 simp⟩
    classical
    obtain ⟨e⟩ := Fintype.truncEquivFin α
    exact ⟨open scoped Fin.CommRing in 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