1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115
116. 116
117. 117
118. 118
119. 119
120. 120
121. 121
122. 122
123. 123
124. 124
125. 125
126. 126
127. 127
128. 128
129. 129
130. 130
131. 131
132. 132
133. 133
134. 134
135. 135
136. 136
137. 137
138. 138
139. 139
140. 140
141. 141
142. 142
143. 143
144. 144
145. 145
146. 146
147. 147
148. 148
149. 149
150. 150
151. 151
152. 152
153. 153
154. 154
155. 155
156. 156
157. 157
158. 158
159. 159
160. 160
161. 161
162. 162
163. 163
164. 164
165. 165
166. 166
167. 167
168. 168
169. 169
170. 170
171. 171
172. 172
173. 173
174. 174
175. 175
176. 176
177. 177
178. 178
179. 179
180. 180
181. 181
182. 182
183. 183
184. 184
185. 185
186. 186
187. 187
188. 188
189. 189
190. 190
191. 191
192. 192
193. 193
194. 194
195. 195
196. 196
197. 197
198. 198
199. 199
200. 200
201. 201
202. 202
203. 203
204. 204
205. 205
206. 206
207. 207
208. 208
209. 209
210. 210
211. 211
212. 212
213. 213
214. 214
215. 215
216. 216
217. 217
218. 218
219. 219
220. 220
221. 221
222. 222
223. 223
224. 224
225. 225
226. 226
227. 227
228. 228
229. 229
230. 230
231. 231
232. 232
233. 233
234. 234
235. 235
236. 236
237. 237
238. 238
239. 239
240. 240
241. 241
242. 242
243. 243
244. 244
245. 245
246. 246
247. 247
248. 248
249. 249
250. 250
251. 251
252. 252
253. 253
254. 254
255. 255
256. 256
257. 257
258. 258
259. 259
260. 260
261. 261
262. 262
263. 263
264. 264
265. 265
266. 266
267. 267
268. 268
269. 269
270. 270
271. 271
272. 272
273. 273
274. 274
275. 275
276. 276
277. 277
278. 278
279. 279
280. 280
281. 281
282. 282
283. 283
284. 284
285. 285
286. 286
287. 287
288. 288
289. 289
290. 290
291. 291
292. 292
293. 293
294. 294
295. 295
296. 296
297. 297
298. 298
299. 299
300. 300
301. 301
302. 302
303. 303
304. 304
305. 305
306. 306
307. 307
308. 308
309. 309
310. 310
311. 311
312. 312
313. 313
314. 314
315. 315
316. 316
317. 317
318. 318
319. 319
320. 320
321. 321
322. 322
323. 323
324. 324
325. 325
326. 326
327. 327
328. 328
329. 329
330. 330
331. 331
332. 332
333. 333
334. 334
335. 335
336. 336
337. 337
338. 338
339. 339
340. 340
341. 341
342. 342
343. 343
344. 344
345. 345
346. 346
347. 347
348. 348
349. 349
350. 350
351. 351
352. 352
353. 353
354. 354
355. 355
356. 356
357. 357
358. 358
359. 359
360. 360
361. 361
362. 362
363. 363
364. 364
365. 365
366. 366
367. 367
368. 368
369. 369
370. 370
371. 371
372. 372
373. 373
374. 374
375. 375
376. 376
377. 377
378. 378
379. 379
380. 380
381. 381
382. 382
383. 383
384. 384
385. 385
386. 386
387. 387
388. 388
389. 389
390. 390
391. 391
392. 392
393. 393
394. 394
395. 395
396. 396
397. 397
398. 398
399. 399
400. 400
401. 401
402. 402
403. 403
404. 404
405. 405
406. 406
407. 407
408. 408
409. 409
410. 410
411. 411
412. 412
413. 413
414. 414
415. 415
416. 416
417. 417
418. 418
419. 419
420. 420
421. 421
422. 422
423. 423
424. 424
425. 425
426. 426
427. 427
428. 428
429. 429
430. 430
431. 431
432. 432
433. 433
434. 434
435. 435
436. 436
437. 437
438. 438
439. 439
440. 440
441. 441
442. 442
443. 443
444. 444
445. 445
446. 446
447. 447
448. 448
449. 449
450. 450
451. 451
452. 452
453. 453
454. 454
455. 455
456. 456
457. 457
458. 458
459. 459
460. 460
461. 461
462. 462
463. 463
464. 464
465. 465
466. 466
467. 467
468. 468
469. 469
470. 470
471. 471
472. 472
473. 473
474. 474
475. 475
476. 476
477. 477
478. 478
479. 479
480. 480
481. 481
482. 482
483. 483
484. 484
485. 485
486. 486
487. 487
488. 488
489. 489
490. 490
491. 491
492. 492
493. 493
494. 494
495. 495
496. 496
497. 497
498. 498
499. 499
500. 500
501. 501
502. 502
503. 503
504. 504
505. 505
506. 506
507. 507
508. 508
509. 509
510. 510
511. 511
512. 512
513. 513
514. 514
515. 515
516. 516
517. 517
518. 518
519. 519
520. 520
521. 521
522. 522
523. 523
524. 524
525. 525
526. 526
527. 527
528. 528
529. 529
530. 530
531. 531
532. 532
533. 533
534. 534
535. 535
536. 536
537. 537
538. 538
539. 539
540. 540
541. 541
542. 542
543. 543
544. 544
545. 545
546. 546
547. 547
548. 548
549. 549
550. 550
551. 551
552. 552
553. 553
554. 554
555. 555
556. 556
557. 557
558. 558
559. 559
560. 560
561. 561
562. 562
563. 563
564. 564
565. 565
566. 566
567. 567
568. 568
569. 569
570. 570
571. 571
572. 572
573. 573
574. 574
575. 575
576. 576
577. 577
578. 578
579. 579
580. 580
581. 581
582. 582
583. 583
584. 584
585. 585
586. 586
587. 587
588. 588
589. 589
590. 590
591. 591
592. 592
593. 593
594. 594
595. 595
596. 596
597. 597
598. 598
599. 599
600. 600
601. 601
602. 602
603. 603
604. 604
605. 605
606. 606
607. 607
608. 608
609. 609
610. 610
611. 611
612. 612
613. 613
614. 614
615. 615
616. 616
617. 617
618. 618
619. 619
620. 620
621. 621
622. 622
623. 623
624. 624
625. 625
626. 626
627. 627
628. 628
629. 629
630. 630
631. 631
632. 632
633. 633
634. 634
635. 635
636. 636
637. 637
638. 638
639. 639
640. 640
641. 641
642. 642
643. 643
644. 644
645. 645
646. 646
647. 647
648. 648
649. 649
650. 650
651. 651
652. 652
653. 653
654. 654
655. 655
656. 656
657. 657
658. 658
659. 659
660. 660
661. 661
662. 662
663. 663
664. 664
665. 665
666. 666
667. 667
668. 668
669. 669
670. 670
671. 671
672. 672
673. 673
674. 674
675. 675
676. 676
677. 677
678. 678
679. 679
680. 680
681. 681
682. 682
683. 683
684. 684
685. 685
686. 686
687. 687
688. 688
689. 689
690. 690
691. 691
692. 692
693. 693
694. 694
695. 695
696. 696
697. 697
698. 698
699. 699
700. 700
701. 701
702. 702
703. 703
704. 704
705. 705
706. 706
707. 707
708. 708
709. 709
710. 710
711. 711
712. 712
713. 713
714. 714
715. 715
716. 716
717. 717
718. 718
719. 719
720. 720
721. 721
722. 722
723. 723
724. 724
725. 725
726. 726
727. 727
728. 728
729. 729
730. 730
731. 731
732. 732
733. 733
734. 734
735. 735
736. 736
737. 737
738. 738
739. 739
740. 740
741. 741
742. 742
743. 743
744. 744
745. 745
746. 746
747. 747
748. 748
749. 749
750. 750
751. 751
752. 752
753. 753
754. 754
755. 755
756. 756
757. 757
758. 758
759. 759
760. 760
761. 761
762. 762
763. 763
764. 764
765. 765
766. 766
767. 767
768. 768
769. 769
770. 770
771. 771
772. 772
773. 773
774. 774
775. 775
776. 776
777. 777
778. 778
779. 779
780. 780
781. 781
782. 782
783. 783
784. 784
785. 785
786. 786
787. 787
788. 788
789. 789
790. 790
791. 791
792. 792
793. 793
794. 794
795. 795
796. 796
797. 797
798. 798
799. 799
800. 800
801. 801
802. 802
803. 803
804. 804
805. 805
806. 806
807. 807
808. 808
809. 809
810. 810
811. 811
812. 812
813. 813
814. 814
815. 815
816. 816
817. 817
818. 818
819. 819
820. 820
821. 821
822. 822
823. 823
824. 824
825. 825
826. 826
827. 827
828. 828
829. 829
830. 830
831. 831
832. 832
833. 833
834. 834
835. 835
836. 836
837. 837
838. 838
839. 839
840. 840
841. 841
842. 842
843. 843
844. 844
845. 845
846. 846
847. 847
848. 848
849. 849
850. 850
851. 851
852. 852
853. 853
854. 854
855. 855
856. 856
857. 857
858. 858
859. 859
860. 860
861. 861
862. 862
863. 863
864. 864
865. 865
866. 866
867. 867
868. 868
869. 869
870. 870
871. 871
872. 872
873. 873
874. 874
875. 875
876. 876
877. 877
878. 878
879. 879
880. 880
881. 881
882. 882
883. 883
884. 884
885. 885
886. 886
887. 887
888. 888
889. 889
890. 890
891. 891
892. 892
893. 893
894. 894
895. 895
896. 896
897. 897
898. 898
899. 899
900. 900
901. 901
902. 902
903. 903
904. 904
905. 905
906. 906
907. 907
908. 908
909. 909
910. 910
911. 911
912. 912
913. 913
914. 914
915. 915
916. 916
917. 917
918. 918
919. 919
920. 920
921. 921
922. 922
923. 923
924. 924
925. 925
926. 926
927. 927
928. 928
929. 929
930. 930
931. 931
932. 932
933. 933
934. 934
935. 935
936. 936
937. 937
938. 938
939. 939
940. 940
941. 941
942. 942
943. 943
944. 944
945. 945
946. 946
947. 947
948. 948
949. 949
950. 950
951. 951
952. 952
953. 953
954. 954
955. 955
956. 956
957. 957
958. 958
959. 959
960. 960
961. 961
962. 962
963. 963
964. 964
965. 965
966. 966
967. 967
968. 968
969. 969
970. 970
971. 971
972. 972
973. 973
974. 974
975. 975
976. 976
977. 977
978. 978
979. 979
980. 980
981. 981
982. 982
983. 983
984. 984
985. 985
986. 986
987. 987
988. 988
989. 989
990. 990
991. 991
992. 992
993. 993
994. 994
995. 995
996. 996
997. 997
998. 998
999. 999
1000. 1000
1001. 1001
1002. 1002
1003. 1003
1004. 1004
1005. 1005
1006. 1006
1007. 1007
1008. 1008
1009. 1009
1010. 1010
1011. 1011
1012. 1012
1013. 1013
1014. 1014
1015. 1015
1016. 1016
1017. 1017
1018. 1018
1019. 1019
1020. 1020
1021. 1021
1022. 1022
1023. 1023
1024. 1024
1025. 1025
1026. 1026
1027. 1027
1028. 1028
1029. 1029
1030. 1030
1031. 1031
1032. 1032
1033. 1033
1034. 1034
1035. 1035
1036. 1036
1037. 1037
1038. 1038
1039. 1039
1040. 1040
1041. 1041
1042. 1042
1043. 1043
1044. 1044
1045. 1045
1046. 1046
1047. 1047
1048. 1048
1049. 1049
1050. 1050
1051. 1051
1052. 1052
1053. 1053
1054. 1054
1055. 1055
1056. 1056
1057. 1057
1058. 1058
1059. 1059
1060. 1060
1061. 1061
1062. 1062
1063. 1063
1064. 1064
1065. 1065
1066. 1066
1067. 1067
1068. 1068
1069. 1069
1070. 1070
1071. 1071
1072. 1072
1073. 1073
1074. 1074
1075. 1075
1076. 1076
1077. 1077
1078. 1078
1079. 1079
1080. 1080
1081. 1081
1082. 1082
1083. 1083
1084. 1084
1085. 1085
1086. 1086
1087. 1087
1088. 1088
1089. 1089
1090. 1090
1091. 1091
1092. 1092
1093. 1093
1094. 1094
1095. 1095
1096. 1096
1097. 1097
1098. 1098
1099. 1099
1100. 1100
1101. 1101
1102. 1102
1103. 1103
1104. 1104
1105. 1105
1106. 1106
1107. 1107
1108. 1108
1109. 1109
1110. 1110
1111. 1111
1112. 1112
1113. 1113
1114. 1114
1115. 1115
1116. 1116
1117. 1117
1118. 1118
1119. 1119
1120. 1120
1121. 1121
1122. 1122
1123. 1123
1124. 1124
1125. 1125
1126. 1126
1127. 1127
1128. 1128
1129. 1129
1130. 1130
1131. 1131
1132. 1132
1133. 1133
1134. 1134
1135. 1135
1136. 1136
1137. 1137
1138. 1138
1139. 1139
1140. 1140
1141. 1141
1142. 1142
1143. 1143
1144. 1144
1145. 1145
1146. 1146
1147. 1147

