-
Notifications
You must be signed in to change notification settings - Fork 307
/
Defs.lean
293 lines (227 loc) · 10 KB
/
Defs.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
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
/-
Copyright (c) 2019 Neil Strickland. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Neil Strickland, Yury Kudryashov
-/
import Mathlib.Algebra.Group.Semiconj.Defs
import Mathlib.Data.Nat.Defs
import Mathlib.Init.Algebra.Classes
#align_import algebra.group.commute from "leanprover-community/mathlib"@"05101c3df9d9cfe9430edc205860c79b6d660102"
/-!
# Commuting pairs of elements in monoids
We define the predicate `Commute a b := a * b = b * a` and provide some operations on terms
`(h : Commute a b)`. E.g., if `a`, `b`, and c are elements of a semiring, and that
`hb : Commute a b` and `hc : Commute a c`. Then `hb.pow_left 5` proves `Commute (a ^ 5) b` and
`(hb.pow_right 2).add_right (hb.mul_right hc)` proves `Commute a (b ^ 2 + b * c)`.
Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like
`rw [(hb.pow_left 5).eq]` rather than just `rw [hb.pow_left 5]`.
This file defines only a few operations (`mul_left`, `inv_right`, etc). Other operations
(`pow_right`, field inverse etc) are in the files that define corresponding notions.
## Implementation details
Most of the proofs come from the properties of `SemiconjBy`.
-/
variable {G : Type*}
/-- Two elements commute if `a * b = b * a`. -/
@[to_additive "Two elements additively commute if `a + b = b + a`"]
def Commute {S : Type*} [Mul S] (a b : S) : Prop :=
SemiconjBy a b b
#align commute Commute
#align add_commute AddCommute
/--
Two elements `a` and `b` commute if `a * b = b * a`.
-/
@[to_additive]
theorem commute_iff_eq {S : Type*} [Mul S] (a b : S) : Commute a b ↔ a * b = b * a := Iff.rfl
namespace Commute
section Mul
variable {S : Type*} [Mul S]
/-- Equality behind `Commute a b`; useful for rewriting. -/
@[to_additive "Equality behind `AddCommute a b`; useful for rewriting."]
protected theorem eq {a b : S} (h : Commute a b) : a * b = b * a :=
h
#align commute.eq Commute.eq
#align add_commute.eq AddCommute.eq
/-- Any element commutes with itself. -/
@[to_additive (attr := refl, simp) "Any element commutes with itself."]
protected theorem refl (a : S) : Commute a a :=
Eq.refl (a * a)
#align commute.refl Commute.refl
#align add_commute.refl AddCommute.refl
/-- If `a` commutes with `b`, then `b` commutes with `a`. -/
@[to_additive (attr := symm) "If `a` commutes with `b`, then `b` commutes with `a`."]
protected theorem symm {a b : S} (h : Commute a b) : Commute b a :=
Eq.symm h
#align commute.symm Commute.symm
#align add_commute.symm AddCommute.symm
@[to_additive]
protected theorem semiconjBy {a b : S} (h : Commute a b) : SemiconjBy a b b :=
h
#align commute.semiconj_by Commute.semiconjBy
#align add_commute.semiconj_by AddCommute.addSemiconjBy
@[to_additive]
protected theorem symm_iff {a b : S} : Commute a b ↔ Commute b a :=
⟨Commute.symm, Commute.symm⟩
#align commute.symm_iff Commute.symm_iff
#align add_commute.symm_iff AddCommute.symm_iff
@[to_additive]
instance : IsRefl S Commute :=
⟨Commute.refl⟩
-- This instance is useful for `Finset.noncommProd`
@[to_additive]
instance on_isRefl {f : G → S} : IsRefl G fun a b => Commute (f a) (f b) :=
⟨fun _ => Commute.refl _⟩
#align commute.on_is_refl Commute.on_isRefl
#align add_commute.on_is_refl AddCommute.on_isRefl
end Mul
section Semigroup
variable {S : Type*} [Semigroup S] {a b c : S}
/-- If `a` commutes with both `b` and `c`, then it commutes with their product. -/
@[to_additive (attr := simp)
"If `a` commutes with both `b` and `c`, then it commutes with their sum."]
theorem mul_right (hab : Commute a b) (hac : Commute a c) : Commute a (b * c) :=
SemiconjBy.mul_right hab hac
#align commute.mul_right Commute.mul_rightₓ
#align add_commute.add_right AddCommute.add_rightₓ
-- I think `ₓ` is necessary because of the `mul` vs `HMul` distinction
/-- If both `a` and `b` commute with `c`, then their product commutes with `c`. -/
@[to_additive (attr := simp)
"If both `a` and `b` commute with `c`, then their product commutes with `c`."]
theorem mul_left (hac : Commute a c) (hbc : Commute b c) : Commute (a * b) c :=
SemiconjBy.mul_left hac hbc
#align commute.mul_left Commute.mul_leftₓ
#align add_commute.add_left AddCommute.add_leftₓ
-- I think `ₓ` is necessary because of the `mul` vs `HMul` distinction
@[to_additive]
protected theorem right_comm (h : Commute b c) (a : S) : a * b * c = a * c * b :=
by simp only [mul_assoc, h.eq]
#align commute.right_comm Commute.right_commₓ
#align add_commute.right_comm AddCommute.right_commₓ
-- I think `ₓ` is necessary because of the `mul` vs `HMul` distinction
@[to_additive]
protected theorem left_comm (h : Commute a b) (c) : a * (b * c) = b * (a * c) :=
by simp only [← mul_assoc, h.eq]
#align commute.left_comm Commute.left_commₓ
#align add_commute.left_comm AddCommute.left_commₓ
-- I think `ₓ` is necessary because of the `mul` vs `HMul` distinction
@[to_additive]
protected theorem mul_mul_mul_comm (hbc : Commute b c) (a d : S) :
a * b * (c * d) = a * c * (b * d) := by simp only [hbc.left_comm, mul_assoc]
#align commute.mul_mul_mul_comm Commute.mul_mul_mul_comm
#align add_commute.add_add_add_comm AddCommute.add_add_add_comm
end Semigroup
@[to_additive]
protected theorem all {S : Type*} [CommMagma S] (a b : S) : Commute a b :=
mul_comm a b
#align commute.all Commute.allₓ
#align add_commute.all AddCommute.allₓ
-- not sure why this needs an `ₓ`, maybe instance names not aligned?
section MulOneClass
variable {M : Type*} [MulOneClass M]
@[to_additive (attr := simp)]
theorem one_right (a : M) : Commute a 1 :=
SemiconjBy.one_right a
#align commute.one_right Commute.one_rightₓ
#align add_commute.zero_right AddCommute.zero_rightₓ
-- I think `ₓ` is necessary because `One.toOfNat1` appears in the Lean 4 version
@[to_additive (attr := simp)]
theorem one_left (a : M) : Commute 1 a :=
SemiconjBy.one_left a
#align commute.one_left Commute.one_leftₓ
#align add_commute.zero_left AddCommute.zero_leftₓ
-- I think `ₓ` is necessary because `One.toOfNat1` appears in the Lean 4 version
end MulOneClass
section Monoid
variable {M : Type*} [Monoid M] {a b : M}
@[to_additive (attr := simp)]
theorem pow_right (h : Commute a b) (n : ℕ) : Commute a (b ^ n) :=
SemiconjBy.pow_right h n
#align commute.pow_right Commute.pow_rightₓ
#align add_commute.nsmul_right AddCommute.nsmul_rightₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
@[to_additive (attr := simp)]
theorem pow_left (h : Commute a b) (n : ℕ) : Commute (a ^ n) b :=
(h.symm.pow_right n).symm
#align commute.pow_left Commute.pow_leftₓ
#align add_commute.nsmul_left AddCommute.nsmul_leftₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
-- todo: should nat power be called `nsmul` here?
@[to_additive (attr := simp)]
theorem pow_pow (h : Commute a b) (m n : ℕ) : Commute (a ^ m) (b ^ n) :=
(h.pow_left m).pow_right n
#align commute.pow_pow Commute.pow_powₓ
#align add_commute.nsmul_nsmul AddCommute.nsmul_nsmulₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
-- Porting note: `simpNF` told me to remove the `simp` attribute
@[to_additive]
theorem self_pow (a : M) (n : ℕ) : Commute a (a ^ n) :=
(Commute.refl a).pow_right n
#align commute.self_pow Commute.self_powₓ
#align add_commute.self_nsmul AddCommute.self_nsmulₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
-- Porting note: `simpNF` told me to remove the `simp` attribute
@[to_additive]
theorem pow_self (a : M) (n : ℕ) : Commute (a ^ n) a :=
(Commute.refl a).pow_left n
#align add_commute.nsmul_self AddCommute.nsmul_selfₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
#align commute.pow_self Commute.pow_self
-- Porting note: `simpNF` told me to remove the `simp` attribute
@[to_additive]
theorem pow_pow_self (a : M) (m n : ℕ) : Commute (a ^ m) (a ^ n) :=
(Commute.refl a).pow_pow m n
#align commute.pow_pow_self Commute.pow_pow_selfₓ
#align add_commute.nsmul_nsmul_self AddCommute.nsmul_nsmul_selfₓ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
end Monoid
section DivisionMonoid
variable [DivisionMonoid G] {a b c d: G}
@[to_additive]
protected theorem mul_inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by rw [hab.eq, mul_inv_rev]
#align commute.mul_inv Commute.mul_inv
#align add_commute.add_neg AddCommute.add_neg
@[to_additive]
protected theorem inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by rw [hab.eq, mul_inv_rev]
#align commute.inv Commute.inv
#align add_commute.neg AddCommute.neg
end DivisionMonoid
section Group
variable [Group G] {a b : G}
@[to_additive]
protected theorem mul_inv_cancel (h : Commute a b) : a * b * a⁻¹ = b := by
rw [h.eq, mul_inv_cancel_right]
#align commute.mul_inv_cancel Commute.mul_inv_cancel
#align add_commute.add_neg_cancel AddCommute.add_neg_cancel
@[to_additive]
theorem mul_inv_cancel_assoc (h : Commute a b) : a * (b * a⁻¹) = b := by
rw [← mul_assoc, h.mul_inv_cancel]
#align commute.mul_inv_cancel_assoc Commute.mul_inv_cancel_assoc
#align add_commute.add_neg_cancel_assoc AddCommute.add_neg_cancel_assoc
end Group
end Commute
section Monoid
variable {M : Type*} [Monoid M] {n : ℕ}
@[to_additive succ_nsmul']
lemma pow_succ' (a : M) (n : ℕ) : a ^ (n + 1) = a * a ^ n :=
(pow_succ a n).trans (Commute.self_pow _ _).symm
#align pow_succ pow_succ'
#align succ_nsmul succ_nsmul'
@[to_additive]
lemma mul_pow_sub_one (hn : n ≠ 0) (a : M) : a * a ^ (n - 1) = a ^ n := by
rw [← pow_succ', Nat.sub_add_cancel $ Nat.one_le_iff_ne_zero.2 hn]
@[to_additive]
lemma pow_sub_one_mul (hn : n ≠ 0) (a : M) : a ^ (n - 1) * a = a ^ n := by
rw [← pow_succ, Nat.sub_add_cancel $ Nat.one_le_iff_ne_zero.2 hn]
end Monoid
section CommGroup
variable [CommGroup G] (a b : G)
@[to_additive (attr := simp)]
theorem mul_inv_cancel_comm : a * b * a⁻¹ = b :=
(Commute.all a b).mul_inv_cancel
#align mul_inv_cancel_comm mul_inv_cancel_comm
#align add_neg_cancel_comm add_neg_cancel_comm
@[to_additive (attr := simp)]
theorem mul_inv_cancel_comm_assoc : a * (b * a⁻¹) = b :=
(Commute.all a b).mul_inv_cancel_assoc
#align mul_inv_cancel_comm_assoc mul_inv_cancel_comm_assoc
#align add_neg_cancel_comm_assoc add_neg_cancel_comm_assoc
end CommGroup