-
Notifications
You must be signed in to change notification settings - Fork 5
/
Center.lean
238 lines (192 loc) · 7.77 KB
/
Center.lean
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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
/-
Copyright (c) 2021 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser, Jireh Loreaux
! This file was ported from Lean 3 source module group_theory.subsemigroup.center
! leanprover-community/mathlib commit 1ac8d4304efba9d03fa720d06516fac845aa5353
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Algebra.Ring.Defs
import Mathbin.GroupTheory.Subsemigroup.Operations
/-!
# Centers of magmas and semigroups
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
## Main definitions
* `set.center`: the center of a magma
* `subsemigroup.center`: the center of a semigroup
* `set.add_center`: the center of an additive magma
* `add_subsemigroup.center`: the center of an additive semigroup
We provide `submonoid.center`, `add_submonoid.center`, `subgroup.center`, `add_subgroup.center`,
`subsemiring.center`, and `subring.center` in other files.
-/
variable {M : Type _}
namespace Set
variable (M)
#print Set.center /-
/-- The center of a magma. -/
@[to_additive add_center " The center of an additive magma. "]
def center [Mul M] : Set M :=
{z | ∀ m, m * z = z * m}
#align set.center Set.center
#align set.add_center Set.addCenter
-/
#print Set.mem_center_iff /-
@[to_additive mem_add_center]
theorem mem_center_iff [Mul M] {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g :=
Iff.rfl
#align set.mem_center_iff Set.mem_center_iff
#align set.mem_add_center Set.mem_addCenter_iff
-/
#print Set.decidableMemCenter /-
instance decidableMemCenter [Mul M] [∀ a : M, Decidable <| ∀ b : M, b * a = a * b] :
DecidablePred (· ∈ center M) := fun _ => decidable_of_iff' _ (mem_center_iff M)
#align set.decidable_mem_center Set.decidableMemCenter
-/
#print Set.one_mem_center /-
@[simp, to_additive zero_mem_add_center]
theorem one_mem_center [MulOneClass M] : (1 : M) ∈ Set.center M := by simp [mem_center_iff]
#align set.one_mem_center Set.one_mem_center
#align set.zero_mem_add_center Set.zero_mem_addCenter
-/
#print Set.zero_mem_center /-
@[simp]
theorem zero_mem_center [MulZeroClass M] : (0 : M) ∈ Set.center M := by simp [mem_center_iff]
#align set.zero_mem_center Set.zero_mem_center
-/
variable {M}
#print Set.mul_mem_center /-
@[simp, to_additive add_mem_add_center]
theorem mul_mem_center [Semigroup M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
a * b ∈ Set.center M := fun g => by rw [mul_assoc, ← hb g, ← mul_assoc, ha g, mul_assoc]
#align set.mul_mem_center Set.mul_mem_center
#align set.add_mem_add_center Set.add_mem_addCenter
-/
#print Set.inv_mem_center /-
@[simp, to_additive neg_mem_add_center]
theorem inv_mem_center [Group M] {a : M} (ha : a ∈ Set.center M) : a⁻¹ ∈ Set.center M := fun g => by
rw [← inv_inj, mul_inv_rev, inv_inv, ← ha, mul_inv_rev, inv_inv]
#align set.inv_mem_center Set.inv_mem_center
#align set.neg_mem_add_center Set.neg_mem_addCenter
-/
#print Set.add_mem_center /-
@[simp]
theorem add_mem_center [Distrib M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
a + b ∈ Set.center M := fun c => by rw [add_mul, mul_add, ha c, hb c]
#align set.add_mem_center Set.add_mem_center
-/
@[simp]
theorem neg_mem_center [Ring M] {a : M} (ha : a ∈ Set.center M) : -a ∈ Set.center M := fun c => by
rw [← neg_mul_comm, ha (-c), neg_mul_comm]
#align set.neg_mem_center Set.neg_mem_centerₓ
#print Set.subset_center_units /-
@[to_additive subset_add_center_add_units]
theorem subset_center_units [Monoid M] : (coe : Mˣ → M) ⁻¹' center M ⊆ Set.center Mˣ :=
fun a ha b => Units.ext <| ha _
#align set.subset_center_units Set.subset_center_units
#align set.subset_add_center_add_units Set.subset_addCenter_add_units
-/
#print Set.center_units_subset /-
theorem center_units_subset [GroupWithZero M] : Set.center Mˣ ⊆ (coe : Mˣ → M) ⁻¹' center M :=
fun a ha b => by
obtain rfl | hb := eq_or_ne b 0
· rw [MulZeroClass.zero_mul, MulZeroClass.mul_zero]
· exact units.ext_iff.mp (ha (Units.mk0 _ hb))
#align set.center_units_subset Set.center_units_subset
-/
#print Set.center_units_eq /-
/-- In a group with zero, the center of the units is the preimage of the center. -/
theorem center_units_eq [GroupWithZero M] : Set.center Mˣ = (coe : Mˣ → M) ⁻¹' center M :=
Subset.antisymm center_units_subset subset_center_units
#align set.center_units_eq Set.center_units_eq
-/
#print Set.inv_mem_center₀ /-
@[simp]
theorem inv_mem_center₀ [GroupWithZero M] {a : M} (ha : a ∈ Set.center M) : a⁻¹ ∈ Set.center M :=
by
obtain rfl | ha0 := eq_or_ne a 0
· rw [inv_zero]; exact zero_mem_center M
rcases IsUnit.mk0 _ ha0 with ⟨a, rfl⟩
rw [← Units.val_inv_eq_inv_val]
exact center_units_subset (inv_mem_center (subset_center_units ha))
#align set.inv_mem_center₀ Set.inv_mem_center₀
-/
#print Set.div_mem_center /-
@[simp, to_additive sub_mem_add_center]
theorem div_mem_center [Group M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
a / b ∈ Set.center M := by
rw [div_eq_mul_inv]
exact mul_mem_center ha (inv_mem_center hb)
#align set.div_mem_center Set.div_mem_center
#align set.sub_mem_add_center Set.sub_mem_addCenter
-/
#print Set.div_mem_center₀ /-
@[simp]
theorem div_mem_center₀ [GroupWithZero M] {a b : M} (ha : a ∈ Set.center M)
(hb : b ∈ Set.center M) : a / b ∈ Set.center M :=
by
rw [div_eq_mul_inv]
exact mul_mem_center ha (inv_mem_center₀ hb)
#align set.div_mem_center₀ Set.div_mem_center₀
-/
variable (M)
#print Set.center_eq_univ /-
@[simp, to_additive add_center_eq_univ]
theorem center_eq_univ [CommSemigroup M] : center M = Set.univ :=
Subset.antisymm (subset_univ _) fun x _ y => mul_comm y x
#align set.center_eq_univ Set.center_eq_univ
#align set.add_center_eq_univ Set.addCenter_eq_univ
-/
end Set
namespace Subsemigroup
section
variable (M) [Semigroup M]
#print Subsemigroup.center /-
/-- The center of a semigroup `M` is the set of elements that commute with everything in `M` -/
@[to_additive
"The center of a semigroup `M` is the set of elements that commute with everything in\n`M`"]
def center : Subsemigroup M where
carrier := Set.center M
mul_mem' a b := Set.mul_mem_center
#align subsemigroup.center Subsemigroup.center
#align add_subsemigroup.center AddSubsemigroup.center
-/
@[to_additive]
theorem coe_center : ↑(center M) = Set.center M :=
rfl
#align subsemigroup.coe_center Subsemigroup.coe_center
#align add_subsemigroup.coe_center AddSubsemigroup.coe_center
variable {M}
#print Subsemigroup.mem_center_iff /-
@[to_additive]
theorem mem_center_iff {z : M} : z ∈ center M ↔ ∀ g, g * z = z * g :=
Iff.rfl
#align subsemigroup.mem_center_iff Subsemigroup.mem_center_iff
#align add_subsemigroup.mem_center_iff AddSubsemigroup.mem_center_iff
-/
#print Subsemigroup.decidableMemCenter /-
@[to_additive]
instance decidableMemCenter (a) [Decidable <| ∀ b : M, b * a = a * b] : Decidable (a ∈ center M) :=
decidable_of_iff' _ mem_center_iff
#align subsemigroup.decidable_mem_center Subsemigroup.decidableMemCenter
#align add_subsemigroup.decidable_mem_center AddSubsemigroup.decidableMemCenter
-/
/-- The center of a semigroup is commutative. -/
@[to_additive "The center of an additive semigroup is commutative."]
instance : CommSemigroup (center M) :=
{ MulMemClass.toSemigroup (center M) with mul_comm := fun a b => Subtype.ext <| b.Prop _ }
end
section
variable (M) [CommSemigroup M]
#print Subsemigroup.center_eq_top /-
@[simp, to_additive]
theorem center_eq_top : center M = ⊤ :=
SetLike.coe_injective (Set.center_eq_univ M)
#align subsemigroup.center_eq_top Subsemigroup.center_eq_top
#align add_subsemigroup.center_eq_top AddSubsemigroup.center_eq_top
-/
end
end Subsemigroup
-- Guard against import creep
assert_not_exists Finset