-
Notifications
You must be signed in to change notification settings - Fork 0
/
Grupos.lean
513 lines (439 loc) · 15.2 KB
/
Grupos.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
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
-- Teoría de grupos
-- =====================================================================
import tactic
-- Nota técnica: Trabajamos en un espacio de nombres `oculto` porque
-- Lean ya tiene `group`. Ahora nuestra definición de grupo se llamará
-- realmente `oculto.group`.
-- ---------------------------------------------------------------------
-- Ejercicio. Abrir el espacio de nombres
-- ---------------------------------------------------------------------
namespace oculto
-- =====================================================================
-- § Definición de grupo --
-- =====================================================================
-- ---------------------------------------------------------------------
-- Ejercicio. Definir la clase `group` como una extensión de las clases
-- `has_mul`, `has_one` y `has_inv` que verifica las propiedades
-- asociativa : ∀ (a b c : G), (a * b) * c = a * (b * c)
-- neutro por la izquierda : ∀ (a : G), 1 * a = a
-- inverso por la izquierda : ∀ (a : G), a⁻¹ * a = 1
-- ---------------------------------------------------------------------
class group (G : Type) extends has_mul G, has_one G, has_inv G :=
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)
-- La forma de decir "sea G un grupo" ahora es `(G : Type) [group G]`
-- Formalmente, un término de tipo `grupo G` consta de
-- + la definición de una operación interna: * : G → G → G
-- + la definición de un elemento neutro: 1 : G
-- + la definición de una operación inversa: (⁻¹) : G → G
-- + la 3 pruebas de los 3 axiomas.
-- ---------------------------------------------------------------------
-- Ejercicio. Abrir el espacio de nombres `group`
-- ---------------------------------------------------------------------
namespace group
-- ---------------------------------------------------------------------
-- Ejercicio. Definir `G` como una variable sobre grupos.
-- ---------------------------------------------------------------------
variables {G : Type} [group G]
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que en los grupos se cumple la propiedad
-- cancelativa por la izquierda
-- a * b = a * c → b = c
-- ---------------------------------------------------------------------
lemma mul_left_cancel
(a b c : G)
(Habac : a * b = a * c)
: b = c :=
begin
calc b = 1 * b : by rw one_mul
... = (a⁻¹ * a) * b : by rw mul_left_inv
... = a⁻¹ * (a * b) : by rw mul_assoc
... = a⁻¹ * (a * c) : by rw Habac
... = (a⁻¹ * a) * c : by rw mul_assoc
... = 1 * c : by rw mul_left_inv
... = c : by rw one_mul
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- ∀ a x y : G, x = a⁻¹ * y → a * x = y
-- ---------------------------------------------------------------------
lemma mul_eq_of_eq_inv_mul
{a x y : G}
(h : x = a⁻¹ * y)
: a * x = y :=
begin
apply mul_left_cancel a⁻¹,
rw ←mul_assoc,
rw mul_left_inv,
rwa one_mul,
end
-- ---------------------------------------------------------------------
-- Ejercicio. Definir a, b, c, x e y como variables sobre G.
-- ---------------------------------------------------------------------
variables (a b c x y : G)
-- ---------------------------------------------------------------------
-- Ejercicio [KB-R11). Demostrar que 1 es neutro por la derecha; es
-- decir,
-- a * 1 = a
-- ---------------------------------------------------------------------
@[simp] theorem mul_one :
a * 1 = a :=
begin
apply mul_eq_of_eq_inv_mul,
rw mul_left_inv,
end
-- ---------------------------------------------------------------------
-- Ejercicio (KB-R13). Demostrar que
-- a * a⁻¹ = 1
-- ---------------------------------------------------------------------
@[simp] theorem mul_right_inv :
a * a⁻¹ = 1 :=
begin
apply mul_eq_of_eq_inv_mul,
rw mul_one,
end
-- =====================================================================
-- § Simplificador de Lean --
-- =====================================================================
-- Un humano ve "a * a⁻¹" en la teoría de grupos y lo reemplaza
-- instantáneamente con "1".
--
-- Vamos a entrenar una IA simple llamada "simp" para que haga lo
-- mismo.
--
-- El simplificador de Lean `simp` es un "sistema de reescritura de
-- términos". Esto significa que si le enseñas un montón de teoremas de
-- la forma `A = B` o `P ↔ Q` (etiquetándolos con el atributo `@[simp]`)
-- y luego le das un objetivo complicado, como por ejemplo:
-- (a * b) * 1⁻¹⁻¹ * b⁻¹ * (a⁻¹ * a⁻¹⁻¹⁻¹) * a = 1
-- Lean intentará usar la táctica `rw` tanto como pueda, usando los
-- lemas que se les ha enseñado, en un intento de simplificar el
-- objetivo. Si se las arregla para resolverlo por completo, ¡entonces
-- genial! Si no es así, pero piensas que debería haberlo hecho, es
-- posible que tengas que etiquetar más lemas con `@[simp]`.
--
-- `simp` solo debe usarse para cerrar completamente los objetivos.
--
-- Ahora vamos a entrenar al simplificador para resolver el ejemplo
-- anterior (de hecho, estamos entrenándolo para reducir un elemento
-- arbitrario de un grupo libre en una forma normal única, por lo que
-- resolverá cualquier igualdad que sea verdadera para todos los grupos,
-- como en el ejemplo anterior).
--
-- Notal importante: El simplificador de Lean hace una serie de
-- reescrituras, cada una reemplazando algo con algo más simple. ¡Pero
-- el simplificador siempre reescribirá de izquierda a derecha! Si le
-- dice que `A = B` es un lema de simplificación, entonces reemplazará
-- las `A` por las `B`, pero nunca reemplazará las `B` por las `A`.
--
-- Si etiqueta una prueba de `A = B` con `@[simp]` y también etiqueta
-- una prueba de `B = A` con `@[simp]`, entonces el simplificador se
-- atascará en un bucle infinito cuando se encuentra con una "A".
--
-- La igualdad no debe considerarse aquí simétrica.
--
-- Dado que el simplificador funciona de izquierda a derecha, es
-- importante observar que si `A = B` es un lema de simplificación,
-- entonces `B` debería ser más simple que `A`.
--
-- No es una coincidencia que en los teoremas a continuación
-- `@[simp] theorem mul_one (a : G) : a * 1 = a`
-- `@[simp] theorem mul_right_inv (a : G) : a * a⁻¹ = 1`
-- el lado derecho es más simple que el lado izquierdo.
--
-- Sería un desastre etiquetar `a = a * 1` con la etiqueta
-- `@[simp]`. ¿Puedes ver por qué?
--
-- ¡Entrenemos el simplificador de Lean! Enseñémosle los axiomas de un
-- grupo a continuación. Ya hemos visto los axiomas, por lo que tenemos
-- que etiquetarlos con el atributo `@ [simp]`.
-- ---------------------------------------------------------------------
-- Ejercicio. Etiquetar como reglas de simplificación los axiomas
-- one_mul (KB-R1), mul_left_inv (KB-R2) y mul_assoc (KB-R3).
-- ---------------------------------------------------------------------
attribute [simp] one_mul mul_left_inv mul_assoc
-- ---------------------------------------------------------------------
-- Ejercicio (KB-R4). Demostrar que
-- a⁻¹ * (a * b) = b
-- ---------------------------------------------------------------------
-- 1ª demostración
example :
a⁻¹ * (a * b) = b :=
begin
rw ← mul_assoc,
simp,
end
-- 2ª demostración
@[simp] lemma inv_mul_cancel_left :
a⁻¹ * (a * b) = b :=
begin
rw ← mul_assoc,
-- squeeze_simp,
simp only [one_mul,
mul_left_inv],
end
-- ---------------------------------------------------------------------
-- Ejercicio (KB-R14). Demostrar que
-- a * (a⁻¹ * b) = b
-- ---------------------------------------------------------------------
-- 1ª demostración
example :
a * (a⁻¹ * b) = b :=
begin
rw ←mul_assoc,
simp,
end
-- 2ª demostración
@[simp] lemma mul_inv_cancel_left :
a * (a⁻¹ * b) = b :=
begin
rw ←mul_assoc,
-- squeeze_simp,
simp only [one_mul,
mul_right_inv],
end
-- ---------------------------------------------------------------------
-- Ejercicio (KB-R17). Demostrar que
-- (a * b)⁻¹ = b⁻¹ * a⁻¹
-- ---------------------------------------------------------------------
-- 1ª demostración
example :
(a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
apply mul_left_cancel (a * b),
rw mul_right_inv,
simp,
end
-- 2ª demostración
@[simp] lemma inv_mul :
(a * b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
apply mul_left_cancel (a * b),
rw mul_right_inv,
-- squeeze_simp,
simp only [mul_assoc,
mul_inv_cancel_left,
mul_right_inv]
end
-- ---------------------------------------------------------------------
-- Ejercicio (KB-R8). Demostrar que
-- (1 : G)⁻¹ = 1
-- ---------------------------------------------------------------------
-- 1ª demostración
example :
(1 : G)⁻¹ = 1 :=
begin
apply mul_left_cancel (1 : G),
rw mul_right_inv,
simp,
end
-- 1ª demostración
@[simp] lemma one_inv :
(1 : G)⁻¹ = 1 :=
begin
apply mul_left_cancel (1 : G),
rw mul_right_inv,
-- squeeze_simp,
simp only [one_mul],
end
-- ---------------------------------------------------------------------
-- Ejercicio (KB-R12). Demostrar que
-- (a ⁻¹) ⁻¹ = a
-- ---------------------------------------------------------------------
-- 1ª demostración
example :
(a ⁻¹) ⁻¹ = a :=
begin
apply mul_left_cancel a⁻¹,
simp,
end
-- 2ª demostración
@[simp] lemma inv_inv :
(a ⁻¹) ⁻¹ = a :=
begin
apply mul_left_cancel a⁻¹,
-- squeeze_simp,
simp only [mul_right_inv,
mul_left_inv],
end
-- La razón para elegir estos cinco lemas es https://bit.ly/2YyZdhi
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- (a * b) * 1⁻¹⁻¹ * b⁻¹ * (a⁻¹ * a⁻¹⁻¹⁻¹) * a = 1
-- ---------------------------------------------------------------------
-- 1ª demostración
example :
(a * b) * 1⁻¹⁻¹ * b⁻¹ * (a⁻¹ * a⁻¹⁻¹⁻¹) * a = 1 :=
by simp
-- 2ª demostración
example :
(a * b) * 1⁻¹⁻¹ * b⁻¹ * (a⁻¹ * a⁻¹⁻¹⁻¹) * a = 1 :=
-- by squeeze_simp
by simp only [mul_one,
mul_assoc,
mul_right_inv,
inv_inv,
mul_left_inv]
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- a * c = b → a = b * c⁻¹
-- ---------------------------------------------------------------------
lemma eq_mul_inv_of_mul_eq
{a b c : G}
(h : a * c = b)
: a = b * c⁻¹ :=
begin
rw ← h,
simp,
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- b * a = c → a = b⁻¹ * c
-- ---------------------------------------------------------------------
lemma eq_inv_mul_of_mul_eq
{a b c : G}
(h : b * a = c)
: a = b⁻¹ * c :=
begin
rw ← h,
simp,
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- a * b = b ↔ a = 1
-- ---------------------------------------------------------------------
lemma mul_left_eq_self
{a b : G}
: a * b = b ↔ a = 1 :=
begin
split,
{ intro h,
replace h := eq_mul_inv_of_mul_eq h,
simp [h] },
{ intro h,
rw [h, one_mul] }
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- a * b = a ↔ b = 1
-- ---------------------------------------------------------------------
lemma mul_right_eq_self
{a b : G}
: a * b = a ↔ b = 1 :=
begin
split,
{ intro h,
replace h := eq_inv_mul_of_mul_eq h,
simp [h] },
{ rintro rfl,
simp },
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- a * b = 1 → a = b⁻¹
-- ---------------------------------------------------------------------
lemma eq_inv_of_mul_eq_one
{a b : G}
(h : a * b = 1)
: a = b⁻¹ :=
begin
convert eq_mul_inv_of_mul_eq h,
simp,
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- a * b = 1 → a⁻¹ = b
-- ---------------------------------------------------------------------
lemma inv_eq_of_mul_eq_one
{a b : G}
(h : a * b = 1)
: a⁻¹ = b :=
begin
replace h := eq_mul_inv_of_mul_eq h,
simp [h],
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- ∀ x : G, e * x = x → e = 1
-- ---------------------------------------------------------------------
lemma unique_left_id {e : G} (h : ∀ x : G, e * x = x) : e = 1 :=
calc e = e * 1 : by rw mul_one
... = 1 : by rw h 1
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- a * b = 1 → b = a⁻¹
-- ---------------------------------------------------------------------
lemma unique_right_inv
{a b : G}
(h : a * b = 1)
: b = a⁻¹ :=
begin
apply mul_left_cancel a,
simp [h],
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- a * x = a * y ↔ x = y
-- ---------------------------------------------------------------------
lemma mul_left_cancel_iff
(a x y : G)
: a * x = a * y ↔ x = y :=
begin
split,
{ apply mul_left_cancel, },
{ intro hxy,
rwa hxy, },
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- x * a = y * a → x = y
-- ---------------------------------------------------------------------
lemma mul_right_cancel
(a x y : G)
(Habac : x * a = y * a)
: x = y :=
calc x = x * 1 : by rw mul_one
... = x * (a * a⁻¹) : by rw mul_right_inv
... = x * a * a⁻¹ : by rw mul_assoc
... = y * a * a⁻¹ : by rw Habac
... = y * (a * a⁻¹) : by rw mul_assoc
... = y * 1 : by rw mul_right_inv
... = y : by rw mul_one
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- a⁻¹ = b⁻¹ ↔ a = b
-- ---------------------------------------------------------------------
@[simp] theorem inv_inj_iff
{a b : G}
: a⁻¹ = b⁻¹ ↔ a = b :=
begin
split,
{ intro h,
rw [← inv_inv a, h, inv_inv b], },
{ rintro rfl,
refl }
end
-- ---------------------------------------------------------------------
-- Ejercicio. Demostrar que
-- a⁻¹ = b ↔ b⁻¹ = a
-- ---------------------------------------------------------------------
theorem inv_eq
{a b : G}
: a⁻¹ = b ↔ b⁻¹ = a :=
begin
split;
{ rintro rfl,
rw inv_inv }
end
end group
end oculto
-- =====================================================================
-- § Referencias --
-- =====================================================================
-- + Kevin Buzzard. "Formalising mathematics : workshop 2 — groups and
-- subgroups. https://bit.ly/3iaYdqM
-- + Kevin Buzzard. formalising-mathematics: week 2, Part_A_groups.lean
-- https://bit.ly/2WGkyoy
-- + Kevin Buzzard. formalising-mathematics: week 2, Part_A_groups_solutions.lean
-- https://bit.ly/3le1WGc