-
Notifications
You must be signed in to change notification settings - Fork 298
/
basic.lean
730 lines (515 loc) · 30.2 KB
/
basic.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
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
/-
Copyright (c) 2019 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash
-/
import algebra.module.equiv
import data.bracket
import linear_algebra.basic
import tactic.noncomm_ring
/-!
# Lie algebras
This file defines Lie rings and Lie algebras over a commutative ring together with their
modules, morphisms and equivalences, as well as various lemmas to make these definitions usable.
## Main definitions
* `lie_ring`
* `lie_algebra`
* `lie_ring_module`
* `lie_module`
* `lie_hom`
* `lie_equiv`
* `lie_module_hom`
* `lie_module_equiv`
## Notation
Working over a fixed commutative ring `R`, we introduce the notations:
* `L →ₗ⁅R⁆ L'` for a morphism of Lie algebras,
* `L ≃ₗ⁅R⁆ L'` for an equivalence of Lie algebras,
* `M →ₗ⁅R,L⁆ N` for a morphism of Lie algebra modules `M`, `N` over a Lie algebra `L`,
* `M ≃ₗ⁅R,L⁆ N` for an equivalence of Lie algebra modules `M`, `N` over a Lie algebra `L`.
## Implementation notes
Lie algebras are defined as modules with a compatible Lie ring structure and thus, like modules,
are partially unbundled.
## References
* [N. Bourbaki, *Lie Groups and Lie Algebras, Chapters 1--3*](bourbaki1975)
## Tags
lie bracket, jacobi identity, lie ring, lie algebra, lie module
-/
universes u v w w₁ w₂
open function
/-- A Lie ring is an additive group with compatible product, known as the bracket, satisfying the
Jacobi identity. -/
@[protect_proj] class lie_ring (L : Type v) extends add_comm_group L, has_bracket L L :=
(add_lie : ∀ (x y z : L), ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆)
(lie_add : ∀ (x y z : L), ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆)
(lie_self : ∀ (x : L), ⁅x, x⁆ = 0)
(leibniz_lie : ∀ (x y z : L), ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆)
/-- A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi
identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring. -/
@[protect_proj] class lie_algebra (R : Type u) (L : Type v) [comm_ring R] [lie_ring L]
extends module R L :=
(lie_smul : ∀ (t : R) (x y : L), ⁅x, t • y⁆ = t • ⁅x, y⁆)
/-- A Lie ring module is an additive group, together with an additive action of a
Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms.
(For representations of Lie *algebras* see `lie_module`.) -/
@[protect_proj] class lie_ring_module (L : Type v) (M : Type w)
[lie_ring L] [add_comm_group M] extends has_bracket L M :=
(add_lie : ∀ (x y : L) (m : M), ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆)
(lie_add : ∀ (x : L) (m n : M), ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆)
(leibniz_lie : ∀ (x y : L) (m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆)
/-- A Lie module is a module over a commutative ring, together with a linear action of a Lie
algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms. -/
@[protect_proj] class lie_module (R : Type u) (L : Type v) (M : Type w)
[comm_ring R] [lie_ring L] [lie_algebra R L] [add_comm_group M] [module R M]
[lie_ring_module L M] :=
(smul_lie : ∀ (t : R) (x : L) (m : M), ⁅t • x, m⁆ = t • ⁅x, m⁆)
(lie_smul : ∀ (t : R) (x : L) (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆)
section basic_properties
variables {R : Type u} {L : Type v} {M : Type w} {N : Type w₁}
variables [comm_ring R] [lie_ring L] [lie_algebra R L]
variables [add_comm_group M] [module R M] [lie_ring_module L M] [lie_module R L M]
variables [add_comm_group N] [module R N] [lie_ring_module L N] [lie_module R L N]
variables (t : R) (x y z : L) (m n : M)
@[simp] lemma add_lie : ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆ := lie_ring_module.add_lie x y m
@[simp] lemma lie_add : ⁅x, m + n⁆ = ⁅x, m⁆ + ⁅x, n⁆ := lie_ring_module.lie_add x m n
@[simp] lemma smul_lie : ⁅t • x, m⁆ = t • ⁅x, m⁆ := lie_module.smul_lie t x m
@[simp] lemma lie_smul : ⁅x, t • m⁆ = t • ⁅x, m⁆ := lie_module.lie_smul t x m
lemma leibniz_lie : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ := lie_ring_module.leibniz_lie x y m
@[simp] lemma lie_zero : ⁅x, 0⁆ = (0 : M) := (add_monoid_hom.mk' _ (lie_add x)).map_zero
@[simp] lemma zero_lie : ⁅(0 : L), m⁆ = 0 :=
(add_monoid_hom.mk' (λ (x : L), ⁅x, m⁆) (λ x y, add_lie x y m)).map_zero
@[simp] lemma lie_self : ⁅x, x⁆ = 0 := lie_ring.lie_self x
instance lie_ring_self_module : lie_ring_module L L := { ..(infer_instance : lie_ring L) }
@[simp] lemma lie_skew : -⁅y, x⁆ = ⁅x, y⁆ :=
have h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0, { rw ← lie_add, apply lie_self, },
by simpa [neg_eq_iff_add_eq_zero] using h
/-- Every Lie algebra is a module over itself. -/
instance lie_algebra_self_module : lie_module R L L :=
{ smul_lie := λ t x m, by rw [←lie_skew, ←lie_skew x m, lie_algebra.lie_smul, smul_neg],
lie_smul := by apply lie_algebra.lie_smul, }
@[simp] lemma neg_lie : ⁅-x, m⁆ = -⁅x, m⁆ :=
by { rw [←sub_eq_zero, sub_neg_eq_add, ←add_lie], simp, }
@[simp] lemma lie_neg : ⁅x, -m⁆ = -⁅x, m⁆ :=
by { rw [←sub_eq_zero, sub_neg_eq_add, ←lie_add], simp, }
@[simp] lemma sub_lie : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆ :=
by simp [sub_eq_add_neg]
@[simp] lemma lie_sub : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆ :=
by simp [sub_eq_add_neg]
@[simp] lemma nsmul_lie (n : ℕ) : ⁅n • x, m⁆ = n • ⁅x, m⁆ :=
add_monoid_hom.map_nsmul ⟨λ (x : L), ⁅x, m⁆, zero_lie m, λ _ _, add_lie _ _ _⟩ _ _
@[simp] lemma lie_nsmul (n : ℕ) : ⁅x, n • m⁆ = n • ⁅x, m⁆ :=
add_monoid_hom.map_nsmul ⟨λ (m : M), ⁅x, m⁆, lie_zero x, λ _ _, lie_add _ _ _⟩ _ _
@[simp] lemma zsmul_lie (a : ℤ) : ⁅a • x, m⁆ = a • ⁅x, m⁆ :=
add_monoid_hom.map_zsmul ⟨λ (x : L), ⁅x, m⁆, zero_lie m, λ _ _, add_lie _ _ _⟩ _ _
@[simp] lemma lie_zsmul (a : ℤ) : ⁅x, a • m⁆ = a • ⁅x, m⁆ :=
add_monoid_hom.map_zsmul ⟨λ (m : M), ⁅x, m⁆, lie_zero x, λ _ _, lie_add _ _ _⟩ _ _
@[simp] lemma lie_lie : ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ :=
by rw [leibniz_lie, add_sub_cancel]
lemma lie_jacobi : ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0 :=
by { rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie], abel, }
instance lie_ring.int_lie_algebra : lie_algebra ℤ L :=
{ lie_smul := λ n x y, lie_zsmul x y n, }
instance : lie_ring_module L (M →ₗ[R] N) :=
{ bracket := λ x f,
{ to_fun := λ m, ⁅x, f m⁆ - f ⁅x, m⁆,
map_add' := λ m n, by { simp only [lie_add, linear_map.map_add], abel, },
map_smul' := λ t m, by simp only [smul_sub, linear_map.map_smul, lie_smul, ring_hom.id_apply] },
add_lie := λ x y f, by
{ ext n, simp only [add_lie, linear_map.coe_mk, linear_map.add_apply, linear_map.map_add],
abel, },
lie_add := λ x f g, by
{ ext n, simp only [linear_map.coe_mk, lie_add, linear_map.add_apply], abel, },
leibniz_lie := λ x y f, by
{ ext n,
simp only [lie_lie, linear_map.coe_mk, linear_map.map_sub, linear_map.add_apply, lie_sub],
abel, }, }
@[simp] lemma lie_hom.lie_apply (f : M →ₗ[R] N) (x : L) (m : M) :
⁅x, f⁆ m = ⁅x, f m⁆ - f ⁅x, m⁆ :=
rfl
instance : lie_module R L (M →ₗ[R] N) :=
{ smul_lie := λ t x f, by
{ ext n,
simp only [smul_sub, smul_lie, linear_map.smul_apply, lie_hom.lie_apply,
linear_map.map_smul], },
lie_smul := λ t x f, by
{ ext n, simp only [smul_sub, linear_map.smul_apply, lie_hom.lie_apply, lie_smul], }, }
end basic_properties
/-- A morphism of Lie algebras is a linear map respecting the bracket operations. -/
structure lie_hom (R : Type u) (L : Type v) (L' : Type w)
[comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L']
extends L →ₗ[R] L' :=
(map_lie' : ∀ {x y : L}, to_fun ⁅x, y⁆ = ⁅to_fun x, to_fun y⁆)
attribute [nolint doc_blame] lie_hom.to_linear_map
notation L ` →ₗ⁅`:25 R:25 `⁆ `:0 L':0 := lie_hom R L L'
namespace lie_hom
variables {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁}
variables [comm_ring R]
variables [lie_ring L₁] [lie_algebra R L₁]
variables [lie_ring L₂] [lie_algebra R L₂]
variables [lie_ring L₃] [lie_algebra R L₃]
instance : has_coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂) := ⟨lie_hom.to_linear_map⟩
/-- see Note [function coercion] -/
instance : has_coe_to_fun (L₁ →ₗ⁅R⁆ L₂) (λ _, L₁ → L₂) := ⟨λ f, f.to_linear_map.to_fun⟩
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections. -/
def simps.apply (h : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂ := h
initialize_simps_projections lie_hom (to_linear_map_to_fun → apply)
@[simp, norm_cast] lemma coe_to_linear_map (f : L₁ →ₗ⁅R⁆ L₂) : ((f : L₁ →ₗ[R] L₂) : L₁ → L₂) = f :=
rfl
@[simp] lemma to_fun_eq_coe (f : L₁ →ₗ⁅R⁆ L₂) : f.to_fun = ⇑f := rfl
@[simp] lemma map_smul (f : L₁ →ₗ⁅R⁆ L₂) (c : R) (x : L₁) : f (c • x) = c • f x :=
linear_map.map_smul (f : L₁ →ₗ[R] L₂) c x
@[simp] lemma map_add (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f (x + y) = (f x) + (f y) :=
linear_map.map_add (f : L₁ →ₗ[R] L₂) x y
@[simp] lemma map_sub (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f (x - y) = (f x) - (f y) :=
linear_map.map_sub (f : L₁ →ₗ[R] L₂) x y
@[simp] lemma map_neg (f : L₁ →ₗ⁅R⁆ L₂) (x : L₁) : f (-x) = -(f x) :=
linear_map.map_neg (f : L₁ →ₗ[R] L₂) x
@[simp] lemma map_lie (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f ⁅x, y⁆ = ⁅f x, f y⁆ := lie_hom.map_lie' f
@[simp] lemma map_zero (f : L₁ →ₗ⁅R⁆ L₂) : f 0 = 0 := (f : L₁ →ₗ[R] L₂).map_zero
/-- The identity map is a morphism of Lie algebras. -/
def id : L₁ →ₗ⁅R⁆ L₁ :=
{ map_lie' := λ x y, rfl,
.. (linear_map.id : L₁ →ₗ[R] L₁) }
@[simp] lemma coe_id : ((id : L₁ →ₗ⁅R⁆ L₁) : L₁ → L₁) = _root_.id := rfl
lemma id_apply (x : L₁) : (id : L₁ →ₗ⁅R⁆ L₁) x = x := rfl
/-- The constant 0 map is a Lie algebra morphism. -/
instance : has_zero (L₁ →ₗ⁅R⁆ L₂) := ⟨{ map_lie' := by simp, ..(0 : L₁ →ₗ[R] L₂)}⟩
@[norm_cast, simp] lemma coe_zero : ((0 : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = 0 := rfl
lemma zero_apply (x : L₁) : (0 : L₁ →ₗ⁅R⁆ L₂) x = 0 := rfl
/-- The identity map is a Lie algebra morphism. -/
instance : has_one (L₁ →ₗ⁅R⁆ L₁) := ⟨id⟩
@[simp] lemma coe_one : ((1 : (L₁ →ₗ⁅R⁆ L₁)) : L₁ → L₁) = _root_.id := rfl
lemma one_apply (x : L₁) : (1 : (L₁ →ₗ⁅R⁆ L₁)) x = x := rfl
instance : inhabited (L₁ →ₗ⁅R⁆ L₂) := ⟨0⟩
lemma coe_injective : @function.injective (L₁ →ₗ⁅R⁆ L₂) (L₁ → L₂) coe_fn :=
by rintro ⟨⟨f, _⟩⟩ ⟨⟨g, _⟩⟩ ⟨h⟩; congr
@[ext] lemma ext {f g : L₁ →ₗ⁅R⁆ L₂} (h : ∀ x, f x = g x) : f = g :=
coe_injective $ funext h
lemma ext_iff {f g : L₁ →ₗ⁅R⁆ L₂} : f = g ↔ ∀ x, f x = g x :=
⟨by { rintro rfl x, refl }, ext⟩
lemma congr_fun {f g : L₁ →ₗ⁅R⁆ L₂} (h : f = g) (x : L₁) : f x = g x := h ▸ rfl
@[simp] lemma mk_coe (f : L₁ →ₗ⁅R⁆ L₂) (h₁ h₂ h₃) :
(⟨⟨f, h₁, h₂⟩, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) = f :=
by { ext, refl, }
@[simp] lemma coe_mk (f : L₁ → L₂) (h₁ h₂ h₃) :
((⟨⟨f, h₁, h₂⟩, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = f := rfl
/-- The composition of morphisms is a morphism. -/
def comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) : L₁ →ₗ⁅R⁆ L₃ :=
{ map_lie' := λ x y, by { change f (g ⁅x, y⁆) = ⁅f (g x), f (g y)⁆, rw [map_lie, map_lie], },
..linear_map.comp f.to_linear_map g.to_linear_map }
lemma comp_apply (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) (x : L₁) :
f.comp g x = f (g x) := rfl
@[norm_cast, simp]
lemma coe_comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :
(f.comp g : L₁ → L₃) = f ∘ g :=
rfl
@[norm_cast, simp]
lemma coe_linear_map_comp (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂) :
(f.comp g : L₁ →ₗ[R] L₃) = (f : L₂ →ₗ[R] L₃).comp (g : L₁ →ₗ[R] L₂) :=
rfl
@[simp] lemma comp_id (f : L₁ →ₗ⁅R⁆ L₂) : f.comp (id : L₁ →ₗ⁅R⁆ L₁) = f :=
by { ext, refl, }
@[simp] lemma id_comp (f : L₁ →ₗ⁅R⁆ L₂) : (id : L₂ →ₗ⁅R⁆ L₂).comp f = f :=
by { ext, refl, }
/-- The inverse of a bijective morphism is a morphism. -/
def inverse (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁)
(h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : L₂ →ₗ⁅R⁆ L₁ :=
{ map_lie' := λ x y,
calc g ⁅x, y⁆ = g ⁅f (g x), f (g y)⁆ : by { conv_lhs { rw [←h₂ x, ←h₂ y], }, }
... = g (f ⁅g x, g y⁆) : by rw map_lie
... = ⁅g x, g y⁆ : (h₁ _),
..linear_map.inverse f.to_linear_map g h₁ h₂ }
end lie_hom
section module_pull_back
variables {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁)
variables [comm_ring R] [lie_ring L₁] [lie_algebra R L₁] [lie_ring L₂] [lie_algebra R L₂]
variables [add_comm_group M] [lie_ring_module L₂ M]
variables (f : L₁ →ₗ⁅R⁆ L₂)
include f
/-- A Lie ring module may be pulled back along a morphism of Lie algebras.
See note [reducible non-instances]. -/
@[reducible]
def lie_ring_module.comp_lie_hom : lie_ring_module L₁ M :=
{ bracket := λ x m, ⁅f x, m⁆,
lie_add := λ x, lie_add (f x),
add_lie := λ x y m, by simp only [lie_hom.map_add, add_lie],
leibniz_lie := λ x y m, by simp only [lie_lie, sub_add_cancel, lie_hom.map_lie], }
lemma lie_ring_module.comp_lie_hom_apply (x : L₁) (m : M) :
by haveI := lie_ring_module.comp_lie_hom M f; exact
⁅x, m⁆ = ⁅f x, m⁆ :=
rfl
/-- A Lie module may be pulled back along a morphism of Lie algebras.
See note [reducible non-instances]. -/
@[reducible]
def lie_module.comp_lie_hom [module R M] [lie_module R L₂ M] :
@lie_module R L₁ M _ _ _ _ _ (lie_ring_module.comp_lie_hom M f) :=
{ smul_lie := λ t x m, by simp only [smul_lie, lie_hom.map_smul],
lie_smul := λ t x m, by simp only [lie_smul], }
end module_pull_back
/-- An equivalence of Lie algebras is a morphism which is also a linear equivalence. We could
instead define an equivalence to be a morphism which is also a (plain) equivalence. However it is
more convenient to define via linear equivalence to get `.to_linear_equiv` for free. -/
structure lie_equiv (R : Type u) (L : Type v) (L' : Type w)
[comm_ring R] [lie_ring L] [lie_algebra R L] [lie_ring L'] [lie_algebra R L']
extends L →ₗ⁅R⁆ L' :=
(inv_fun : L' → L)
(left_inv : function.left_inverse inv_fun to_lie_hom.to_fun)
(right_inv : function.right_inverse inv_fun to_lie_hom.to_fun)
attribute [nolint doc_blame] lie_equiv.to_lie_hom
notation L ` ≃ₗ⁅`:50 R `⁆ ` L' := lie_equiv R L L'
namespace lie_equiv
variables {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁}
variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃]
variables [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃]
/-- Consider an equivalence of Lie algebras as a linear equivalence. -/
def to_linear_equiv (f : L₁ ≃ₗ⁅R⁆ L₂) : L₁ ≃ₗ[R] L₂ := { ..f.to_lie_hom, ..f }
instance has_coe_to_lie_hom : has_coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ →ₗ⁅R⁆ L₂) := ⟨to_lie_hom⟩
instance has_coe_to_linear_equiv : has_coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ ≃ₗ[R] L₂) := ⟨to_linear_equiv⟩
/-- see Note [function coercion] -/
instance : has_coe_to_fun (L₁ ≃ₗ⁅R⁆ L₂) (λ _, L₁ → L₂) := ⟨λ e, e.to_lie_hom.to_fun⟩
@[simp, norm_cast] lemma coe_to_lie_hom (e : L₁ ≃ₗ⁅R⁆ L₂) : ((e : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = e :=
rfl
@[simp, norm_cast] lemma coe_to_linear_equiv (e : L₁ ≃ₗ⁅R⁆ L₂) :
((e : L₁ ≃ₗ[R] L₂) : L₁ → L₂) = e := rfl
@[simp] lemma to_linear_equiv_mk (f : L₁ →ₗ⁅R⁆ L₂) (g h₁ h₂) :
(mk f g h₁ h₂ : L₁ ≃ₗ[R] L₂) = { inv_fun := g, left_inv := h₁, right_inv := h₂, .. f } := rfl
lemma coe_linear_equiv_injective : injective (coe : (L₁ ≃ₗ⁅R⁆ L₂) → (L₁ ≃ₗ[R] L₂)) :=
begin
intros f₁ f₂ h, cases f₁, cases f₂, dsimp at h, simp only at h,
congr, exacts [lie_hom.coe_injective h.1, h.2]
end
lemma coe_injective : @injective (L₁ ≃ₗ⁅R⁆ L₂) (L₁ → L₂) coe_fn :=
linear_equiv.coe_injective.comp coe_linear_equiv_injective
@[ext] lemma ext {f g : L₁ ≃ₗ⁅R⁆ L₂} (h : ∀ x, f x = g x) : f = g := coe_injective $ funext h
instance : has_one (L₁ ≃ₗ⁅R⁆ L₁) :=
⟨{ map_lie' := λ x y, rfl,
..(1 : L₁ ≃ₗ[R] L₁)}⟩
@[simp] lemma one_apply (x : L₁) : (1 : (L₁ ≃ₗ⁅R⁆ L₁)) x = x := rfl
instance : inhabited (L₁ ≃ₗ⁅R⁆ L₁) := ⟨1⟩
/-- Lie algebra equivalences are reflexive. -/
@[refl]
def refl : L₁ ≃ₗ⁅R⁆ L₁ := 1
@[simp] lemma refl_apply (x : L₁) : (refl : L₁ ≃ₗ⁅R⁆ L₁) x = x := rfl
/-- Lie algebra equivalences are symmetric. -/
@[symm]
def symm (e : L₁ ≃ₗ⁅R⁆ L₂) : L₂ ≃ₗ⁅R⁆ L₁ :=
{ ..lie_hom.inverse e.to_lie_hom e.inv_fun e.left_inv e.right_inv,
..e.to_linear_equiv.symm }
@[simp] lemma symm_symm (e : L₁ ≃ₗ⁅R⁆ L₂) : e.symm.symm = e :=
by { ext, refl }
@[simp] lemma apply_symm_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e (e.symm x) = x :=
e.to_linear_equiv.apply_symm_apply
@[simp] lemma symm_apply_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e.symm (e x) = x :=
e.to_linear_equiv.symm_apply_apply
/-- Lie algebra equivalences are transitive. -/
@[trans]
def trans (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) : L₁ ≃ₗ⁅R⁆ L₃ :=
{ ..lie_hom.comp e₂.to_lie_hom e₁.to_lie_hom,
..linear_equiv.trans e₁.to_linear_equiv e₂.to_linear_equiv }
@[simp] lemma self_trans_symm (e : L₁ ≃ₗ⁅R⁆ L₂) : e.trans e.symm = refl :=
ext e.symm_apply_apply
@[simp] lemma symm_trans_self (e : L₁ ≃ₗ⁅R⁆ L₂) : e.symm.trans e = refl :=
e.symm.self_trans_symm
@[simp] lemma trans_apply (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) (x : L₁) :
(e₁.trans e₂) x = e₂ (e₁ x) := rfl
@[simp] lemma symm_trans (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) :
(e₁.trans e₂).symm = e₂.symm.trans e₁.symm := rfl
protected lemma bijective (e : L₁ ≃ₗ⁅R⁆ L₂) : function.bijective ((e : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) :=
e.to_linear_equiv.bijective
protected lemma injective (e : L₁ ≃ₗ⁅R⁆ L₂) : function.injective ((e : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) :=
e.to_linear_equiv.injective
protected lemma surjective (e : L₁ ≃ₗ⁅R⁆ L₂) : function.surjective ((e : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) :=
e.to_linear_equiv.surjective
/-- A bijective morphism of Lie algebras yields an equivalence of Lie algebras. -/
@[simps] noncomputable def of_bijective (f : L₁ →ₗ⁅R⁆ L₂)
(h₁ : function.injective f) (h₂ : function.surjective f) : L₁ ≃ₗ⁅R⁆ L₂ :=
{ to_fun := f,
map_lie' := f.map_lie,
.. (linear_equiv.of_bijective (f : L₁ →ₗ[R] L₂) h₁ h₂), }
end lie_equiv
section lie_module_morphisms
variables (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂)
variables [comm_ring R] [lie_ring L] [lie_algebra R L]
variables [add_comm_group M] [add_comm_group N] [add_comm_group P]
variables [module R M] [module R N] [module R P]
variables [lie_ring_module L M] [lie_ring_module L N] [lie_ring_module L P]
variables [lie_module R L M] [lie_module R L N] [lie_module R L P]
/-- A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie
algebra. -/
structure lie_module_hom extends M →ₗ[R] N :=
(map_lie' : ∀ {x : L} {m : M}, to_fun ⁅x, m⁆ = ⁅x, to_fun m⁆)
attribute [nolint doc_blame] lie_module_hom.to_linear_map
notation M ` →ₗ⁅`:25 R,L:25 `⁆ `:0 N:0 := lie_module_hom R L M N
namespace lie_module_hom
variables {R L M N P}
instance : has_coe (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N) := ⟨lie_module_hom.to_linear_map⟩
/-- see Note [function coercion] -/
instance : has_coe_to_fun (M →ₗ⁅R,L⁆ N) (λ _, M → N) := ⟨λ f, f.to_linear_map.to_fun⟩
@[simp, norm_cast] lemma coe_to_linear_map (f : M →ₗ⁅R,L⁆ N) : ((f : M →ₗ[R] N) : M → N) = f :=
rfl
@[simp] lemma map_smul (f : M →ₗ⁅R,L⁆ N) (c : R) (x : M) : f (c • x) = c • f x :=
linear_map.map_smul (f : M →ₗ[R] N) c x
@[simp] lemma map_add (f : M →ₗ⁅R,L⁆ N) (x y : M) : f (x + y) = (f x) + (f y) :=
linear_map.map_add (f : M →ₗ[R] N) x y
@[simp] lemma map_sub (f : M →ₗ⁅R,L⁆ N) (x y : M) : f (x - y) = (f x) - (f y) :=
linear_map.map_sub (f : M →ₗ[R] N) x y
@[simp] lemma map_neg (f : M →ₗ⁅R,L⁆ N) (x : M) : f (-x) = -(f x) :=
linear_map.map_neg (f : M →ₗ[R] N) x
@[simp] lemma map_lie (f : M →ₗ⁅R,L⁆ N) (x : L) (m : M) : f ⁅x, m⁆ = ⁅x, f m⁆ :=
lie_module_hom.map_lie' f
lemma map_lie₂ (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (x : L) (m : M) (n : N) :
⁅x, f m n⁆ = f ⁅x, m⁆ n + f m ⁅x, n⁆ :=
by simp only [sub_add_cancel, map_lie, lie_hom.lie_apply]
@[simp] lemma map_zero (f : M →ₗ⁅R,L⁆ N) : f 0 = 0 :=
linear_map.map_zero (f : M →ₗ[R] N)
/-- The identity map is a morphism of Lie modules. -/
def id : M →ₗ⁅R,L⁆ M :=
{ map_lie' := λ x m, rfl,
.. (linear_map.id : M →ₗ[R] M) }
@[simp] lemma coe_id : ((id : M →ₗ⁅R,L⁆ M) : M → M) = _root_.id := rfl
lemma id_apply (x : M) : (id : M →ₗ⁅R,L⁆ M) x = x := rfl
/-- The constant 0 map is a Lie module morphism. -/
instance : has_zero (M →ₗ⁅R,L⁆ N) := ⟨{ map_lie' := by simp, ..(0 : M →ₗ[R] N) }⟩
@[norm_cast, simp] lemma coe_zero : ((0 : M →ₗ⁅R,L⁆ N) : M → N) = 0 := rfl
lemma zero_apply (m : M) : (0 : M →ₗ⁅R,L⁆ N) m = 0 := rfl
/-- The identity map is a Lie module morphism. -/
instance : has_one (M →ₗ⁅R,L⁆ M) := ⟨id⟩
instance : inhabited (M →ₗ⁅R,L⁆ N) := ⟨0⟩
lemma coe_injective : @function.injective (M →ₗ⁅R,L⁆ N) (M → N) coe_fn :=
by { rintros ⟨⟨f, _⟩⟩ ⟨⟨g, _⟩⟩ ⟨h⟩, congr, }
@[ext] lemma ext {f g : M →ₗ⁅R,L⁆ N} (h : ∀ m, f m = g m) : f = g :=
coe_injective $ funext h
lemma ext_iff {f g : M →ₗ⁅R,L⁆ N} : f = g ↔ ∀ m, f m = g m :=
⟨by { rintro rfl m, refl, }, ext⟩
lemma congr_fun {f g : M →ₗ⁅R,L⁆ N} (h : f = g) (x : M) : f x = g x := h ▸ rfl
@[simp] lemma mk_coe (f : M →ₗ⁅R,L⁆ N) (h) :
(⟨f, h⟩ : M →ₗ⁅R,L⁆ N) = f :=
by { ext, refl, }
@[simp] lemma coe_mk (f : M →ₗ[R] N) (h) :
((⟨f, h⟩ : M →ₗ⁅R,L⁆ N) : M → N) = f :=
by { ext, refl, }
@[norm_cast, simp] lemma coe_linear_mk (f : M →ₗ[R] N) (h) :
((⟨f, h⟩ : M →ₗ⁅R,L⁆ N) : M →ₗ[R] N) = f :=
by { ext, refl, }
/-- The composition of Lie module morphisms is a morphism. -/
def comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) : M →ₗ⁅R,L⁆ P :=
{ map_lie' := λ x m, by { change f (g ⁅x, m⁆) = ⁅x, f (g m)⁆, rw [map_lie, map_lie], },
..linear_map.comp f.to_linear_map g.to_linear_map }
lemma comp_apply (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) (m : M) :
f.comp g m = f (g m) := rfl
@[norm_cast, simp] lemma coe_comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :
(f.comp g : M → P) = f ∘ g :=
rfl
@[norm_cast, simp] lemma coe_linear_map_comp (f : N →ₗ⁅R,L⁆ P) (g : M →ₗ⁅R,L⁆ N) :
(f.comp g : M →ₗ[R] P) = (f : N →ₗ[R] P).comp (g : M →ₗ[R] N) :=
rfl
/-- The inverse of a bijective morphism of Lie modules is a morphism of Lie modules. -/
def inverse (f : M →ₗ⁅R,L⁆ N) (g : N → M)
(h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) : N →ₗ⁅R,L⁆ M :=
{ map_lie' := λ x n,
calc g ⁅x, n⁆ = g ⁅x, f (g n)⁆ : by rw h₂
... = g (f ⁅x, g n⁆) : by rw map_lie
... = ⁅x, g n⁆ : (h₁ _),
..linear_map.inverse f.to_linear_map g h₁ h₂ }
instance : has_add (M →ₗ⁅R,L⁆ N) :=
{ add := λ f g, { map_lie' := by simp, ..((f : M →ₗ[R] N) + (g : M →ₗ[R] N)) }, }
instance : has_sub (M →ₗ⁅R,L⁆ N) :=
{ sub := λ f g, { map_lie' := by simp, ..((f : M →ₗ[R] N) - (g : M →ₗ[R] N)) }, }
instance : has_neg (M →ₗ⁅R,L⁆ N) :=
{ neg := λ f, { map_lie' := by simp, ..(-(f : (M →ₗ[R] N))) }, }
@[norm_cast, simp] lemma coe_add (f g : M →ₗ⁅R,L⁆ N) : ⇑(f + g) = f + g := rfl
lemma add_apply (f g : M →ₗ⁅R,L⁆ N) (m : M) : (f + g) m = f m + g m := rfl
@[norm_cast, simp] lemma coe_sub (f g : M →ₗ⁅R,L⁆ N) : ⇑(f - g) = f - g := rfl
lemma sub_apply (f g : M →ₗ⁅R,L⁆ N) (m : M) : (f - g) m = f m - g m := rfl
@[norm_cast, simp] lemma coe_neg (f : M →ₗ⁅R,L⁆ N) : ⇑(-f) = -f := rfl
lemma neg_apply (f : M →ₗ⁅R,L⁆ N) (m : M) : (-f) m = -(f m) := rfl
instance has_nsmul : has_scalar ℕ (M →ₗ⁅R,L⁆ N) :=
{ smul := λ n f, { map_lie' := λ x m, by simp, ..(n • (f : M →ₗ[R] N)) } }
@[norm_cast, simp] lemma coe_nsmul (n : ℕ) (f : M →ₗ⁅R,L⁆ N) : ⇑(n • f) = n • f := rfl
lemma nsmul_apply (n : ℕ) (f : M →ₗ⁅R,L⁆ N) (m : M) : (n • f) m = n • f m := rfl
instance has_zsmul : has_scalar ℤ (M →ₗ⁅R,L⁆ N) :=
{ smul := λ z f, { map_lie' := λ x m, by simp, ..(z • (f : M →ₗ[R] N)) } }
@[norm_cast, simp] lemma coe_zsmul (z : ℤ) (f : M →ₗ⁅R,L⁆ N) : ⇑(z • f) = z • f := rfl
lemma zsmul_apply (z : ℤ) (f : M →ₗ⁅R,L⁆ N) (m : M) : (z • f) m = z • f m := rfl
instance : add_comm_group (M →ₗ⁅R,L⁆ N) :=
coe_injective.add_comm_group _
coe_zero coe_add coe_neg coe_sub (λ _ _, coe_nsmul _ _) (λ _ _, coe_zsmul _ _)
instance : has_scalar R (M →ₗ⁅R,L⁆ N) :=
{ smul := λ t f, { map_lie' := by simp, ..(t • (f : M →ₗ[R] N)) }, }
@[norm_cast, simp] lemma coe_smul (t : R) (f : M →ₗ⁅R,L⁆ N) : ⇑(t • f) = t • f := rfl
lemma smul_apply (t : R) (f : M →ₗ⁅R,L⁆ N) (m : M) : (t • f) m = t • (f m) := rfl
instance : module R (M →ₗ⁅R,L⁆ N) :=
function.injective.module R ⟨λ f, f.to_linear_map.to_fun, rfl, coe_add⟩ coe_injective coe_smul
end lie_module_hom
/-- An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of
Lie algebra modules. -/
structure lie_module_equiv extends M →ₗ⁅R,L⁆ N :=
(inv_fun : N → M)
(left_inv : function.left_inverse inv_fun to_fun)
(right_inv : function.right_inverse inv_fun to_fun)
attribute [nolint doc_blame] lie_module_equiv.to_lie_module_hom
notation M ` ≃ₗ⁅`:25 R,L:25 `⁆ `:0 N:0 := lie_module_equiv R L M N
namespace lie_module_equiv
variables {R L M N P}
/-- View an equivalence of Lie modules as a linear equivalence. -/
@[ancestor]
def to_linear_equiv (e : M ≃ₗ⁅R,L⁆ N) : M ≃ₗ[R] N := { ..e }
/-- View an equivalence of Lie modules as a type level equivalence. -/
@[ancestor]
def to_equiv (e : M ≃ₗ⁅R,L⁆ N) : M ≃ N := { ..e }
instance has_coe_to_equiv : has_coe (M ≃ₗ⁅R,L⁆ N) (M ≃ N) := ⟨to_equiv⟩
instance has_coe_to_lie_module_hom : has_coe (M ≃ₗ⁅R,L⁆ N) (M →ₗ⁅R,L⁆ N) := ⟨to_lie_module_hom⟩
instance has_coe_to_linear_equiv : has_coe (M ≃ₗ⁅R,L⁆ N) (M ≃ₗ[R] N) := ⟨to_linear_equiv⟩
/-- see Note [function coercion] -/
instance : has_coe_to_fun (M ≃ₗ⁅R,L⁆ N) (λ _, M → N) := ⟨λ e, e.to_lie_module_hom.to_fun⟩
lemma injective (e : M ≃ₗ⁅R,L⁆ N) : function.injective e := e.to_equiv.injective
@[simp] lemma coe_mk (f : M →ₗ⁅R,L⁆ N) (inv_fun h₁ h₂) :
((⟨f, inv_fun, h₁, h₂⟩ : M ≃ₗ⁅R,L⁆ N) : M → N) = f := rfl
@[simp, norm_cast] lemma coe_to_lie_module_hom (e : M ≃ₗ⁅R,L⁆ N) :
((e : M →ₗ⁅R,L⁆ N) : M → N) = e := rfl
@[simp, norm_cast] lemma coe_to_linear_equiv (e : M ≃ₗ⁅R,L⁆ N) : ((e : M ≃ₗ[R] N) : M → N) = e :=
rfl
lemma to_equiv_injective : function.injective (to_equiv : (M ≃ₗ⁅R,L⁆ N) → M ≃ N) :=
λ e₁ e₂ h, begin
rcases e₁ with ⟨⟨⟩⟩, rcases e₂ with ⟨⟨⟩⟩,
have inj := equiv.mk.inj h,
dsimp at inj,
apply lie_module_equiv.mk.inj_eq.mpr,
split,
{ congr,
ext,
rw inj.1 },
{ exact inj.2 },
end
@[ext] lemma ext (e₁ e₂ : M ≃ₗ⁅R,L⁆ N) (h : ∀ m, e₁ m = e₂ m) : e₁ = e₂ :=
to_equiv_injective (equiv.ext h)
instance : has_one (M ≃ₗ⁅R,L⁆ M) := ⟨{ map_lie' := λ x m, rfl, ..(1 : M ≃ₗ[R] M) }⟩
@[simp] lemma one_apply (m : M) : (1 : (M ≃ₗ⁅R,L⁆ M)) m = m := rfl
instance : inhabited (M ≃ₗ⁅R,L⁆ M) := ⟨1⟩
/-- Lie module equivalences are reflexive. -/
@[refl] def refl : M ≃ₗ⁅R,L⁆ M := 1
@[simp] lemma refl_apply (m : M) : (refl : M ≃ₗ⁅R,L⁆ M) m = m := rfl
/-- Lie module equivalences are syemmtric. -/
@[symm] def symm (e : M ≃ₗ⁅R,L⁆ N) : N ≃ₗ⁅R,L⁆ M :=
{ ..lie_module_hom.inverse e.to_lie_module_hom e.inv_fun e.left_inv e.right_inv,
..(e : M ≃ₗ[R] N).symm }
@[simp] lemma apply_symm_apply (e : M ≃ₗ⁅R,L⁆ N) : ∀ x, e (e.symm x) = x :=
e.to_linear_equiv.apply_symm_apply
@[simp] lemma symm_apply_apply (e : M ≃ₗ⁅R,L⁆ N) : ∀ x, e.symm (e x) = x :=
e.to_linear_equiv.symm_apply_apply
@[simp] lemma symm_symm (e : M ≃ₗ⁅R,L⁆ N) : e.symm.symm = e :=
by { ext, apply_fun e.symm using e.symm.injective, simp, }
/-- Lie module equivalences are transitive. -/
@[trans] def trans (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) : M ≃ₗ⁅R,L⁆ P :=
{ ..lie_module_hom.comp e₂.to_lie_module_hom e₁.to_lie_module_hom,
..linear_equiv.trans e₁.to_linear_equiv e₂.to_linear_equiv }
@[simp] lemma trans_apply (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) (m : M) :
(e₁.trans e₂) m = e₂ (e₁ m) := rfl
@[simp] lemma symm_trans (e₁ : M ≃ₗ⁅R,L⁆ N) (e₂ : N ≃ₗ⁅R,L⁆ P) :
(e₁.trans e₂).symm = e₂.symm.trans e₁.symm := rfl
@[simp] lemma self_trans_symm (e : M ≃ₗ⁅R,L⁆ N) : e.trans e.symm = refl :=
ext _ _ e.symm_apply_apply
@[simp] lemma symm_trans_self (e : M ≃ₗ⁅R,L⁆ N) : e.symm.trans e = refl :=
ext _ _ e.apply_symm_apply
end lie_module_equiv
end lie_module_morphisms