<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>8. Groups and Rings &mdash; Mathematics in Lean 0.1 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=e59714d7" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
      <script src="_static/jquery.js?v=5d32c60e"></script>
      <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
      <script src="_static/documentation_options.js?v=2709fde1"></script>
      <script src="_static/doctools.js?v=9bcbadda"></script>
      <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
      <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="9. Linear algebra" href="C09_Linear_Algebra.html" />
    <link rel="prev" title="7. Hierarchies" href="C07_Hierarchies.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Structures.html">6. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Hierarchies.html">7. Hierarchies</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">8. Groups and Rings</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#monoids-and-groups">8.1. Monoids and Groups</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#monoids-and-their-morphisms">8.1.1. Monoids and their morphisms</a></li>
<li class="toctree-l3"><a class="reference internal" href="#groups-and-their-morphisms">8.1.2. Groups and their morphisms</a></li>
<li class="toctree-l3"><a class="reference internal" href="#subgroups">8.1.3. Subgroups</a></li>
<li class="toctree-l3"><a class="reference internal" href="#concrete-groups">8.1.4. Concrete groups</a></li>
<li class="toctree-l3"><a class="reference internal" href="#group-actions">8.1.5. Group actions</a></li>
<li class="toctree-l3"><a class="reference internal" href="#quotient-groups">8.1.6. Quotient groups</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#rings">8.2. Rings</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#rings-their-units-morphisms-and-subrings">8.2.1. Rings, their units, morphisms and subrings</a></li>
<li class="toctree-l3"><a class="reference internal" href="#ideals-and-quotients">8.2.2. Ideals and quotients</a></li>
<li class="toctree-l3"><a class="reference internal" href="#algebras-and-polynomials">8.2.3. Algebras and polynomials</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C09_Linear_Algebra.html">9. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Topology.html">10. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Differential_Calculus.html">11. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Integration_and_Measure_Theory.html">12. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">8. </span>Groups and Rings</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C08_Groups_and_Rings.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="groups-and-rings">
<span id="groups-and-ring"></span><h1><span class="section-number">8. </span>Groups and Rings<a class="headerlink" href="#groups-and-rings" title="Link to this heading">&#61633;</a></h1>
<p>We saw in <a class="reference internal" href="C02_Basics.html#proving-identities-in-algebraic-structures"><span class="std std-numref">Section 2.2</span></a> how to reason about
operations in groups and rings. Later, in <a class="reference internal" href="C06_Structures.html#section-algebraic-structures"><span class="std std-numref">Section 6.2</span></a>, we saw how
to define abstract algebraic structures, such as group structures, as well as concrete instances
such as the ring structure on the Gaussian integers. <a class="reference internal" href="C07_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 7</span></a> explained how
hierarchies of abstract structures are handled in Mathlib.</p>
<p>In this chapter we work with groups and rings in more detail. We won&#8217;t be able to
cover every aspect of the treatment of these topics in Mathlib, especially since Mathlib is constantly growing.
But we will provide entry points to the library and show how the essential concepts are used.
There is some overlap with the discussion of
<a class="reference internal" href="C07_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 7</span></a>, but here we will focus on how to use Mathlib instead of the design
decisions behind the way the topics are treated.
So making sense of some of the examples may require reviewing the background from
<a class="reference internal" href="C07_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 7</span></a>.</p>
<section id="monoids-and-groups">
<span id="groups"></span><h2><span class="section-number">8.1. </span>Monoids and Groups<a class="headerlink" href="#monoids-and-groups" title="Link to this heading">&#61633;</a></h2>
<section id="monoids-and-their-morphisms">
<span id="index-1"></span><span id="index-0"></span><h3><span class="section-number">8.1.1. </span>Monoids and their morphisms<a class="headerlink" href="#monoids-and-their-morphisms" title="Link to this heading">&#61633;</a></h3>
<p>Courses in abstract algebra often start with groups and
then progress to rings, fields, and vector spaces. This involves some contortions when discussing
multiplication on rings since the multiplication operation does not come from a group structure
but many of the proofs carry over verbatim from group theory to this new setting.
The most common fix, when doing mathematics with pen and paper,
is to leave those proofs as exercises. A less efficient but safer and
more formalization-friendly way of proceeding is to use monoids. A <em>monoid</em> structure on a type <cite>M</cite>
is an internal composition law that is associative and has a neutral element.
Monoids are used primarily to accommodate both groups and the multiplicative structure of
rings. But there are also a number of natural examples; for instance, the set of natural numbers
equipped with addition forms a monoid.</p>
<p>From a practical point of view, you can mostly ignore monoids when using Mathlib. But you need
to know they exist when you are looking for a lemma by browsing Mathlib files. Otherwise, you
might end up looking for a statement in the group theory files when it is actually in the found
with monoids because it does not require elements to be invertible.</p>
<p>The type of monoid structures on a type <code class="docutils literal notranslate"><span class="pre">M</span></code> is written <code class="docutils literal notranslate"><span class="pre">Monoid</span> <span class="pre">M</span></code>.
The function <code class="docutils literal notranslate"><span class="pre">Monoid</span></code> is a type class so it will almost always appear as an instance implicit
argument (in other words, in square brackets).
By default, <code class="docutils literal notranslate"><span class="pre">Monoid</span></code> uses multiplicative notation for the operation; for additive notation
use <code class="docutils literal notranslate"><span class="pre">AddMonoid</span></code> instead.
The commutative versions of these structures add the prefix <code class="docutils literal notranslate"><span class="pre">Comm</span></code> before <code class="docutils literal notranslate"><span class="pre">Monoid</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">mul_one</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommMonoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">add_comm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>
</pre></div>
</div>
<p>Note that although <code class="docutils literal notranslate"><span class="pre">AddMonoid</span></code> is found in the library,
it is generally confusing to use additive notation with a non-commutative operation.</p>
<p>The type of morphisms between monoids <code class="docutils literal notranslate"><span class="pre">M</span></code> and <code class="docutils literal notranslate"><span class="pre">N</span></code> is called <code class="docutils literal notranslate"><span class="pre">MonoidHom</span> <span class="pre">M</span> <span class="pre">N</span></code> and written
<code class="docutils literal notranslate"><span class="pre">M</span> <span class="pre">&#8594;*</span> <span class="pre">N</span></code>. Lean will automatically see such a morphism as a function from <code class="docutils literal notranslate"><span class="pre">M</span></code> to <code class="docutils literal notranslate"><span class="pre">N</span></code> when
we apply it to elements of <code class="docutils literal notranslate"><span class="pre">M</span></code>. The additive version is called <code class="docutils literal notranslate"><span class="pre">AddMonoidHom</span></code> and written
<code class="docutils literal notranslate"><span class="pre">M</span> <span class="pre">&#8594;+</span> <span class="pre">N</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">N</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">N</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">N</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8594;+</span><span class="w"> </span><span class="n">N</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_zero</span>
</pre></div>
</div>
<p>These morphisms are bundled maps, i.e. they package together a map and some of its properties.
Remember that <a class="reference internal" href="C07_Hierarchies.html#section-hierarchies-morphisms"><span class="std std-numref">Section 7.2</span></a> explains bundled maps;
here we simply note the slightly unfortunate consequence that we cannot use ordinary function
composition to compose maps. Instead, we need to use <code class="docutils literal notranslate"><span class="pre">MonoidHom.comp</span></code> and <code class="docutils literal notranslate"><span class="pre">AddMonoidHom.comp</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">N</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">AddMonoid</span><span class="w"> </span><span class="n">P</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8594;+</span><span class="w"> </span><span class="n">N</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8594;+</span><span class="w"> </span><span class="n">P</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8594;+</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">g.comp</span><span class="w"> </span><span class="n">f</span>
</pre></div>
</div>
</section>
<section id="groups-and-their-morphisms">
<h3><span class="section-number">8.1.2. </span>Groups and their morphisms<a class="headerlink" href="#groups-and-their-morphisms" title="Link to this heading">&#61633;</a></h3>
<p>We will have much more to say about groups, which are monoids with the extra
property that every element has an inverse.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">mul_inv_cancel</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p id="index-2">Similar to the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic that we saw earlier, there is a <code class="docutils literal notranslate"><span class="pre">group</span></code> tactic that proves
any identity that holds in any group. (Equivalently, it proves the identities that hold in
free groups.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="o">)</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">group</span>
</pre></div>
</div>
<p id="index-3">There is also a tactic for identities in commutative additive groups called <code class="docutils literal notranslate"><span class="pre">abel</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddCommGroup</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">y</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">abel</span>
</pre></div>
</div>
<p>Interestingly, a group
morphism is nothing more than a monoid morphism between groups. So we can copy and paste one of our
earlier examples, replacing <code class="docutils literal notranslate"><span class="pre">Monoid</span></code> with <code class="docutils literal notranslate"><span class="pre">Group</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>
</pre></div>
</div>
<p>Of course we do get some new properties, such as this one:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_inv</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>You may be worried that constructing group morphisms will require us to do unnecessary work since
the definition of monoid morphism enforces that neutral elements are sent to neutral elements
while this is automatic in the case of group morphisms. In practice the extra work is not hard,
but, to avoid it, there is a function building a group morphism from a function
between groups that is compatible with the composition laws.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MonoidHom.mk&#39;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>There is also a type <code class="docutils literal notranslate"><span class="pre">MulEquiv</span></code> of group (or monoid) isomorphisms denoted by <code class="docutils literal notranslate"><span class="pre">&#8771;*</span></code> (and
<code class="docutils literal notranslate"><span class="pre">AddEquiv</span></code> denoted by <code class="docutils literal notranslate"><span class="pre">&#8771;+</span></code> in additive notation).
The inverse of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">G</span> <span class="pre">&#8771;*</span> <span class="pre">H</span></code> is <code class="docutils literal notranslate"><span class="pre">MulEquiv.symm</span> <span class="pre">f</span> <span class="pre">:</span> <span class="pre">H</span> <span class="pre">&#8771;*</span> <span class="pre">G</span></code>,
composition of <code class="docutils literal notranslate"><span class="pre">f</span></code> and <code class="docutils literal notranslate"><span class="pre">g</span></code> is <code class="docutils literal notranslate"><span class="pre">MulEquiv.trans</span> <span class="pre">f</span> <span class="pre">g</span></code>, and
the identity isomorphism of <code class="docutils literal notranslate"><span class="pre">G</span></code> is <code class="docutils literal notranslate"><span class="pre">M&#768;ulEquiv.refl</span> <span class="pre">G</span></code>.
Using anonymous projector notation, the first two can be written <code class="docutils literal notranslate"><span class="pre">f.symm</span></code> and
<code class="docutils literal notranslate"><span class="pre">f.trans</span> <span class="pre">g</span></code> respectively.
Elements of this type are automatically coerced to morphisms and functions when necessary.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">f.trans</span><span class="w"> </span><span class="n">f.symm</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">MulEquiv.refl</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.self_trans_symm</span>
</pre></div>
</div>
<p>One can use <code class="docutils literal notranslate"><span class="pre">MulEquiv.ofBijective</span></code> to build an isomorphism from a bijective morphism.
Doing so makes the inverse function noncomputable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Function.Bijective</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MulEquiv.ofBijective</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
</section>
<section id="subgroups">
<h3><span class="section-number">8.1.3. </span>Subgroups<a class="headerlink" href="#subgroups" title="Link to this heading">&#61633;</a></h3>
<p>Just as group morphisms are bundled, a subgroup of <code class="docutils literal notranslate"><span class="pre">G</span></code> is also a bundled structure consisting of
a set in <code class="docutils literal notranslate"><span class="pre">G</span></code> with the relevant closure properties.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hx</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">H.mul_mem</span><span class="w"> </span><span class="n">hx</span><span class="w"> </span><span class="n">hy</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hx</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">H.inv_mem</span><span class="w"> </span><span class="n">hx</span>
</pre></div>
</div>
<p>In the example above, it is important to understand that <code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code> is the type of subgroups
of <code class="docutils literal notranslate"><span class="pre">G</span></code>, rather than a predicate <code class="docutils literal notranslate"><span class="pre">IsSubgroup</span> <span class="pre">H</span></code> where <code class="docutils literal notranslate"><span class="pre">H</span></code> is an element of <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">G</span></code>.
<code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code> is endowed with a coercion to <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">G</span></code> and a membership predicate on <code class="docutils literal notranslate"><span class="pre">G</span></code>.
See <a class="reference internal" href="C07_Hierarchies.html#section-hierarchies-subobjects"><span class="std std-numref">Section 7.3</span></a> for an explanation of how and why this is done.</p>
<p>Of course, two subgroups are the same if and only if they have the same elements. This fact
is registered for use with the <code class="docutils literal notranslate"><span class="pre">ext</span></code> tactic, which can be used to prove two subgroups are
equal in the same way it is used to prove that two sets are equal.</p>
<p>To state and prove, for example, that <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> is an additive subgroup of <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>,
what we really want is to construct a term of type <code class="docutils literal notranslate"><span class="pre">AddSubgroup</span> <span class="pre">&#8474;</span></code> whose projection to
<code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">&#8474;</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code>, or, more precisely, the image of <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code> in <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">AddSubgroup</span><span class="w"> </span><span class="n">&#8474;</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">carrier</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Set.range</span><span class="w"> </span><span class="o">((</span><span class="bp">&#8593;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8474;</span><span class="o">)</span>
<span class="w">  </span><span class="n">add_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rintro</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">rfl</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">rfl</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">m</span>
<span class="w">    </span><span class="n">simp</span>
<span class="w">  </span><span class="n">zero_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="mi">0</span>
<span class="w">    </span><span class="n">simp</span>
<span class="w">  </span><span class="n">neg_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rintro</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">rfl</span><span class="o">&#10217;</span>
<span class="w">    </span><span class="n">use</span><span class="w"> </span><span class="bp">-</span><span class="n">n</span>
<span class="w">    </span><span class="n">simp</span>
</pre></div>
</div>
<p>Using type classes, Mathlib knows that a subgroup of a group inherits a group structure.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>This example is subtle. The object <code class="docutils literal notranslate"><span class="pre">H</span></code> is not a type, but Lean automatically coerces it to
a type by interpreting it as a subtype of <code class="docutils literal notranslate"><span class="pre">G</span></code>.
So the above example can be restated more explicitly as:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>An important benefit of having a type <code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code> instead of a predicate
<code class="docutils literal notranslate"><span class="pre">IsSubgroup</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">G</span> <span class="pre">&#8594;</span> <span class="pre">Prop</span></code> is that one can easily endow <code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code> with additional structure.
Importantly, it has the structure of a complete lattice structure with respect to
inclusion. For instance, instead of having a lemma stating that an intersection of
two subgroups of <code class="docutils literal notranslate"><span class="pre">G</span></code> is again a subgroup, we
have used the lattice operation <code class="docutils literal notranslate"><span class="pre">&#8851;</span></code> to construct the intersection. We can then apply arbitrary
lemmas about lattices to the construction.</p>
<p>Let us check that the set underlying the infimum of two subgroups is indeed, by definition,
their intersection.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">((</span><span class="n">H</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8745;</span><span class="w"> </span><span class="o">(</span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>
</pre></div>
</div>
<p>It may look strange to have a different notation for what amounts to the intersection of the
underlying sets, but the correspondence does not carry over to the supremum operation and set
union, since a union of subgroups is not, in general, a subgroup.
Instead one needs to use the subgroup generated by the union, which is done
using <code class="docutils literal notranslate"><span class="pre">Subgroup.closure</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">((</span><span class="n">H</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Subgroup.closure</span><span class="w"> </span><span class="o">((</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8746;</span><span class="w"> </span><span class="o">(</span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">G</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Subgroup.sup_eq_closure</span><span class="o">]</span>
</pre></div>
</div>
<p>Another subtlety is that <code class="docutils literal notranslate"><span class="pre">G</span></code> itself does not have type <code class="docutils literal notranslate"><span class="pre">Subgroup</span> <span class="pre">G</span></code>,
so we need a way to talk about <code class="docutils literal notranslate"><span class="pre">G</span></code> seen as a subgroup of <code class="docutils literal notranslate"><span class="pre">G</span></code>.
This is also provided by the lattice structure: the full subgroup is the top element of
this lattice.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">trivial</span>
</pre></div>
</div>
<p>Similarly the bottom element of this lattice is the subgroup whose only element is the
neutral element.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Subgroup.mem_bot</span>
</pre></div>
</div>
<p>As an exercise in manipulating groups and subgroups, you can define the conjugate of a subgroup
by an element of the ambient group.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">conjugate</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">carrier</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">h</span><span class="o">,</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="o">}</span>
<span class="w">  </span><span class="n">one_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">dsimp</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">inv_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">dsimp</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">mul_mem&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">dsimp</span>
<span class="w">    </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Tying the previous two topics together, one can push forward and pull back subgroups using
group morphisms. The naming convention in Mathlib is to call those operations <code class="docutils literal notranslate"><span class="pre">map</span></code>
and <code class="docutils literal notranslate"><span class="pre">comap</span></code>.
These are not the common mathematical terms, but they have the advantage of being
shorter than &#8220;pushforward&#8221; and &#8220;direct image.&#8221;</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">G&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Subgroup.map</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">G&#39;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Subgroup.comap</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">H&#39;</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Subgroup.mem_map</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Subgroup.mem_comap</span>
</pre></div>
</div>
<p>In particular, the preimage of the bottom subgroup under a morphism <code class="docutils literal notranslate"><span class="pre">f</span></code> is a subgroup called
the <em>kernel</em> of <code class="docutils literal notranslate"><span class="pre">f</span></code>, and the range of <code class="docutils literal notranslate"><span class="pre">f</span></code> is also a subgroup.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">MonoidHom.ker</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.mem_ker</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">h</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">MonoidHom.range</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.mem_range</span>
</pre></div>
</div>
<p>As exercises in manipulating group morphisms and subgroups, let us prove some elementary properties.
They are already proved in Mathlib, so do not use <code class="docutils literal notranslate"><span class="pre">exact?</span></code> too quickly if you want to benefit
from these exercises.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">exercises</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">H</span><span class="o">]</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Subgroup</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">S</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hST</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">T</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">S</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hST</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">T</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">map</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">map</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">T</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">K</span><span class="o">]</span>

<span class="c1">-- Remember you can use the `ext` tactic to prove an equality of subgroups.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">comap</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;.comp</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">comap</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="c1">-- Pushing a subgroup along one homomorphism and then another is equal to</span>
<span class="c1">-- pushing it forward along the composite of the homomorphisms.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">map</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;.comp</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">map</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">(</span><span class="n">S.map</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">end</span><span class="w"> </span><span class="n">exercises</span>
</pre></div>
</div>
<p>Let us finish this introduction to subgroups in Mathlib with two very classical results.
Lagrange theorem states the cardinality of a subgroup of a finite group divides the cardinality of
the group. Sylow&#8217;s first theorem is a famous partial converse to Lagrange&#8217;s theorem.</p>
<p>While this corner of Mathlib is partly set up to allow computation, we can tell
Lean to use nonconstructive logic anyway using the following <code class="docutils literal notranslate"><span class="pre">open</span> <span class="pre">scoped</span></code> command.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">scoped</span><span class="w"> </span><span class="n">Classical</span>


<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">G&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G&#39;</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">G&#39;.index</span><span class="o">,</span><span class="w"> </span><span class="n">mul_comm</span><span class="w"> </span><span class="n">G&#39;.index</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#9656;</span><span class="w"> </span><span class="n">G&#39;.index_mul_card.symm</span><span class="o">&#10217;</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Subgroup</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Finite</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Fact</span><span class="w"> </span><span class="n">p.Prime</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">hdvd</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Sylow.exists_subgroup_card_pow_prime</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="n">hdvd</span>
</pre></div>
</div>
<p>The next two exercises derive a corollary of Lagrange&#8217;s lemma. (This is also already in Mathlib,
so do not use <code class="docutils literal notranslate"><span class="pre">exact?</span></code> too quickly.)</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span><span class="w"> </span><span class="n">eq_bot_iff_card</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">H</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">suffices</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">H</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">simpa</span><span class="w"> </span><span class="o">[</span><span class="n">eq_bot_iff_forall</span><span class="o">,</span><span class="w"> </span><span class="n">Nat.card_eq_one_iff_exists</span><span class="o">]</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="k">#check</span><span class="w"> </span><span class="n">card_dvd_of_le</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">inf_bot_of_coprime</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.card</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="bp">.</span><span class="n">Coprime</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="concrete-groups">
<h3><span class="section-number">8.1.4. </span>Concrete groups<a class="headerlink" href="#concrete-groups" title="Link to this heading">&#61633;</a></h3>
<p>One can also manipulate concrete groups in Mathlib, although this is typically more complicated
than working with the abstract theory.
For instance, given any type <code class="docutils literal notranslate"><span class="pre">X</span></code>, the group of permutations of <code class="docutils literal notranslate"><span class="pre">X</span></code> is <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">X</span></code>.
In particular the symmetric group <span class="math notranslate nohighlight">\(\mathfrak{S}_n\)</span> is <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">(Fin</span> <span class="pre">n)</span></code>.
One can state abstract results about this group, for instance saying that <code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">X</span></code> is
generated by cycles if <code class="docutils literal notranslate"><span class="pre">X</span></code> is finite.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Equiv</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Finite</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup.closure</span><span class="w"> </span><span class="o">{</span><span class="n">&#963;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Perm</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">Perm.IsCycle</span><span class="w"> </span><span class="n">&#963;</span><span class="o">}</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8868;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Perm.closure_isCycle</span>
</pre></div>
</div>
<p>One can be fully concrete and compute actual products of cycles. Below we use the <code class="docutils literal notranslate"><span class="pre">#simp</span></code> command,
which calls the <code class="docutils literal notranslate"><span class="pre">simp</span></code> tactic on a given expression. The notation <code class="docutils literal notranslate"><span class="pre">c[]</span></code> is used to define a
cyclic permutation. In the example, the result is a permutation of <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code>. One could use a type
ascription such as <code class="docutils literal notranslate"><span class="pre">(1</span> <span class="pre">:</span> <span class="pre">Fin</span> <span class="pre">5)</span></code> on the first number appearing to make it a computation in
<code class="docutils literal notranslate"><span class="pre">Perm</span> <span class="pre">(Fin</span> <span class="pre">5)</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">#</span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">mul_assoc</span><span class="o">]</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">]</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span>
</pre></div>
</div>
<p>Another way to work with concrete groups is to use free groups and group presentations.
The free group on a type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> is <code class="docutils literal notranslate"><span class="pre">FreeGroup</span> <span class="pre">&#945;</span></code> and the inclusion map is
<code class="docutils literal notranslate"><span class="pre">FreeGroup.of</span> <span class="pre">:</span> <span class="pre">&#945;</span> <span class="pre">&#8594;</span> <span class="pre">FreeGroup</span> <span class="pre">&#945;</span></code>. For instance let us define a type <code class="docutils literal notranslate"><span class="pre">S</span></code> with three elements denoted
by <code class="docutils literal notranslate"><span class="pre">a</span></code>, <code class="docutils literal notranslate"><span class="pre">b</span></code> and <code class="docutils literal notranslate"><span class="pre">c</span></code>, and the element <code class="docutils literal notranslate"><span class="pre">ab&#8315;&#185;</span></code> of the corresponding free group.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">FreeGroup</span>

<span class="kd">inductive</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="n">c</span>

<span class="kn">open</span><span class="w"> </span><span class="n">S</span>

<span class="kd">def</span><span class="w"> </span><span class="n">myElement</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">FreeGroup</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="bp">.</span><span class="n">of</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="bp">.</span><span class="n">of</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">&#8315;&#185;</span>
</pre></div>
</div>
<p>Note that we gave the expected type of the definition so that Lean knows that <code class="docutils literal notranslate"><span class="pre">.of</span></code> means
<code class="docutils literal notranslate"><span class="pre">FreeGroup.of</span></code>.</p>
<p>The universal property of free groups is embodied as the equivalence <code class="docutils literal notranslate"><span class="pre">FreeGroup.lift</span></code>.
For example, let us define the group morphism from <code class="docutils literal notranslate"><span class="pre">FreeGroup</span> <span class="pre">S</span></code> to <code class="docutils literal notranslate"><span class="pre">Perm</span> <span class="pre">(Fin</span> <span class="pre">5)</span></code> that
sends <code class="docutils literal notranslate"><span class="pre">a</span></code> to <code class="docutils literal notranslate"><span class="pre">c[1,</span> <span class="pre">2,</span> <span class="pre">3]</span></code>, <code class="docutils literal notranslate"><span class="pre">b</span></code> to <code class="docutils literal notranslate"><span class="pre">c[2,</span> <span class="pre">3,</span> <span class="pre">1]</span></code>, and <code class="docutils literal notranslate"><span class="pre">c</span></code> to <code class="docutils literal notranslate"><span class="pre">c[2,</span> <span class="pre">3]</span></code>,</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">myMorphism</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">FreeGroup</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">Perm</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">5</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">FreeGroup.lift</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="bp">.</span><span class="n">a</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">]</span>
<span class="w">                     </span><span class="bp">|</span><span class="w"> </span><span class="bp">.</span><span class="n">b</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span>
<span class="w">                     </span><span class="bp">|</span><span class="w"> </span><span class="bp">.</span><span class="n">c</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">]</span>
</pre></div>
</div>
<p>As a last concrete example, let us see how to define a group generated by a single element whose
cube is one (so that group will be isomorphic to <span class="math notranslate nohighlight">\(\mathbb{Z}/3\)</span>) and build a morphism
from that group to <code class="docutils literal notranslate"><span class="pre">Perm</span> <span class="pre">(Fin</span> <span class="pre">5)</span></code>.</p>
<p>As a type with exactly one element, we will use <code class="docutils literal notranslate"><span class="pre">Unit</span></code> whose
only element is denoted by <code class="docutils literal notranslate"><span class="pre">()</span></code>. The function <code class="docutils literal notranslate"><span class="pre">PresentedGroup</span></code> takes a set of relations,
i.e. a set of elements of some free group, and returns a group that is this free group quotiented
by a normal subgroup generated by relations. (We will see how to handle more general quotients
in <a class="reference internal" href="#quotient-groups"><span class="std std-numref">Section 8.1.6</span></a>.) Since we somehow hide this behind a definition, we use <code class="docutils literal notranslate"><span class="pre">deriving</span> <span class="pre">Group</span></code> to force creation
of a group instance on <code class="docutils literal notranslate"><span class="pre">myGroup</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">myGroup</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">PresentedGroup</span><span class="w"> </span><span class="o">{</span><span class="bp">.</span><span class="n">of</span><span class="w"> </span><span class="o">()</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">3</span><span class="o">}</span><span class="w"> </span><span class="n">deriving</span><span class="w"> </span><span class="n">Group</span>
</pre></div>
</div>
<p>The universal property of presented groups ensures that morphisms out of this group can be built
from functions that send the relations to the neutral element of the target group.
So we need such a function and a proof that the condition holds. Then we can feed this proof
to <code class="docutils literal notranslate"><span class="pre">PresentedGroup.toGroup</span></code> to get the desired group morphism.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">myMap</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Unit</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Perm</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">5</span><span class="o">)</span>
<span class="bp">|</span><span class="w"> </span><span class="o">()</span><span class="w"> </span><span class="bp">=&gt;</span><span class="w"> </span><span class="n">c</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">3</span><span class="o">]</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">compat_myMap</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">({</span><span class="bp">.</span><span class="n">of</span><span class="w"> </span><span class="o">()</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">3</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="o">(</span><span class="n">FreeGroup</span><span class="w"> </span><span class="n">Unit</span><span class="o">)),</span><span class="w"> </span><span class="n">FreeGroup.lift</span><span class="w"> </span><span class="n">myMap</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rintro</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">rfl</span>
<span class="w">  </span><span class="n">simp</span>
<span class="w">  </span><span class="n">decide</span>

<span class="kd">def</span><span class="w"> </span><span class="n">myNewMorphism</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">myGroup</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">Perm</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">5</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">PresentedGroup.toGroup</span><span class="w"> </span><span class="n">compat_myMap</span>

<span class="kd">end</span><span class="w"> </span><span class="n">FreeGroup</span>
</pre></div>
</div>
</section>
<section id="group-actions">
<h3><span class="section-number">8.1.5. </span>Group actions<a class="headerlink" href="#group-actions" title="Link to this heading">&#61633;</a></h3>
<p>One important way that group theory interacts with the rest of mathematics is through
the use of group actions.
An action of a group <code class="docutils literal notranslate"><span class="pre">G</span></code> on some type <code class="docutils literal notranslate"><span class="pre">X</span></code> is nothing more than a morphism from <code class="docutils literal notranslate"><span class="pre">G</span></code> to
<code class="docutils literal notranslate"><span class="pre">Equiv.Perm</span> <span class="pre">X</span></code>. So in a sense group actions are already covered by the previous discussion.
But we don&#8217;t want to carry this morphism around; instead, we want it to be inferred automatically
by Lean as much as possible. So we have a type class for this, which is <code class="docutils literal notranslate"><span class="pre">MulAction</span> <span class="pre">G</span> <span class="pre">X</span></code>.
The downside of this setup is that having multiple actions of the same group on the same type
requires some contortions, such as defining type synonyms, each of which carries different
type class instances.</p>
<p>This allows us in particular to use <code class="docutils literal notranslate"><span class="pre">g</span> <span class="pre">&#8226;</span> <span class="pre">x</span></code> to denote the action of a group element <code class="docutils literal notranslate"><span class="pre">g</span></code> on
a point <code class="docutils literal notranslate"><span class="pre">x</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kn">section</span><span class="w"> </span><span class="n">GroupActions</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="n">g&#39;</span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="o">(</span><span class="n">g&#39;</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">g&#39;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">mul_smul</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">g&#39;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">symm</span>
</pre></div>
</div>
<p>There is also a version for additive group called <code class="docutils literal notranslate"><span class="pre">AddAction</span></code>, where the action is denoted by
<code class="docutils literal notranslate"><span class="pre">+&#7525;</span></code>. This is used for instance in the definition of affine spaces.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">AddGroup</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">AddAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="n">g&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">g</span><span class="w"> </span><span class="bp">+&#7525;</span><span class="w"> </span><span class="o">(</span><span class="n">g&#39;</span><span class="w"> </span><span class="bp">+&#7525;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">g&#39;</span><span class="o">)</span><span class="w"> </span><span class="bp">+&#7525;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">add_vadd</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">g&#39;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">symm</span>
</pre></div>
</div>
<p>The underlying group morphism is called <code class="docutils literal notranslate"><span class="pre">MulAction.toPermHom</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">MulAction</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">Equiv.Perm</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">toPermHom</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span>
</pre></div>
</div>
<p>As an illustration let us see how to define the Cayley isomorphism embedding of any group <code class="docutils literal notranslate"><span class="pre">G</span></code> into
a permutation group, namely <code class="docutils literal notranslate"><span class="pre">Perm</span> <span class="pre">G</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">CayleyIsoMorphism</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="o">(</span><span class="n">toPermHom</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="bp">.</span><span class="n">range</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Equiv.Perm.subgroupOfMulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">G</span>
</pre></div>
</div>
<p>Note that nothing before the above definition required having a group rather than a monoid (or any
type endowed with a multiplication operation really).</p>
<p>The group condition really enters the picture when we will want to partition <code class="docutils literal notranslate"><span class="pre">X</span></code> into orbits.
The corresponding equivalence relation on <code class="docutils literal notranslate"><span class="pre">X</span></code> is called <code class="docutils literal notranslate"><span class="pre">MulAction.orbitRel</span></code>.
It is not declared as a global instance.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Setoid</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">orbitRel</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span>
</pre></div>
</div>
<p>Using this we can state that <code class="docutils literal notranslate"><span class="pre">X</span></code> is partitioned into orbits under the action of <code class="docutils literal notranslate"><span class="pre">G</span></code>.
More precisely, we get a bijection between <code class="docutils literal notranslate"><span class="pre">X</span></code> and the dependent product
<code class="docutils literal notranslate"><span class="pre">(&#969;</span> <span class="pre">:</span> <span class="pre">orbitRel.Quotient</span> <span class="pre">G</span> <span class="pre">X)</span> <span class="pre">&#215;</span> <span class="pre">(orbit</span> <span class="pre">G</span> <span class="pre">(Quotient.out'</span> <span class="pre">&#969;))</span></code>
where <code class="docutils literal notranslate"><span class="pre">Quotient.out'</span> <span class="pre">&#969;</span></code> simply chooses an element that projects to <code class="docutils literal notranslate"><span class="pre">&#969;</span></code>.
Recall that elements of this dependent product are pairs <code class="docutils literal notranslate"><span class="pre">&#10216;&#969;,</span> <span class="pre">x&#10217;</span></code> where the type
<code class="docutils literal notranslate"><span class="pre">orbit</span> <span class="pre">G</span> <span class="pre">(Quotient.out'</span> <span class="pre">&#969;)</span></code> of <code class="docutils literal notranslate"><span class="pre">x</span></code> depends on <code class="docutils literal notranslate"><span class="pre">&#969;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">X</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="o">(</span><span class="n">&#969;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">orbitRel.Quotient</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">)</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="o">(</span><span class="n">orbit</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">(</span><span class="n">Quotient.out&#39;</span><span class="w"> </span><span class="n">&#969;</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MulAction.selfEquivSigmaOrbits</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span>
</pre></div>
</div>
<p>In particular, when X is finite, this can be combined with <code class="docutils literal notranslate"><span class="pre">Fintype.card_congr</span></code> and
<code class="docutils literal notranslate"><span class="pre">Fintype.card_sigma</span></code> to deduce that the cardinality of <code class="docutils literal notranslate"><span class="pre">X</span></code> is the sum of the cardinalities
of the orbits.
Furthermore, the orbits are in bijection with the quotient of <code class="docutils literal notranslate"><span class="pre">G</span></code> under the action of the
stabilizers by left translation.
This action of a subgroup by left-translation is used to define quotients of a group by a
subgroup with notation <cite>/</cite> so we can use the following concise statement.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">orbit</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">stabilizer</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">MulAction.orbitEquivQuotientStabilizer</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>An important special case of combining the above two results is when <code class="docutils literal notranslate"><span class="pre">X</span></code> is a group <code class="docutils literal notranslate"><span class="pre">G</span></code>
equipped with the action of a subgroup <code class="docutils literal notranslate"><span class="pre">H</span></code> by translation.
In this case all stabilizers are trivial so every orbit is in bijection with <code class="docutils literal notranslate"><span class="pre">H</span></code> and we get:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">groupEquivQuotientProdSubgroup</span>
</pre></div>
</div>
<p>This is the conceptual variant of the version of Lagrange theorem that we saw above.
Note this version makes no finiteness assumption.</p>
<p>As an exercise for this section, let us build the action of a group on its subgroup by
conjugation, using our definition of <code class="docutils literal notranslate"><span class="pre">conjugate</span></code> from a previous exercise.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">conjugate_one</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">conjugate</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">instance</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MulAction</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="o">(</span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">smul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">conjugate</span>
<span class="w">  </span><span class="n">one_smul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">mul_smul</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="gr">sorry</span>

<span class="kd">end</span><span class="w"> </span><span class="n">GroupActions</span>
</pre></div>
</div>
</section>
<section id="quotient-groups">
<span id="id1"></span><h3><span class="section-number">8.1.6. </span>Quotient groups<a class="headerlink" href="#quotient-groups" title="Link to this heading">&#61633;</a></h3>
<p>In the above discussion of subgroups acting on groups, we saw the quotient <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#10744;</span> <span class="pre">H</span></code> appear.
In general this is only a type. It can be endowed with a group structure such that the quotient
map is a group morphism if and only if <code class="docutils literal notranslate"><span class="pre">H</span></code> is a normal subgroup (and this group structure is
then unique).</p>
<p>The normality assumption is a type class <code class="docutils literal notranslate"><span class="pre">Subgroup.Normal</span></code> so that type class inference can use it
to derive the group structure on the quotient.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kn">section</span><span class="w"> </span><span class="n">QuotientGroup</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">H.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">H.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">QuotientGroup.mk&#39;</span><span class="w"> </span><span class="n">H</span>
</pre></div>
</div>
<p>The universal property of quotient groups is accessed through <code class="docutils literal notranslate"><span class="pre">QuotientGroup.lift</span></code>:
a group morphism <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> descends to <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#10744;</span> <span class="pre">N</span></code> as soon as its kernel contains <code class="docutils literal notranslate"><span class="pre">N</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">N.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span>
<span class="w">    </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">MonoidHom.ker</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">QuotientGroup.lift</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>The fact that the target group is called <code class="docutils literal notranslate"><span class="pre">M</span></code> is the above snippet is a clue that having a
monoid structure on <code class="docutils literal notranslate"><span class="pre">M</span></code> would be enough.</p>
<p>An important special case is when <code class="docutils literal notranslate"><span class="pre">N</span> <span class="pre">=</span> <span class="pre">ker</span> <span class="pre">&#966;</span></code>. In that case the descended morphism is
injective and we get a group isomorphism onto its image. This result is often called
the first isomorphism theorem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">MonoidHom.ker</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">MonoidHom.range</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">QuotientGroup.quotientKerEquivRange</span><span class="w"> </span><span class="n">&#966;</span>
</pre></div>
</div>
<p>Applying the universal property to a composition of a morphism <code class="docutils literal notranslate"><span class="pre">&#966;</span> <span class="pre">:</span> <span class="pre">G</span> <span class="pre">&#8594;*</span> <span class="pre">G'</span></code>
with a quotient group projection <code class="docutils literal notranslate"><span class="pre">Quotient.mk'</span> <span class="pre">N'</span></code>,
we can also aim for a morphism from <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#10744;</span> <span class="pre">N</span></code> to <code class="docutils literal notranslate"><span class="pre">G'</span> <span class="pre">&#10744;</span> <span class="pre">N'</span></code>.
The condition required on <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> is usually formulated by saying &#8220;<code class="docutils literal notranslate"><span class="pre">&#966;</span></code> should send <code class="docutils literal notranslate"><span class="pre">N</span></code> inside
<code class="docutils literal notranslate"><span class="pre">N'</span></code>.&#8221; But this is equivalent to asking that <code class="docutils literal notranslate"><span class="pre">&#966;</span></code> should pull <code class="docutils literal notranslate"><span class="pre">N'</span></code> back over
<code class="docutils literal notranslate"><span class="pre">N</span></code>, and the latter condition is nicer to work with since the definition of pullback does not
involve an existential quantifier.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="n">G&#39;</span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G&#39;</span><span class="o">]</span>
<span class="w">    </span><span class="o">{</span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">N.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">N&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G&#39;</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">N&#39;.Normal</span><span class="o">]</span>
<span class="w">    </span><span class="o">{</span><span class="n">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">G&#39;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">Subgroup.comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">N&#39;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">G&#39;</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">N&#39;</span><span class="o">:=</span>
<span class="w">  </span><span class="n">QuotientGroup.map</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="n">N&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>One subtle point to keep in mind is that the type <code class="docutils literal notranslate"><span class="pre">G</span> <span class="pre">&#10744;</span> <span class="pre">N</span></code> really depends on <code class="docutils literal notranslate"><span class="pre">N</span></code>
(up to definitional equality), so having a proof that two normal subgroups <code class="docutils literal notranslate"><span class="pre">N</span></code> and <code class="docutils literal notranslate"><span class="pre">M</span></code> are equal
is not enough to make the corresponding quotients equal. However the universal properties does give
an isomorphism in this case.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">M.Normal</span><span class="o">]</span>
<span class="w">    </span><span class="o">[</span><span class="n">N.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">N</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">N</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">QuotientGroup.quotientMulEquivOfEq</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>As a final series of exercises for this section, we will prove that if <code class="docutils literal notranslate"><span class="pre">H</span></code> and <code class="docutils literal notranslate"><span class="pre">K</span></code> are disjoint
normal subgroups of a finite group <code class="docutils literal notranslate"><span class="pre">G</span></code> such that the product of their cardinalities is equal to
the cardinality of <code class="docutils literal notranslate"><span class="pre">G</span></code>
then <code class="docutils literal notranslate"><span class="pre">G</span></code> is isomorphic to <code class="docutils literal notranslate"><span class="pre">H</span> <span class="pre">&#215;</span> <span class="pre">K</span></code>. Recall that disjoint in this context means <code class="docutils literal notranslate"><span class="pre">H</span> <span class="pre">&#8851;</span> <span class="pre">K</span> <span class="pre">=</span> <span class="pre">&#8869;</span></code>.</p>
<p>We start with playing a bit with Lagrange&#8217;s lemma, without assuming the subgroups are normal
or disjoint.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">H</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subgroup</span><span class="w"> </span><span class="n">G</span><span class="o">}</span>

<span class="kn">open</span><span class="w"> </span><span class="n">MonoidHom</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Nat.card_pos</span><span class="w"> </span><span class="c1">-- The nonempty argument will be automatically inferred for subgroups</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Subgroup.index_eq_card</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Subgroup.index_mul_card</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Nat.eq_of_mul_eq_mul_right</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">aux_card_eq</span><span class="w"> </span><span class="o">[</span><span class="n">Finite</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Nat.card</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>From now on, we assume that our subgroups are normal and disjoint, and we assume the cardinality
condition. Now we construct the first building block of the desired isomorphism.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">[</span><span class="n">H.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">K.Normal</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Disjoint</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>
<span class="w">  </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Nat.bijective_iff_injective_and_card</span>
<span class="k">#check</span><span class="w"> </span><span class="n">ker_eq_bot_iff</span>
<span class="k">#check</span><span class="w"> </span><span class="n">restrict</span>
<span class="k">#check</span><span class="w"> </span><span class="n">ker_restrict</span>

<span class="kd">def</span><span class="w"> </span><span class="n">iso&#8321;</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">G</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Disjoint</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">Nat.card</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Now we can define our second building block.
We will need <code class="docutils literal notranslate"><span class="pre">MonoidHom.prod</span></code>, which builds a morphism from <code class="docutils literal notranslate"><span class="pre">G&#8320;</span></code> to <code class="docutils literal notranslate"><span class="pre">G&#8321;</span> <span class="pre">&#215;</span> <span class="pre">G&#8322;</span></code> out of
morphisms from <code class="docutils literal notranslate"><span class="pre">G&#8320;</span></code> to <code class="docutils literal notranslate"><span class="pre">G&#8321;</span></code> and <code class="docutils literal notranslate"><span class="pre">G&#8322;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">def</span><span class="w"> </span><span class="n">iso&#8322;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="o">(</span><span class="n">G</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">H</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We are ready to put all pieces together.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">MulEquiv.prodCongr</span>

<span class="kd">def</span><span class="w"> </span><span class="n">finalIso</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="w"> </span><span class="bp">&#8771;*</span><span class="w"> </span><span class="n">H</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
</section>
<section id="rings">
<span id="id2"></span><h2><span class="section-number">8.2. </span>Rings<a class="headerlink" href="#rings" title="Link to this heading">&#61633;</a></h2>
<section id="rings-their-units-morphisms-and-subrings">
<span id="index-4"></span><h3><span class="section-number">8.2.1. </span>Rings, their units, morphisms and subrings<a class="headerlink" href="#rings-their-units-morphisms-and-subrings" title="Link to this heading">&#61633;</a></h3>
<p>The type of ring structures on a type <code class="docutils literal notranslate"><span class="pre">R</span></code> is <code class="docutils literal notranslate"><span class="pre">Ring</span> <span class="pre">R</span></code>. The variant where multiplication is
assumed to be commutative is <code class="docutils literal notranslate"><span class="pre">CommRing</span> <span class="pre">R</span></code>. We have already seen that the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic will
prove any equality that follows from the axioms of a commutative ring.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
</pre></div>
</div>
<p>More exotic variants do not require that the addition on <code class="docutils literal notranslate"><span class="pre">R</span></code> forms a group but only an additive
monoid. The corresponding type classes are <code class="docutils literal notranslate"><span class="pre">Semiring</span> <span class="pre">R</span></code> and <code class="docutils literal notranslate"><span class="pre">CommSemiring</span> <span class="pre">R</span></code>.
The type of natural numbers is an important instance of <code class="docutils literal notranslate"><span class="pre">CommSemiring</span> <span class="pre">R</span></code>, as is any type
of functions taking values in the natural numbers.
Another important example is the type of ideals in a ring, which will be discussed below.
The name of the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic is doubly misleading, since it assumes commutativity but works
in semirings as well. In other words, it applies to any <code class="docutils literal notranslate"><span class="pre">CommSemiring</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
</pre></div>
</div>
<p>There are also versions of the ring and semiring classes that do not assume the existence of a
multiplicative unit or
the associativity of multiplication. We will not discuss those here.</p>
<p>Some concepts that are traditionally taught in an introduction to ring theory are actually about
the underlying multiplicative monoid.
A prominent example is the definition of the units of a ring. Every (multiplicative) monoid <code class="docutils literal notranslate"><span class="pre">M</span></code>
has a predicate <code class="docutils literal notranslate"><span class="pre">IsUnit</span> <span class="pre">:</span> <span class="pre">M</span> <span class="pre">&#8594;</span> <span class="pre">Prop</span></code> asserting existence of a two-sided inverse, a
type <code class="docutils literal notranslate"><span class="pre">Units</span> <span class="pre">M</span></code> of units with notation <code class="docutils literal notranslate"><span class="pre">M&#739;</span></code>, and a coercion to <code class="docutils literal notranslate"><span class="pre">M</span></code>.
The type <code class="docutils literal notranslate"><span class="pre">Units</span> <span class="pre">M</span></code> bundles an invertible element with its inverse as well as properties than ensure
that each is indeed the inverse of the other.
This implementation detail is relevant mainly when defining computable functions. In most
situations one can use <code class="docutils literal notranslate"><span class="pre">IsUnit.unit</span> <span class="pre">{x</span> <span class="pre">:</span> <span class="pre">M}</span> <span class="pre">:</span> <span class="pre">IsUnit</span> <span class="pre">x</span> <span class="pre">&#8594;</span> <span class="pre">M&#739;</span></code> to build a unit.
In the commutative case, one also has <code class="docutils literal notranslate"><span class="pre">Units.mkOfMulEqOne</span> <span class="pre">(x</span> <span class="pre">y</span> <span class="pre">:</span> <span class="pre">M)</span> <span class="pre">:</span> <span class="pre">x</span> <span class="pre">*</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">1</span> <span class="pre">&#8594;</span> <span class="pre">M&#739;</span></code>
which builds <code class="docutils literal notranslate"><span class="pre">x</span></code> seen as unit.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="bp">&#739;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8744;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Int.units_eq_one_or</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="bp">&#739;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Units.mul_inv</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Monoid</span><span class="w"> </span><span class="n">M</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Group</span><span class="w"> </span><span class="n">M</span><span class="bp">&#739;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>The type of ring morphisms between two (semi)-rings <code class="docutils literal notranslate"><span class="pre">R</span></code> and <code class="docutils literal notranslate"><span class="pre">S</span></code> is <code class="docutils literal notranslate"><span class="pre">RingHom</span> <span class="pre">R</span> <span class="pre">S</span></code>,
with notation <code class="docutils literal notranslate"><span class="pre">R</span> <span class="pre">&#8594;+*</span> <span class="pre">S</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">S</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">f.map_add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">S</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="bp">&#739;</span><span class="w"> </span><span class="bp">&#8594;*</span><span class="w"> </span><span class="n">S</span><span class="bp">&#739;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Units.map</span><span class="w"> </span><span class="n">f</span>
</pre></div>
</div>
<p>The isomorphism variant is <code class="docutils literal notranslate"><span class="pre">RingEquiv</span></code>, with notation <code class="docutils literal notranslate"><span class="pre">&#8771;+*</span></code>.</p>
<p>As with submonoids and subgroups, there is a <code class="docutils literal notranslate"><span class="pre">Subring</span> <span class="pre">R</span></code> type for subrings of a ring <code class="docutils literal notranslate"><span class="pre">R</span></code>,
but this type is a lot less useful than the type of subgroups since one cannot quotient a ring by
a subring.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Subring</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ring</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>Also notice that <code class="docutils literal notranslate"><span class="pre">RingHom.range</span></code> produces a subring.</p>
</section>
<section id="ideals-and-quotients">
<h3><span class="section-number">8.2.2. </span>Ideals and quotients<a class="headerlink" href="#ideals-and-quotients" title="Link to this heading">&#61633;</a></h3>
<p>For historical reasons, Mathlib only has a theory of ideals for commutative rings.
(The ring library was originally developed to make quick progress toward the foundations of modern
algebraic geometry.) So in this section we will work with commutative (semi)rings.
Ideals of <code class="docutils literal notranslate"><span class="pre">R</span></code> are defined as submodules of <code class="docutils literal notranslate"><span class="pre">R</span></code> seen as <code class="docutils literal notranslate"><span class="pre">R</span></code>-modules. Modules will
be covered later in a chapter on linear algebra, but this implementation detail can mostly be
safely ignored since most (but not all) relevant lemmas are restated in the special context of
ideals. But anonymous projection notation won&#8217;t always work as expected. For instance,
one cannot replace <code class="docutils literal notranslate"><span class="pre">Ideal.Quotient.mk</span> <span class="pre">I</span></code> by <code class="docutils literal notranslate"><span class="pre">I.Quotient.mk</span></code> in the snippet below because there
are two <code class="docutils literal notranslate"><span class="pre">.``s</span> <span class="pre">and</span> <span class="pre">so</span> <span class="pre">it</span> <span class="pre">will</span> <span class="pre">parse</span> <span class="pre">as</span> <span class="pre">``(Ideal.Quotient</span> <span class="pre">I).mk</span></code>; but <code class="docutils literal notranslate"><span class="pre">Ideal.Quotient</span></code> by itself
doesn&#8217;t exist.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.Quotient.mk</span><span class="w"> </span><span class="n">I</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Ideal.Quotient.mk</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.Quotient.eq_zero_iff_mem</span>
</pre></div>
</div>
<p>The universal property of quotient rings is <code class="docutils literal notranslate"><span class="pre">Ideal.Quotient.lift</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">S</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">RingHom.ker</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.Quotient.lift</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">H</span>
</pre></div>
</div>
<p>In particular it leads to the first isomorphism theorem for rings.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">S</span><span class="o">](</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">RingHom.ker</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="n">f.range</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">RingHom.quotientKerEquivRange</span><span class="w"> </span><span class="n">f</span>
</pre></div>
</div>
<p>Ideals form a complete lattice structure with the inclusion relation, as well as a semiring
structure. These two structures interact nicely.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">I</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">J</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">Submodule.mem_sup</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Ideal.mul_le_left</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Ideal.mul_le_right</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Ideal.mul_le_inf</span>
</pre></div>
</div>
<p>One can use ring morphisms to push ideals forward and pull them back using <code class="docutils literal notranslate"><span class="pre">Ideal.map</span></code> and
<code class="docutils literal notranslate"><span class="pre">Ideal.comap</span></code>, respectively. As usual,
the latter is more convenient to use since it does not involve an existential quantifier.
This explains why it is used to state the condition that allows us to build morphisms between
quotient rings.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">S</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">J</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">S</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">H</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">Ideal.comap</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">J</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.quotientMap</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">H</span>
</pre></div>
</div>
<p>One subtle point is that the type <code class="docutils literal notranslate"><span class="pre">R</span> <span class="pre">&#10744;</span> <span class="pre">I</span></code> really depends on <code class="docutils literal notranslate"><span class="pre">I</span></code>
(up to definitional equality), so having a proof that two ideals <code class="docutils literal notranslate"><span class="pre">I</span></code> and <code class="docutils literal notranslate"><span class="pre">J</span></code> are equal is not
enough to make the corresponding quotients equal. However, the universal properties do provide
an isomorphism in this case.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">J</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.quotEquivOfEq</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>We can now present the Chinese remainder isomorphism as an example. Pay attention to the difference
between the indexed infimum symbol <code class="docutils literal notranslate"><span class="pre">&#10757;</span></code> and the big product of types symbol <code class="docutils literal notranslate"><span class="pre">&#928;</span></code>. Depending on
your font, those can be pretty hard to distinguish.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Ideal.quotientInfRingEquivPiQuotient</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">hf</span>
</pre></div>
</div>
<p>The elementary version of the Chinese remainder theorem, a statement about <code class="docutils literal notranslate"><span class="pre">ZMod</span></code>, can be easily
deduced from the previous one:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">BigOperators</span><span class="w"> </span><span class="n">PiNotation</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">coprime</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="bp">.</span><span class="n">Coprime</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">ZMod</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8719;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">ZMod</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">ZMod.prodEquivPi</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">coprime</span>
</pre></div>
</div>
<p>As a series of exercises, we will reprove the Chinese remainder theorem in the general case.</p>
<p>We first need to define the map appearing in the theorem, as a ring morphism, using the
universal property of quotient rings.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>
<span class="kn">open</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">Quotient</span><span class="w"> </span><span class="n">Function</span>

<span class="k">#check</span><span class="w"> </span><span class="k">Pi</span><span class="bp">.</span><span class="n">ringHom</span>
<span class="k">#check</span><span class="w"> </span><span class="n">ker_Pi_Quotient_mk</span>

<span class="sd">/-- The homomorphism from ``R &#10744; &#10757; i, I i`` to ``&#928; i, R &#10744; I i`` featured in the Chinese</span>
<span class="sd">  Remainder Theorem. -/</span>
<span class="kd">def</span><span class="w"> </span><span class="n">chineseMap</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Make sure the following next two lemmas can be proven by <code class="docutils literal notranslate"><span class="pre">rfl</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span><span class="w"> </span><span class="n">chineseMap_mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">chineseMap</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">(</span><span class="n">Quotient.mk</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">Ideal.Quotient.mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">chineseMap_mk&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">chineseMap</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">(</span><span class="n">mk</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>The next lemma proves the easy half of the Chinese remainder theorem, without any assumption on
the family of ideals. The proof is less than one line long.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">injective_lift_iff</span>

<span class="kd">lemma</span><span class="w"> </span><span class="n">chineseMap_inj</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Injective</span><span class="w"> </span><span class="o">(</span><span class="n">chineseMap</span><span class="w"> </span><span class="n">I</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We are now ready for the heart of the theorem, which will show the surjectivity
of our <code class="docutils literal notranslate"><span class="pre">chineseMap</span></code>. First we need to know the different ways one can express the coprimality
(also called co-maximality assumption). Only the first two will be needed below.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">IsCoprime</span>
<span class="k">#check</span><span class="w"> </span><span class="n">isCoprime_iff_add</span>
<span class="k">#check</span><span class="w"> </span><span class="n">isCoprime_iff_exists</span>
<span class="k">#check</span><span class="w"> </span><span class="n">isCoprime_iff_sup_eq</span>
<span class="k">#check</span><span class="w"> </span><span class="n">isCoprime_iff_codisjoint</span>
</pre></div>
</div>
<p>We take the opportunity to use induction on <code class="docutils literal notranslate"><span class="pre">Finset</span></code>. Relevant lemmas on <code class="docutils literal notranslate"><span class="pre">Finset</span></code> are given
below.
Remember that the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic works for semirings and that the ideals of a ring form a semiring.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Finset.mem_insert_of_mem</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Finset.mem_insert_self</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">isCoprime_Inf</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">J</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#953;</span><span class="o">}</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">(</span><span class="n">J</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">(</span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">j</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">classical</span>
<span class="w">  </span><span class="n">simp_rw</span><span class="w"> </span><span class="o">[</span><span class="n">isCoprime_iff_add</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="bp">*</span>
<span class="w">  </span><span class="n">induction</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Finset.induction</span><span class="w"> </span><span class="k">with</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">empty</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="n">simp</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="bp">@</span><span class="n">insert</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">hs</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">Finset.iInf_insert</span><span class="o">,</span><span class="w"> </span><span class="n">inf_comm</span><span class="o">,</span><span class="w"> </span><span class="n">one_eq_top</span><span class="o">,</span><span class="w"> </span><span class="n">eq_top_iff</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">one_eq_top</span><span class="o">]</span>
<span class="w">      </span><span class="n">set</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">,</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">j</span>
<span class="w">      </span><span class="k">calc</span>
<span class="w">        </span><span class="mi">1</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="w">                  </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">        </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w">      </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">        </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">i</span><span class="w">  </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">        </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">J</span><span class="w"> </span><span class="n">i</span><span class="w">            </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We can now prove surjectivity of the map appearing in the Chinese remainder theorem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">lemma</span><span class="w"> </span><span class="n">chineseMap_surj</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">}</span>
<span class="w">    </span><span class="o">(</span><span class="n">hI</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Surjective</span><span class="w"> </span><span class="o">(</span><span class="n">chineseMap</span><span class="w"> </span><span class="n">I</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">classical</span>
<span class="w">  </span><span class="n">intro</span><span class="w"> </span><span class="n">g</span>
<span class="w">  </span><span class="n">choose</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">hf</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">Ideal.Quotient.mk_surjective</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="o">)</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">key</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="n">mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">mk</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">j</span><span class="o">)</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">i</span>
<span class="w">    </span><span class="k">have</span><span class="w"> </span><span class="n">hI&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="o">({</span><span class="n">i</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finset</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="bp">&#7580;</span><span class="o">,</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">I</span><span class="w"> </span><span class="n">j</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">    </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">choose</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">he</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">key</span>
<span class="w">  </span><span class="n">use</span><span class="w"> </span><span class="n">mk</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">i</span><span class="o">)</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Now all the pieces come together in the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">noncomputable</span><span class="w"> </span><span class="kd">def</span><span class="w"> </span><span class="n">chineseIso</span><span class="w"> </span><span class="o">[</span><span class="n">Fintype</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Ideal</span><span class="w"> </span><span class="n">R</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">IsCoprime</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">j</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="bp">&#10757;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;+*</span><span class="w"> </span><span class="bp">&#928;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">{</span><span class="w"> </span><span class="n">Equiv.ofBijective</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">chineseMap_inj</span><span class="w"> </span><span class="n">f</span><span class="o">,</span><span class="w"> </span><span class="n">chineseMap_surj</span><span class="w"> </span><span class="n">hf</span><span class="o">&#10217;,</span>
<span class="w">    </span><span class="n">chineseMap</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="k">with</span><span class="w"> </span><span class="o">}</span>
</pre></div>
</div>
</section>
<section id="algebras-and-polynomials">
<h3><span class="section-number">8.2.3. </span>Algebras and polynomials<a class="headerlink" href="#algebras-and-polynomials" title="Link to this heading">&#61633;</a></h3>
<p>Given a commutative (semi)ring <code class="docutils literal notranslate"><span class="pre">R</span></code>, an <em>algebra over</em> <code class="docutils literal notranslate"><span class="pre">R</span></code> is a semiring <code class="docutils literal notranslate"><span class="pre">A</span></code> equipped
with a ring morphism whose image commutes with every element of <code class="docutils literal notranslate"><span class="pre">A</span></code>. This is encoded as
a type class <code class="docutils literal notranslate"><span class="pre">Algebra</span> <span class="pre">R</span> <span class="pre">A</span></code>.
The morphism from <code class="docutils literal notranslate"><span class="pre">R</span></code> to <code class="docutils literal notranslate"><span class="pre">A</span></code> is called the structure map and is denoted
<code class="docutils literal notranslate"><span class="pre">algebraMap</span> <span class="pre">R</span> <span class="pre">A</span> <span class="pre">:</span> <span class="pre">R</span> <span class="pre">&#8594;+*</span> <span class="pre">A</span></code> in Lean.
Multiplication of <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">:</span> <span class="pre">A</span></code> by <code class="docutils literal notranslate"><span class="pre">algebraMap</span> <span class="pre">R</span> <span class="pre">A</span> <span class="pre">r</span></code> for some <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">:</span> <span class="pre">R</span></code> is called the scalar
multiplication of <code class="docutils literal notranslate"><span class="pre">a</span></code> by <code class="docutils literal notranslate"><span class="pre">r</span></code> and denoted by <code class="docutils literal notranslate"><span class="pre">r</span> <span class="pre">&#8226;</span> <span class="pre">a</span></code>.
Note that this notion of algebra is sometimes called an <em>associative unital algebra</em> to emphasize the
existence of more general notions of algebra.</p>
<p>The fact that <code class="docutils literal notranslate"><span class="pre">algebraMap</span> <span class="pre">R</span> <span class="pre">A</span></code> is ring morphism packages together a lot of properties of scalar
multiplication, such as the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">A</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Algebra</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="n">A</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">A</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">r&#39;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">add_smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="n">a</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="n">A</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">A</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Algebra</span><span class="w"> </span><span class="n">R</span><span class="w"> </span><span class="n">A</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">A</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">r&#39;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mul_smul</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="n">r&#39;</span><span class="w"> </span><span class="n">a</span>
</pre></div>
</div>
<p>The morphisms between two <code class="docutils literal notranslate"><span class="pre">R</span></code>-algebras <code class="docutils literal notranslate"><span class="pre">A</span></code> and <code class="docutils literal notranslate"><span class="pre">B</span></code> are ring morphisms
which commute with scalar multiplication by elements of <code class="docutils literal notranslate"><span class="pre">R</span></code>. They are bundled morphisms
with type <code class="docutils literal notranslate"><span class="pre">AlgHom</span> <span class="pre">R</span> <span class="pre">A</span> <span class="pre">B</span></code>, which is denoted by <code class="docutils literal notranslate"><span class="pre">A</span> <span class="pre">&#8594;&#8336;[R]</span> <span class="pre">B</span></code>.</p>
<p>Important examples of non-commutative algebras include algebras of endomorphisms and
algebras of square matrices, both of which will be covered in the chapter on linear algebra.
In this chapter we will discuss one of the most important examples of a commutative algebra,
namely, polynomial algebras.</p>
<p>The algebra of univariate polynomials with coefficients in <code class="docutils literal notranslate"><span class="pre">R</span></code> is called <code class="docutils literal notranslate"><span class="pre">Polynomial</span> <span class="pre">R</span></code>,
which can be written as <code class="docutils literal notranslate"><span class="pre">R[X]</span></code> as soon as one opens the <code class="docutils literal notranslate"><span class="pre">Polynomial</span></code> namespace.
The algebra structure map from <code class="docutils literal notranslate"><span class="pre">R</span></code> to <code class="docutils literal notranslate"><span class="pre">R[X]</span></code> is denoted by <code class="docutils literal notranslate"><span class="pre">C</span></code>,
which stands for &#8220;constant&#8221; since the corresponding
polynomial functions are always constant. The indeterminate is denoted by <code class="docutils literal notranslate"><span class="pre">X</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Polynomial</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">X</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span>
</pre></div>
</div>
<p>In the first example above, it is crucial that we give Lean the expected type since it cannot be
determined from the body of the definition. In the second example, the target polynomial
algebra can be inferred from our use of <code class="docutils literal notranslate"><span class="pre">C</span> <span class="pre">r</span></code> since the type of <code class="docutils literal notranslate"><span class="pre">r</span></code> is known.</p>
<p>Because <code class="docutils literal notranslate"><span class="pre">C</span></code> is a ring morphism from <code class="docutils literal notranslate"><span class="pre">R</span></code> to <code class="docutils literal notranslate"><span class="pre">R[X]</span></code>, we can use all ring morphisms lemmas
such as <code class="docutils literal notranslate"><span class="pre">map_zero</span></code>, <code class="docutils literal notranslate"><span class="pre">map_one</span></code>, <code class="docutils literal notranslate"><span class="pre">map_mul</span></code>, and <code class="docutils literal notranslate"><span class="pre">map_pow</span></code> before computing in the ring
<code class="docutils literal notranslate"><span class="pre">R[X]</span></code>. For example:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">C.map_pow</span><span class="o">]</span>
<span class="w">  </span><span class="n">ring</span>
</pre></div>
</div>
<p>You can access coefficients using <code class="docutils literal notranslate"><span class="pre">Polynomial.coeff</span></code></p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="o">:</span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="bp">.</span><span class="n">coeff</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="bp">.</span><span class="n">coeff</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>Defining the degree of a polynomial is always tricky because of the special case of the zero
polynomial. Mathlib has two variants: <code class="docutils literal notranslate"><span class="pre">Polynomial.natDegree</span> <span class="pre">:</span> <span class="pre">R[X]</span> <span class="pre">&#8594;</span> <span class="pre">&#8469;</span></code> assigns degree
<code class="docutils literal notranslate"><span class="pre">0</span></code> to the zero polynomial, and <code class="docutils literal notranslate"><span class="pre">Polynomial.degree</span> <span class="pre">:</span> <span class="pre">R[X]</span> <span class="pre">&#8594;</span> <span class="pre">WithBot</span> <span class="pre">&#8469;</span></code> assigns <code class="docutils literal notranslate"><span class="pre">&#8869;</span></code>.
In the latter, <code class="docutils literal notranslate"><span class="pre">WithBot</span> <span class="pre">&#8469;</span></code> can be seen as <code class="docutils literal notranslate"><span class="pre">&#8469;</span> <span class="pre">&#8746;</span> <span class="pre">{-&#8734;}</span></code>, except that <code class="docutils literal notranslate"><span class="pre">-&#8734;</span></code> is denoted <code class="docutils literal notranslate"><span class="pre">&#8869;</span></code>,
the same symbol as the bottom element in a complete lattice. This special value is used as the
degree of the zero polynomial, and it is absorbent for addition. (It is almost absorbent for
multiplication, except that <code class="docutils literal notranslate"><span class="pre">&#8869;</span> <span class="pre">*</span> <span class="pre">0</span> <span class="pre">=</span> <span class="pre">0</span></code>.)</p>
<p>Morally speaking, the <code class="docutils literal notranslate"><span class="pre">degree</span></code> version is the correct one. For instance, it allows us to state
the expected formula for the degree of a product (assuming the base ring has no zero divisor).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Semiring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NoZeroDivisors</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">]}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">degree</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">degree</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">degree</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Polynomial.degree_mul</span>
</pre></div>
</div>
<p>Whereas the version for <code class="docutils literal notranslate"><span class="pre">natDegree</span></code> needs to assume non-zero polynomials.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Semiring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NoZeroDivisors</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">]}</span><span class="w"> </span><span class="o">(</span><span class="n">hp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hq</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">natDegree</span><span class="w"> </span><span class="o">(</span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">natDegree</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">natDegree</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Polynomial.natDegree_mul</span><span class="w"> </span><span class="n">hp</span><span class="w"> </span><span class="n">hq</span>
</pre></div>
</div>
<p>However, <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> is much nicer to use than <code class="docutils literal notranslate"><span class="pre">WithBot</span> <span class="pre">&#8469;</span></code>, so Mathlib makes both versions available
and provides lemmas to convert between them. Also, <code class="docutils literal notranslate"><span class="pre">natDegree</span></code> is the more convenient definition
to use when computing the degree of a composition. Composition of polynomial is <code class="docutils literal notranslate"><span class="pre">Polynomial.comp</span></code>
and we have:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Semiring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NoZeroDivisors</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">]}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">natDegree</span><span class="w"> </span><span class="o">(</span><span class="n">comp</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">natDegree</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">natDegree</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Polynomial.natDegree_comp</span>
</pre></div>
</div>
<p>Polynomials give rise to polynomial functions: any polynomial can be evaluated on <code class="docutils literal notranslate"><span class="pre">R</span></code>
using <code class="docutils literal notranslate"><span class="pre">Polynomial.eval</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">P</span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">P.eval</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="bp">.</span><span class="n">eval</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>In particular, there is a predicate, <code class="docutils literal notranslate"><span class="pre">IsRoot</span></code>, that holds for elements <code class="docutils literal notranslate"><span class="pre">r</span></code> in <code class="docutils literal notranslate"><span class="pre">R</span></code> where a
polynomial vanishes.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">P</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsRoot</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">P.eval</span><span class="w"> </span><span class="n">r</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Iff.rfl</span>
</pre></div>
</div>
<p>We would like to say that, assuming <code class="docutils literal notranslate"><span class="pre">R</span></code> has no zero divisor, a polynomial has at most as many
roots as its degree, where the roots are counted with multiplicities.
But once again the case of the zero polynomial is painful.
So Mathlib defines <code class="docutils literal notranslate"><span class="pre">Polynomial.roots</span></code> to send a polynomial <code class="docutils literal notranslate"><span class="pre">P</span></code> to a multiset,
i.e. the finite set that is defined to be empty if <code class="docutils literal notranslate"><span class="pre">P</span></code> is zero and the roots of <code class="docutils literal notranslate"><span class="pre">P</span></code>,
with multiplicities, otherwise. This is defined only when the underlying ring is a domain
since otherwise the definition does not have good properties.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsDomain</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="bp">.</span><span class="n">roots</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">{</span><span class="n">r</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">roots_X_sub_C</span><span class="w"> </span><span class="n">r</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsDomain</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">r</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">):</span>
<span class="w">    </span><span class="o">((</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">r</span><span class="o">)</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="bp">.</span><span class="n">roots</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="o">{</span><span class="n">r</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>Both <code class="docutils literal notranslate"><span class="pre">Polynomial.eval</span></code> and <code class="docutils literal notranslate"><span class="pre">Polynomial.roots</span></code> consider only the coefficients ring. They do not
allow us to say that <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">-</span> <span class="pre">2</span> <span class="pre">:</span> <span class="pre">&#8474;[X]</span></code> has a root in <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> or that <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">+</span> <span class="pre">1</span> <span class="pre">:</span> <span class="pre">&#8477;[X]</span></code> has a root in
<code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>. For this, we need <code class="docutils literal notranslate"><span class="pre">Polynomial.aeval</span></code>, which will evaluate <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">:</span> <span class="pre">R[X]</span></code> in any <code class="docutils literal notranslate"><span class="pre">R</span></code>-algebra.
More precisely, given a semiring <code class="docutils literal notranslate"><span class="pre">A</span></code> and an instance of <code class="docutils literal notranslate"><span class="pre">Algebra</span> <span class="pre">R</span> <span class="pre">A</span></code>, <code class="docutils literal notranslate"><span class="pre">Polynomial.aeval</span></code> sends
every element of <code class="docutils literal notranslate"><span class="pre">a</span></code> along the <code class="docutils literal notranslate"><span class="pre">R</span></code>-algebra morphism of evaluation at <code class="docutils literal notranslate"><span class="pre">a</span></code>. Since <code class="docutils literal notranslate"><span class="pre">AlgHom</span></code>
has a coercion to functions, one can apply it to a polynomial.
But <code class="docutils literal notranslate"><span class="pre">aeval</span></code> does not have a polynomial as an argument, so one cannot use dot notation like in
<code class="docutils literal notranslate"><span class="pre">P.eval</span></code> above.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">aeval</span><span class="w"> </span><span class="n">Complex.I</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>The function corresponding to <code class="docutils literal notranslate"><span class="pre">roots</span></code> in this context is <code class="docutils literal notranslate"><span class="pre">aroots</span></code> which takes a polynomial
and then an algebra and outputs a multiset (with the same caveat about the zero polynomial as
for <code class="docutils literal notranslate"><span class="pre">roots</span></code>).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Complex</span><span class="w"> </span><span class="n">Polynomial</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">aroots</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="n">&#8450;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">{</span><span class="n">Complex.I</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">I</span><span class="o">}</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">suffices</span><span class="w"> </span><span class="n">roots</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8450;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">{</span><span class="n">I</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">I</span><span class="o">}</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simpa</span><span class="w"> </span><span class="o">[</span><span class="n">aroots_def</span><span class="o">]</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">factored</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8450;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">I</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="n">I</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="k">have</span><span class="w"> </span><span class="n">key</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">C</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">I</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8450;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">C_mul</span><span class="o">]</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">C_neg</span><span class="o">]</span>
<span class="w">    </span><span class="n">linear_combination</span><span class="w"> </span><span class="n">key</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">p_ne_zero</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">I</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="n">I</span><span class="o">))</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">H</span>
<span class="w">    </span><span class="n">apply_fun</span><span class="w"> </span><span class="n">eval</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">H</span>
<span class="w">    </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">eval</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">H</span>
<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">only</span><span class="w"> </span><span class="o">[</span><span class="n">factored</span><span class="o">,</span><span class="w"> </span><span class="n">roots_mul</span><span class="w"> </span><span class="n">p_ne_zero</span><span class="o">,</span><span class="w"> </span><span class="n">roots_X_sub_C</span><span class="o">]</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="c1">-- Mathlib knows about D&#39;Alembert-Gauss theorem: ``&#8450;`` is algebraically closed.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsAlgClosed</span><span class="w"> </span><span class="n">&#8450;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">inferInstance</span>
</pre></div>
</div>
<p>More generally, given an ring morphism <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">R</span> <span class="pre">&#8594;+*</span> <span class="pre">S</span></code> one can evaluate <code class="docutils literal notranslate"><span class="pre">P</span> <span class="pre">:</span> <span class="pre">R[X]</span></code> at a point
in <code class="docutils literal notranslate"><span class="pre">S</span></code> using <code class="docutils literal notranslate"><span class="pre">Polynomial.eval&#8322;</span></code>. This one produces an actual function from <code class="docutils literal notranslate"><span class="pre">R[X]</span></code> to <code class="docutils literal notranslate"><span class="pre">S</span></code>
since it does not assume the existence of a <code class="docutils literal notranslate"><span class="pre">Algebra</span> <span class="pre">R</span> <span class="pre">S</span></code> instance, so dot notation works as
you would expect.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Complex.ofRealHom</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;+*</span><span class="w"> </span><span class="n">&#8450;</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">X</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">[</span><span class="n">X</span><span class="o">])</span><span class="bp">.</span><span class="n">eval&#8322;</span><span class="w"> </span><span class="n">Complex.ofRealHom</span><span class="w"> </span><span class="n">Complex.I</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
<p>Let us end by mentioning multivariate polynomials briefly. Given a commutative semiring <code class="docutils literal notranslate"><span class="pre">R</span></code>,
the <code class="docutils literal notranslate"><span class="pre">R</span></code>-algebra of polynomials with coefficients in <code class="docutils literal notranslate"><span class="pre">R</span></code> and indeterminates indexed by
a type <code class="docutils literal notranslate"><span class="pre">&#963;</span></code> is <code class="docutils literal notranslate"><span class="pre">MVPolynomial</span> <span class="pre">&#963;</span> <span class="pre">R</span></code>. Given <code class="docutils literal notranslate"><span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#963;</span></code>, the corresponding polynomial is
<code class="docutils literal notranslate"><span class="pre">MvPolynomial.X</span> <span class="pre">i</span></code>. (As usual, one can open the <code class="docutils literal notranslate"><span class="pre">MVPolynomial</span></code> namespace to shorten this
to <code class="docutils literal notranslate"><span class="pre">X</span> <span class="pre">i</span></code>.)
For instance, if we want two indeterminates we can use
<code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">2</span></code> as <code class="docutils literal notranslate"><span class="pre">&#963;</span></code> and write the polynomial defining the unit circle in <span class="math notranslate nohighlight">\(\mathbb{R}^2`\)</span> as:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">MvPolynomial</span>

<span class="kd">def</span><span class="w"> </span><span class="n">circleEquation</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MvPolynomial</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="mi">1</span>
</pre></div>
</div>
<p>Recall that function application has a very high precedence so the expression above is read as
<code class="docutils literal notranslate"><span class="pre">(X</span> <span class="pre">0)</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">+</span> <span class="pre">(X</span> <span class="pre">1)</span> <span class="pre">^</span> <span class="pre">2</span> <span class="pre">-</span> <span class="pre">1</span></code>.
We can evaluate it to make sure the point with coordinates <span class="math notranslate nohighlight">\((1, 0)\)</span> is on the circle.
Recall the <code class="docutils literal notranslate"><span class="pre">![...]</span></code> notation denotes elements of <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">X</span></code> for some natural number <code class="docutils literal notranslate"><span class="pre">n</span></code>
determined by the number of arguments and some type <code class="docutils literal notranslate"><span class="pre">X</span></code> determined by the type of arguments.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MvPolynomial.eval</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w"> </span><span class="n">circleEquation</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">circleEquation</span><span class="o">]</span>
</pre></div>
</div>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C07_Hierarchies.html" class="btn btn-neutral float-left" title="7. Hierarchies" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C09_Linear_Algebra.html" class="btn btn-neutral float-right" title="9. Linear algebra" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020, Jeremy Avigad, Patrick Massot.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>