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
1148. 1148
1149. 1149
1150. 1150
1151. 1151
1152. 1152
1153. 1153
1154. 1154
1155. 1155
1156. 1156
1157. 1157
1158. 1158
1159. 1159
1160. 1160
1161. 1161
1162. 1162
1163. 1163
1164. 1164
1165. 1165
1166. 1166
1167. 1167
1168. 1168
1169. 1169
1170. 1170
1171. 1171
1172. 1172
1173. 1173
1174. 1174
1175. 1175
1176. 1176
1177. 1177
1178. 1178
1179. 1179
1180. 1180
1181. 1181
1182. 1182
1183. 1183
1184. 1184
1185. 1185
1186. 1186
1187. 1187
1188. 1188
1189. 1189
1190. 1190
1191. 1191
1192. 1192
1193. 1193
1194. 1194
1195. 1195
1196. 1196
1197. 1197
1198. 1198
1199. 1199
1200. 1200
1201. 1201
1202. 1202
1203. 1203
1204. 1204
1205. 1205
1206. 1206
1207. 1207
1208. 1208
1209. 1209
1210. 1210
1211. 1211
1212. 1212
1213. 1213
1214. 1214
1215. 1215
1216. 1216
1217. 1217
1218. 1218
1219. 1219
1220. 1220
1221. 1221
1222. 1222
1223. 1223
1224. 1224
1225. 1225
1226. 1226
1227. 1227
1228. 1228
1229. 1229
1230. 1230
1231. 1231
1232. 1232
1233. 1233
1234. 1234
1235. 1235
1236. 1236
1237. 1237
1238. 1238
1239. 1239
1240. 1240
1241. 1241
1242. 1242
1243. 1243
1244. 1244
1245. 1245
1246. 1246
1247. 1247
1248. 1248
1249. 1249
1250. 1250
1251. 1251
1252. 1252
1253. 1253
1254. 1254
1255. 1255
1256. 1256
1257. 1257
1258. 1258
1259. 1259
1260. 1260
1261. 1261
1262. 1262
1263. 1263
1264. 1264
1265. 1265
1266. 1266
1267. 1267
1268. 1268
1269. 1269
1270. 1270
1271. 1271
1272. 1272
1273. 1273

<!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>10. Linear algebra &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
      <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=7048e04d"></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="11. Topology" href="C11_Topology.html" />
    <link rel="prev" title="9. Groups and Rings" href="C09_Groups_and_Rings.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_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">10. Linear algebra</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#vector-spaces-and-linear-maps">10.1. Vector spaces and linear maps</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#vector-spaces">10.1.1. Vector spaces</a></li>
<li class="toctree-l3"><a class="reference internal" href="#linear-maps">10.1.2. Linear maps</a></li>
<li class="toctree-l3"><a class="reference internal" href="#sums-and-products-of-vector-spaces">10.1.3. Sums and products of vector spaces</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#subspaces-and-quotients">10.2. Subspaces and quotients</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#subspaces">10.2.1. Subspaces</a></li>
<li class="toctree-l3"><a class="reference internal" href="#complete-lattice-structure-and-internal-direct-sums">10.2.2. Complete lattice structure and internal direct sums</a></li>
<li class="toctree-l3"><a class="reference internal" href="#subspace-spanned-by-a-set">10.2.3. Subspace spanned by a set</a></li>
<li class="toctree-l3"><a class="reference internal" href="#pushing-and-pulling-subspaces">10.2.4. Pushing and pulling subspaces</a></li>
<li class="toctree-l3"><a class="reference internal" href="#quotient-spaces">10.2.5. Quotient spaces</a></li>
</ul>
</li>
<li class="toctree-l2"><a class="reference internal" href="#endomorphisms">10.3. Endomorphisms</a></li>
<li class="toctree-l2"><a class="reference internal" href="#matrices-bases-and-dimension">10.4. Matrices, bases and dimension</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#matrices">10.4.1. Matrices</a></li>
<li class="toctree-l3"><a class="reference internal" href="#bases">10.4.2. Bases</a></li>
<li class="toctree-l3"><a class="reference internal" href="#dimension">10.4.3. Dimension</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. 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">10. </span>Linear algebra</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C10_Linear_Algebra.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="linear-algebra">
<span id="id1"></span><h1><span class="section-number">10. </span>Linear algebra<a class="headerlink" href="#linear-algebra" title="Link to this heading">&#61633;</a></h1>
<section id="vector-spaces-and-linear-maps">
<h2><span class="section-number">10.1. </span>Vector spaces and linear maps<a class="headerlink" href="#vector-spaces-and-linear-maps" title="Link to this heading">&#61633;</a></h2>
<section id="vector-spaces">
<h3><span class="section-number">10.1.1. </span>Vector spaces<a class="headerlink" href="#vector-spaces" title="Link to this heading">&#61633;</a></h3>
<p id="index-0">We will start directly abstract linear algebra, taking place in a vector space over any field.
However you can find information about matrices in
<a class="reference internal" href="#matrices"><span class="std std-numref">Section 10.4.1</span></a> which does not logically depend on this abstract theory.
Mathlib actually deals with a more general version of linear algebra involving the word module,
but for now we will pretend this is only an eccentric spelling habit.</p>
<p>The way to say &#8220;let <span class="math notranslate nohighlight">\(K\)</span> be a field and let <span class="math notranslate nohighlight">\(V\)</span> be a vector space over <span class="math notranslate nohighlight">\(K\)</span>&#8221;
(and make them implicit arguments to later results) is:</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">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">Field</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">V</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">V</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>
</pre></div>
</div>
<p>We explained in <a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 8</span></a> why we need two separate
typeclasses <code class="docutils literal notranslate"><span class="pre">[AddCommGroup</span> <span class="pre">V]</span> <span class="pre">[Module</span> <span class="pre">K</span> <span class="pre">V]</span></code>.
The short version is the following.
Mathematically we want to say that having a <span class="math notranslate nohighlight">\(K\)</span>-vector space structure
implies having an additive commutative group structure.
We could tell this to Lean. But then whenever Lean would need to find such a
group structure on a type <span class="math notranslate nohighlight">\(V\)</span>, it would go hunting for vector space
structures using a <em>completely unspecified</em> field <span class="math notranslate nohighlight">\(K\)</span> that cannot be inferred
from <span class="math notranslate nohighlight">\(V\)</span>.
This would be very bad for the type class synthesis system.</p>
<p>The multiplication of a vector <cite>v</cite> by a scalar <cite>a</cite> is denoted by
<cite>a &#8226; v</cite>. We list a couple of algebraic rules about the interaction of this
operation with addition in the following examples. Of course <cite>simp</cite> or <cite>apply?</cite>
would find those proofs. There is also a <cite>module</cite> tactic that solves goals
following from the axioms of vector spaces and fields, in the same way the
<cite>ring</cite> tactic is used in commutative rings or the <cite>group</cite> tactic is used in
groups. But it is still useful to remember that scalar
multiplication is abbreviated <cite>smul</cite> in lemma names.</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">a</span><span class="w"> </span><span class="o">:</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="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="o">(</span><span class="n">u</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">v</span><span class="o">)</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">&#8226;</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">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">smul_add</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">v</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</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">V</span><span class="o">)</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="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8226;</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">a</span><span class="w"> </span><span class="bp">&#8226;</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">b</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">u</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">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">u</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</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">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8226;</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">b</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">&#8226;</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">smul_comm</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">u</span>
</pre></div>
</div>
<p>As a quick note for more advanced readers, let us point out that, as suggested by
terminology, Mathlib&#8217;s linear algebra also covers modules over (not necessarily commutative)
rings.
In fact it even covers semi-modules over semi-rings. If you think you do not need
this level of generality, you can meditate the following example that nicely captures
a lot of algebraic rules about ideals acting on submodules:</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">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">CommSemiring</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">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">Module</span><span class="w"> </span><span class="n">R</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">Module</span><span class="w"> </span><span class="o">(</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">Submodule</span><span class="w"> </span><span class="n">R</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">inferInstance</span>
</pre></div>
</div>
</section>
<section id="linear-maps">
<h3><span class="section-number">10.1.2. </span>Linear maps<a class="headerlink" href="#linear-maps" title="Link to this heading">&#61633;</a></h3>
<p id="index-1">Next we need linear maps. Like group morphisms, linear maps in Mathlib are bundled maps, i.e. packages
made of a map and proofs of its linearity properties.
Those bundled maps are converted to ordinary functions when applied.
See <a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 8</span></a> for more information about this design.</p>
<p>The type of linear maps between two <code class="docutils literal notranslate"><span class="pre">K</span></code>-vector spaces
<code class="docutils literal notranslate"><span class="pre">V</span></code> and <code class="docutils literal notranslate"><span class="pre">W</span></code> is denoted by <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">W</span></code>. The subscript <cite>l</cite> stands for linear.
At first it may feel odd to specify <code class="docutils literal notranslate"><span class="pre">K</span></code> in this notation.
But this is crucial when several fields come into play.
For instance real-linear maps from <span class="math notranslate nohighlight">\(&#8450;\)</span> to <span class="math notranslate nohighlight">\(&#8450;\)</span> are every map <span class="math notranslate nohighlight">\(z &#8614; az + b\bar{z}\)</span>
while only the maps <span class="math notranslate nohighlight">\(z &#8614; az\)</span> are complex linear, and this difference is crucial in
complex analysis.</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">W</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">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">]</span>

<span class="kd">variable</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="kd">example</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">K</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">v</span><span class="o">)</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">&#8226;</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">map_smul</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">v</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="n">w</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">w</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">w</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">map_add</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">w</span>
</pre></div>
</div>
<p>Note that <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">W</span></code> itself carries interesting algebraic structures (this
is part of the motivation for bundling those maps).
It is a <code class="docutils literal notranslate"><span class="pre">K</span></code>-vector space so we can add linear maps and multiply them by scalars.</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">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>
</pre></div>
</div>
<p>One downside of using bundled maps is that we cannot use ordinary function composition.
We need to use <code class="docutils literal notranslate"><span class="pre">LinearMap.comp</span></code> or the notation <code class="docutils literal notranslate"><span class="pre">&#8728;&#8343;</span></code>.</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">&#952;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;.comp</span><span class="w"> </span><span class="n">&#952;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">&#952;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>
</pre></div>
</div>
<p>There are two main ways to construct linear maps.
First we can build the structure by providing the function and the linearity proof.
As usual, this is facilitated by the structure code action: you can type
<code class="docutils literal notranslate"><span class="pre">example</span> <span class="pre">:</span> <span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">V</span> <span class="pre">:=</span> <span class="pre">_</span></code> and use the code action &#8220;Generate a skeleton&#8221; attached to the
underscore.</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">toFun</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">v</span>
<span class="w">  </span><span class="n">map_add&#39;</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">smul_add</span><span class="w"> </span><span class="bp">..</span>
<span class="w">  </span><span class="n">map_smul&#39;</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">smul_comm</span><span class="w"> </span><span class="bp">..</span>
</pre></div>
</div>
<p>You may wonder why the proof fields of <code class="docutils literal notranslate"><span class="pre">LinearMap</span></code> have names ending with a prime.
This is because they are defined before the coercion to functions is defined, hence they are
phrased in terms of <code class="docutils literal notranslate"><span class="pre">LinearMap.toFun</span></code>. Then they are restated as <code class="docutils literal notranslate"><span class="pre">LinearMap.map_add</span></code>
and <code class="docutils literal notranslate"><span class="pre">LinearMap.map_smul</span></code> in terms of the coercion to function.
This is not yet the end of the story. One also wants a version of <code class="docutils literal notranslate"><span class="pre">map_add</span></code> that applies to
any (bundled) map preserving addition, such as additive group morphisms, linear maps, continuous
linear maps, <code class="docutils literal notranslate"><span class="pre">K</span></code>-algebra maps etc&#8230; This one is <code class="docutils literal notranslate"><span class="pre">map_add</span></code> (in the root namespace).
The intermediate version, <code class="docutils literal notranslate"><span class="pre">LinearMap.map_add</span></code> is a bit redundant but allows to use dot notation, which
can be nice sometimes. A similar story exists for <code class="docutils literal notranslate"><span class="pre">map_smul</span></code>, and the general framework
is explained in <a class="reference internal" href="C08_Hierarchies.html#hierarchies"><span class="std std-numref">Chapter 8</span></a>.</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">&#966;.map_add&#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">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">V</span><span class="o">,</span><span class="w"> </span><span class="n">&#966;.toFun</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">&#966;.toFun</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">&#966;.toFun</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;.map_add</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="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">,</span><span class="w"> </span><span class="n">&#966;</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">&#966;</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">&#966;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">map_add</span><span class="w"> </span><span class="n">&#966;</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="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">,</span><span class="w"> </span><span class="n">&#966;</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">&#966;</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">&#966;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
</pre></div>
</div>
<p>One can also build linear maps from the ones that are already defined in Mathlib
using various combinators.
For instance the above example is already known as <code class="docutils literal notranslate"><span class="pre">LinearMap.lsmul</span> <span class="pre">K</span> <span class="pre">V</span> <span class="pre">3</span></code>.
There are several reason why <code class="docutils literal notranslate"><span class="pre">K</span></code> and <code class="docutils literal notranslate"><span class="pre">V</span></code> are explicit arguments here.
The most pressing one is that from a bare <code class="docutils literal notranslate"><span class="pre">LinearMap.lsmul</span> <span class="pre">3</span></code> there would be no way
for Lean to infer <code class="docutils literal notranslate"><span class="pre">V</span></code> or even <code class="docutils literal notranslate"><span class="pre">K</span></code>.
But also <code class="docutils literal notranslate"><span class="pre">LinearMap.lsmul</span> <span class="pre">K</span> <span class="pre">V</span></code> is an interesting object by itself: it has type
<code class="docutils literal notranslate"><span class="pre">K</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">V</span></code>, meaning it is a <code class="docutils literal notranslate"><span class="pre">K</span></code>-linear map from <code class="docutils literal notranslate"><span class="pre">K</span></code>
&#8212;seen as a vector space over itself&#8212; to the space of <code class="docutils literal notranslate"><span class="pre">K</span></code>-linear maps from <code class="docutils literal notranslate"><span class="pre">V</span></code> to <code class="docutils literal notranslate"><span class="pre">V</span></code>.</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">LinearMap.lsmul</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">LinearMap.lsmul</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
</pre></div>
</div>
<p>There is also a type <code class="docutils literal notranslate"><span class="pre">LinearEquiv</span></code> of linear isomorphisms denoted by <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8771;&#8343;[K]</span> <span class="pre">W</span></code>.
The inverse of <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">V</span> <span class="pre">&#8771;&#8343;[K]</span> <span class="pre">W</span></code> is <code class="docutils literal notranslate"><span class="pre">f.symm</span> <span class="pre">:</span> <span class="pre">W</span> <span class="pre">&#8771;&#8343;[K]</span> <span class="pre">V</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">f.trans</span> <span class="pre">g</span></code> also denoted by <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">&#8810;&#8811;&#8343;</span> <span class="pre">g</span></code>, and
the identity isomorphism of <code class="docutils literal notranslate"><span class="pre">V</span></code> is <code class="docutils literal notranslate"><span class="pre">LinearEquiv.refl</span> <span class="pre">K</span> <span class="pre">V</span></code>.
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">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</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="bp">&#8810;&#8811;&#8343;</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">LinearEquiv.refl</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">LinearEquiv.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">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">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="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">V</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="bp">.</span><span class="n">ofBijective</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>Note that in the above example, Lean uses the announced type to understand that <code class="docutils literal notranslate"><span class="pre">.ofBijective</span></code>
refers to <code class="docutils literal notranslate"><span class="pre">LinearEquiv.ofBijective</span></code> (without needing to open any namespace).</p>
</section>
<section id="sums-and-products-of-vector-spaces">
<h3><span class="section-number">10.1.3. </span>Sums and products of vector spaces<a class="headerlink" href="#sums-and-products-of-vector-spaces" title="Link to this heading">&#61633;</a></h3>
<p>We can build new vector spaces out of old ones using direct sums and direct
products.
Let us start with two vectors spaces. In this case there is no difference between sum and product,
and we can simply use the product type.
In the following snippet of code we simply show how to get all the structure maps (inclusions
and projections) as linear maps, as well as the universal properties constructing linear maps
into products and out of sums (if you are not familiar with the category-theoretic distinction
between sums and products, you can simply ignore the universal property vocabulary and focus
on the types of the following examples).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">binary_product</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">W</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">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">]</span>
<span class="kd">variable</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="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">U</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">U</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">T</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">T</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">T</span><span class="o">]</span>

<span class="c1">-- First projection map</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.fst</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span>

<span class="c1">-- Second projection map</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.snd</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span>

<span class="c1">-- Universal property of the product</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">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</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">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w">  </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.prod</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- The product map does the expected thing, first component</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">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</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">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearMap.fst</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">LinearMap.prod</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">=</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">rfl</span>

<span class="c1">-- The product map does the expected thing, second component</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">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</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">U</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearMap.snd</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">LinearMap.prod</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>

<span class="c1">-- We can also combine maps in parallel</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</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">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</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="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</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="bp">&#215;</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">&#966;.prodMap</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- This is simply done by combining the projections with the universal property</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</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">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</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">&#966;.prodMap</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="bp">.</span><span class="n">fst</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="bp">.</span><span class="n">prod</span><span class="w"> </span><span class="o">(</span><span class="n">&#968;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="bp">.</span><span class="n">snd</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">rfl</span>

<span class="c1">-- First inclusion map</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.inl</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span>

<span class="c1">-- Second inclusion map</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">LinearMap.inr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span>

<span class="c1">-- Universal property of the sum (aka coproduct)</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</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">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</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="n">V</span><span class="w"> </span><span class="bp">&#215;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">&#966;.coprod</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- The coproduct map does the expected thing, first component</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</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">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</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="n">&#966;.coprod</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">LinearMap.inl</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">=</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">LinearMap.coprod_inl</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- The coproduct map does the expected thing, second component</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</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">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</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="n">&#966;.coprod</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">LinearMap.inr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">LinearMap.coprod_inr</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span>

<span class="c1">-- The coproduct map is defined in the expected way</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</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">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">w</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">&#966;.coprod</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="o">,</span><span class="w"> </span><span class="n">w</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="n">w</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">end</span><span class="w"> </span><span class="n">binary_product</span>
</pre></div>
</div>
<p>Let us now turn to sums and products of arbitrary families of vector spaces.
Here we will simply see how to define a family of vector spaces and access the universal
properties of sums and products.
Note that the direct sum notation is scoped to the <code class="docutils literal notranslate"><span class="pre">DirectSum</span></code> namespace, and
that the universal property of direct sums requires decidable equality on the
indexing type (this is somehow an implementation accident).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">families</span>
<span class="kn">open</span><span class="w"> </span><span class="n">DirectSum</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="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">DecidableEq</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">V</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="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</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="n">AddCommGroup</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)]</span><span class="w"> </span><span class="o">[</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="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)]</span>

<span class="c1">-- The universal property of the direct sum assembles maps from the summands to build</span>
<span class="c1">-- a map from the direct sum</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="bp">&#928;</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">V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#10753;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">DirectSum.toModule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="n">&#966;</span>

<span class="c1">-- The universal property of the direct product assembles maps into the factors</span>
<span class="c1">-- to build a map into the direct product</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="bp">&#928;</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">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</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">W</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</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">V</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">LinearMap.pi</span><span class="w"> </span><span class="n">&#966;</span>

<span class="c1">--&#8239;The projection maps from the product</span>
<span class="kd">example</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="o">(</span><span class="bp">&#928;</span><span class="w"> </span><span class="n">j</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">j</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</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">LinearMap.proj</span><span class="w"> </span><span class="n">i</span>

<span class="c1">-- The inclusion maps into the sum</span>
<span class="kd">example</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">V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="bp">&#10753;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</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">DirectSum.lof</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span>

<span class="c1">-- The inclusion maps into the product</span>
<span class="kd">example</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">V</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</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">V</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">LinearMap.single</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span>

<span class="c1">-- In case `&#953;` is a finite type, there is an isomorphism between the sum and product.</span>
<span class="kd">example</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="w"> </span><span class="o">(</span><span class="bp">&#10753;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</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">V</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">linearEquivFunOnFintype</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">V</span>

<span class="kd">end</span><span class="w"> </span><span class="n">families</span>
</pre></div>
</div>
</section>
</section>
<section id="subspaces-and-quotients">
<span id="index-2"></span><h2><span class="section-number">10.2. </span>Subspaces and quotients<a class="headerlink" href="#subspaces-and-quotients" title="Link to this heading">&#61633;</a></h2>
<section id="subspaces">
<h3><span class="section-number">10.2.1. </span>Subspaces<a class="headerlink" href="#subspaces" title="Link to this heading">&#61633;</a></h3>
<p>Just as linear maps are bundled, a linear subspace of <code class="docutils literal notranslate"><span class="pre">V</span></code> is also a bundled structure consisting of
a set in <code class="docutils literal notranslate"><span class="pre">V</span></code>, called the carrier of the subspace, with the relevant closure properties.
Again the word module appears instead of vector space because of the more general context that
Mathlib actually uses for linear algebra.</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">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">Field</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">V</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">V</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>

<span class="kd">example</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">V</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">U</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">U</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">U</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">U.add_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">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">V</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">U</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">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">a</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="bp">&#8712;</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">U.smul_mem</span><span class="w"> </span><span class="n">a</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">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code> is the type of <code class="docutils literal notranslate"><span class="pre">K</span></code>-linear
subspaces of <code class="docutils literal notranslate"><span class="pre">V</span></code>, rather than a predicate <code class="docutils literal notranslate"><span class="pre">IsSubmodule</span> <span class="pre">U</span></code> where <code class="docutils literal notranslate"><span class="pre">U</span></code> is an element of <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">V</span></code>.
<code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code> is endowed with a coercion to <code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">V</span></code> and a membership predicate on <code class="docutils literal notranslate"><span class="pre">V</span></code>.
See <a class="reference internal" href="C08_Hierarchies.html#section-hierarchies-subobjects"><span class="std std-numref">Section 8.3</span></a> for an explanation of how and why this is done.</p>
<p>Of course, two subspaces 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 subspaces 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">&#8477;</span></code> is a <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>-linear subspace of <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>,
what we really want is to construct a term of type <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">&#8477;</span> <span class="pre">&#8450;</span></code> whose projection to
<code class="docutils literal notranslate"><span class="pre">Set</span> <span class="pre">&#8450;</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>, or, more precisely, the image of <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> in <code class="docutils literal notranslate"><span class="pre">&#8450;</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="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">&#8450;</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">&#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="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">smul_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">c</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">a</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">c</span><span class="bp">*</span><span class="n">a</span>
<span class="w">    </span><span class="n">simp</span>
</pre></div>
</div>
<p>The prime at the end of proof fields in <code class="docutils literal notranslate"><span class="pre">Submodule</span></code> are analogous to the one in <code class="docutils literal notranslate"><span class="pre">LinearMap</span></code>.
Those fields are stated in terms of the <code class="docutils literal notranslate"><span class="pre">carrier</span></code> field because they are defined before the
<code class="docutils literal notranslate"><span class="pre">MemberShip</span></code> instance.&#8239;They are then superseded by <code class="docutils literal notranslate"><span class="pre">Submodule.add_mem</span></code>, <code class="docutils literal notranslate"><span class="pre">Submodule.zero_mem</span></code>
and <code class="docutils literal notranslate"><span class="pre">Submodule.smul_mem</span></code> that we saw above.</p>
<p>As an exercise in manipulating subspaces and linear maps, you will define the pre-image of
a subspace by a linear map (of course we will see below that Mathlib already knows about this).
Remember that <code class="docutils literal notranslate"><span class="pre">Set.mem_preimage</span></code> can be used to rewrite a statement involving
membership and preimage. This is the only lemma you will need in addition to the lemmas
discussed above about <code class="docutils literal notranslate"><span class="pre">LinearMap</span></code> and <code class="docutils literal notranslate"><span class="pre">Submodule</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">preimage</span><span class="w"> </span><span class="o">{</span><span class="n">W</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">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">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="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">&#966;</span><span class="w"> </span><span class="bp">&#8315;&#185;&#39;</span><span class="w"> </span><span class="n">H</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="gr">sorry</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="gr">sorry</span>
<span class="w">  </span><span class="n">smul_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="gr">sorry</span>
</pre></div>
</div>
<p>Using type classes, Mathlib knows that a subspace of a vector space inherits a vector space 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">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">U</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">U</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">V</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">U</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">K</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">V</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">U</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>
</section>
<section id="complete-lattice-structure-and-internal-direct-sums">
<h3><span class="section-number">10.2.2. </span>Complete lattice structure and internal direct sums<a class="headerlink" href="#complete-lattice-structure-and-internal-direct-sums" title="Link to this heading">&#61633;</a></h3>
<p>An important benefit of having a type <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code> instead of a predicate
<code class="docutils literal notranslate"><span class="pre">IsSubmodule</span> <span class="pre">:</span> <span class="pre">Set</span> <span class="pre">V</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">Submodule</span> <span class="pre">K</span> <span class="pre">V</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 subspaces of <code class="docutils literal notranslate"><span class="pre">V</span></code> is again a subspace, we
use 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 subspaces 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">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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">V</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">V</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">V</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 subspaces is not, in general, a subspace.
Instead one needs to use the subspace generated by the union, which is done
using <code class="docutils literal notranslate"><span class="pre">Submodule.span</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">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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">V</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</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">V</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">V</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><span class="w"> </span><span class="o">[</span><span class="n">Submodule.span_union</span><span class="o">]</span>
</pre></div>
</div>
<p>Another subtlety is that <code class="docutils literal notranslate"><span class="pre">V</span></code> itself does not have type <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code>,
so we need a way to talk about <code class="docutils literal notranslate"><span class="pre">V</span></code> seen as a subspace of <code class="docutils literal notranslate"><span class="pre">V</span></code>.
This is also provided by the lattice structure: the full subspace 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">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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 subspace whose only element is the
zero 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">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Submodule.mem_bot</span><span class="w"> </span><span class="n">K</span>
</pre></div>
</div>
<p>In particular we can discuss the case of subspaces that are in (internal) direct sum.
In the case of two subspaces, we use the general purpose predicate <code class="docutils literal notranslate"><span class="pre">IsCompl</span></code>
which makes sense for any bounded partially ordered type.
In the case of general families of subspaces we use <code class="docutils literal notranslate"><span class="pre">DirectSum.IsInternal</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c1">-- If two subspaces are in direct sum then they span the whole space.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">IsCompl</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">  </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">V</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">h.sup_eq_top</span>

<span class="c1">-- If two subspaces are in direct sum then they intersect only at zero.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">U</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">IsCompl</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">  </span><span class="n">U</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">V</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="n">h.inf_eq_bot</span>

<span class="kn">section</span>
<span class="kn">open</span><span class="w"> </span><span class="n">DirectSum</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="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">DecidableEq</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span>

<span class="c1">-- If subspaces are in direct sum then they span the whole space.</span>
<span class="kd">example</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">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">DirectSum.IsInternal</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="bp">&#10758;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">i</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">h.submodule_iSup_eq_top</span>

<span class="c1">-- If subspaces are in direct sum then they pairwise intersect only at zero.</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">DecidableEq</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">U</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">DirectSum.IsInternal</span><span class="w"> </span><span class="n">U</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">&#953;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hij</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">&#8800;</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">U</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">U</span><span class="w"> </span><span class="n">j</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="o">(</span><span class="n">h.submodule_iSupIndep.pairwiseDisjoint</span><span class="w"> </span><span class="n">hij</span><span class="o">)</span><span class="bp">.</span><span class="n">eq_bot</span>

<span class="c1">-- Those conditions characterize direct sums.</span>
<span class="k">#check</span><span class="w"> </span><span class="n">DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top</span>

<span class="c1">-- The relation with external direct sums: if a family of subspaces is</span>
<span class="c1">-- in internal direct sum then the map from their external direct sum into `V`</span>
<span class="c1">-- is a linear isomorphism.</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">&#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">DecidableEq</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">U</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">DirectSum.IsInternal</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="o">(</span><span class="bp">&#10753;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="n">U</span><span class="w"> </span><span class="n">i</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">LinearEquiv.ofBijective</span><span class="w"> </span><span class="o">(</span><span class="n">coeLinearMap</span><span class="w"> </span><span class="n">U</span><span class="o">)</span><span class="w"> </span><span class="n">h</span>
<span class="kd">end</span>
</pre></div>
</div>
</section>
<section id="subspace-spanned-by-a-set">
<h3><span class="section-number">10.2.3. </span>Subspace spanned by a set<a class="headerlink" href="#subspace-spanned-by-a-set" title="Link to this heading">&#61633;</a></h3>
<p>In addition to building subspaces out of existing subspaces, we can build them out
of any set <code class="docutils literal notranslate"><span class="pre">s</span></code> using <code class="docutils literal notranslate"><span class="pre">Submodule.span</span> <span class="pre">K</span> <span class="pre">s</span></code> which builds the smallest subspace
containing <code class="docutils literal notranslate"><span class="pre">s</span></code>.
On paper it is common to use that this space is made of all linear combinations of elements of
<code class="docutils literal notranslate"><span class="pre">s</span></code>.
But it is often more efficient to use its universal property expressed by <code class="docutils literal notranslate"><span class="pre">Submodule.span_le</span></code>,
and the whole theory of Galois connections.</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">s</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">V</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</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">E</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="bp">&#8838;</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">Submodule.span_le</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">GaloisInsertion</span><span class="w"> </span><span class="o">(</span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</span><span class="o">)</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Submodule.gi</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span>
</pre></div>
</div>
<p>When those are not enough, one can use the relevant induction principle
<code class="docutils literal notranslate"><span class="pre">Submodule.span_induction</span></code> which ensures a property holds for every element of the
span of <code class="docutils literal notranslate"><span class="pre">s</span></code> as long as it holds on <code class="docutils literal notranslate"><span class="pre">zero</span></code> and elements of <code class="docutils literal notranslate"><span class="pre">s</span></code> and is stable under
sum and scalar multiplication.</p>
<p>As an exercise, let us reprove one implication of <code class="docutils literal notranslate"><span class="pre">Submodule.mem_sup</span></code>.
Remember that you can use the <cite>module</cite> tactic to close goals that follow from
the axioms relating the various algebraic operations on <code class="docutils literal notranslate"><span class="pre">V</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">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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">V</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">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">S</span><span class="w"> </span><span class="bp">&#8852;</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="bp">&#8707;</span><span class="w"> </span><span class="n">s</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="bp">&#8707;</span><span class="w"> </span><span class="n">t</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">T</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">s</span><span class="w"> </span><span class="bp">+</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="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">S.span_eq</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">T.span_eq</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">Submodule.span_union</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">induction</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">Submodule.span_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">mem</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">hx</span><span class="w"> </span><span class="n">hy</span><span class="w"> </span><span class="n">hx&#39;</span><span class="w"> </span><span class="n">hy&#39;</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">  </span><span class="bp">|</span><span class="w"> </span><span class="n">smul</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">hx</span><span class="w"> </span><span class="n">hx&#39;</span><span class="w"> </span><span class="bp">=&gt;</span>
<span class="w">      </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="pushing-and-pulling-subspaces">
<h3><span class="section-number">10.2.4. </span>Pushing and pulling subspaces<a class="headerlink" href="#pushing-and-pulling-subspaces" title="Link to this heading">&#61633;</a></h3>
<p>As promised earlier, we now describe how to push and pull subspaces by linear maps.
As usual in Mathlib, the first operation is called <code class="docutils literal notranslate"><span class="pre">map</span></code> and the second one is called
<code class="docutils literal notranslate"><span class="pre">comap</span></code>.</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">W</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">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="k">in</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Submodule.map</span><span class="w"> </span><span class="n">&#966;</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="kd">variable</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="k">in</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Submodule.comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
</pre></div>
</div>
<p>Note those live in the <code class="docutils literal notranslate"><span class="pre">Submodule</span></code> namespace so one can use dot notation and write
<code class="docutils literal notranslate"><span class="pre">E.map</span> <span class="pre">&#966;</span></code> instead of <code class="docutils literal notranslate"><span class="pre">Submodule.map</span> <span class="pre">&#966;</span> <span class="pre">E</span></code>, but this is pretty awkward to read (although some
Mathlib contributors use this spelling).</p>
<p>In particular the range and kernel of a linear map are subspaces. Those special cases are important
enough to get declarations.</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">LinearMap.range</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">.</span><span class="n">map</span><span class="w"> </span><span class="n">&#966;</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">LinearMap.range_eq_map</span><span class="w"> </span><span class="n">&#966;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearMap.ker</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">.</span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Submodule.comap_bot</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="c1">-- or `rfl`</span>
</pre></div>
</div>
<p>Note that we cannot write <code class="docutils literal notranslate"><span class="pre">&#966;.ker</span></code> instead of <code class="docutils literal notranslate"><span class="pre">LinearMap.ker</span> <span class="pre">&#966;</span></code> because <code class="docutils literal notranslate"><span class="pre">LinearMap.ker</span></code> also
applies to classes of maps preserving more structure, hence it does not expect an argument
whose type starts with <code class="docutils literal notranslate"><span class="pre">LinearMap</span></code>, hence dot notation doesn&#8217;t work here.
However we were able to use the other flavor of dot notation in the right-hand side. Because
Lean expects a term with type <code class="docutils literal notranslate"><span class="pre">Submodule</span> <span class="pre">K</span> <span class="pre">V</span></code> after elaborating the left-hand side, it interprets
<code class="docutils literal notranslate"><span class="pre">.comap</span></code> as <code class="docutils literal notranslate"><span class="pre">Submodule.comap</span></code>.</p>
<p>The following lemmas give the key relations between those submodule and the properties of <code class="docutils literal notranslate"><span class="pre">&#966;</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">Function</span><span class="w"> </span><span class="n">LinearMap</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Injective</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="n">&#966;</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="n">ker_eq_bot.symm</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Surjective</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">&#966;</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">range_eq_top.symm</span>
</pre></div>
</div>
<p>As an exercise, let us prove the Galois connection property for <code class="docutils literal notranslate"><span class="pre">map</span></code> and <code class="docutils literal notranslate"><span class="pre">comap</span></code>.
One can use the following lemmas but this is not required since they are true by definition.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Submodule.mem_map_of_mem</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.mem_map</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.mem_comap</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Submodule.map</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</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">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">Submodule.comap</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">F</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="quotient-spaces">
<h3><span class="section-number">10.2.5. </span>Quotient spaces<a class="headerlink" href="#quotient-spaces" title="Link to this heading">&#61633;</a></h3>
<p>Quotient vector spaces use the general quotient notation (typed with <code class="docutils literal notranslate"><span class="pre">\quot</span></code>, not the ordinary
<code class="docutils literal notranslate"><span class="pre">/</span></code>).
The projection onto a quotient space is <code class="docutils literal notranslate"><span class="pre">Submodule.mkQ</span></code> and the universal property is
<code class="docutils literal notranslate"><span class="pre">Submodule.liftQ</span></code>.</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">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">E</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="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</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">E.mkQ</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="n">E.mkQ</span><span class="w"> </span><span class="bp">=</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">E.ker_mkQ</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">range</span><span class="w"> </span><span class="n">E.mkQ</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">E.range_mkQ</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">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">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">E.liftQ</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">h&#966;</span>

<span class="kd">example</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">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">.</span><span class="n">comap</span><span class="w"> </span><span class="n">&#966;</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">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</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="o">:=</span><span class="w"> </span><span class="n">E.mapQ</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">h&#966;</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="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">LinearMap.ker</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">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">&#966;.quotKerEquivRange</span>
</pre></div>
</div>
<p>As an exercise, let us prove the correspondence theorem for subspaces of quotient spaces.
Mathlib knows a slightly more precise version as <code class="docutils literal notranslate"><span class="pre">Submodule.comapMkQRelIso</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">Submodule</span>

<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.map_comap_eq</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.comap_map_eq</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#10744;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;</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="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">}</span><span class="w"> </span><span class="n">where</span>
<span class="w">  </span><span class="n">toFun</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">invFun</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">left_inv</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">right_inv</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="endomorphisms">
<h2><span class="section-number">10.3. </span>Endomorphisms<a class="headerlink" href="#endomorphisms" title="Link to this heading">&#61633;</a></h2>
<p>An important special case of linear maps are endomorphisms: linear maps from a vector space to itself.
They are interesting because they form a <code class="docutils literal notranslate"><span class="pre">K</span></code>-algebra. In particular we can evaluate polynomials
with coefficients in <code class="docutils literal notranslate"><span class="pre">K</span></code> on them, and they can have eigenvalues and eigenvectors.</p>
<p>Mathlib uses the abbreviation <code class="docutils literal notranslate"><span class="pre">Module.End</span> <span class="pre">K</span> <span class="pre">V</span> <span class="pre">:=</span> <span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">V</span></code> which is convenient when
using a lot of these (especially after opening the <code class="docutils literal notranslate"><span class="pre">Module</span></code> namespace).</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">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">Field</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">V</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">V</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">W</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">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</span><span class="o">]</span>


<span class="kn">open</span><span class="w"> </span><span class="n">Polynomial</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">LinearMap</span><span class="w"> </span><span class="n">End</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="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="bp">&#8728;&#8343;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">End.mul_eq_comp</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="c1">-- `rfl` would also work</span>

<span class="c1">-- evaluating `P` on `&#966;`</span>
<span class="kd">example</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">K</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">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</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">&#966;</span><span class="w"> </span><span class="n">P</span>

<span class="c1">-- evaluating `X` on `&#966;` gives back `&#966;`</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">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</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">&#966;</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">K</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="n">&#966;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">aeval_X</span><span class="w"> </span><span class="n">&#966;</span>
</pre></div>
</div>
<p>As an exercise manipulating endomorphisms, subspaces and polynomials, let us prove the
(binary) kernels lemma: for any endomorphism <span class="math notranslate nohighlight">\(&#966;\)</span> and any two relatively
prime polynomials <span class="math notranslate nohighlight">\(P\)</span> and <span class="math notranslate nohighlight">\(Q\)</span>, we have <span class="math notranslate nohighlight">\(\ker P(&#966;) &#8853; \ker Q(&#966;) = \ker \big(PQ(&#966;)\big)\)</span>.</p>
<p>Note that <code class="docutils literal notranslate"><span class="pre">IsCoprime</span> <span class="pre">x</span> <span class="pre">y</span></code> is defined as <code class="docutils literal notranslate"><span class="pre">&#8707;</span> <span class="pre">a</span> <span class="pre">b,</span> <span class="pre">a</span> <span class="pre">*</span> <span class="pre">x</span> <span class="pre">+</span> <span class="pre">b</span> <span class="pre">*</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">1</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">Submodule.eq_bot_iff</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.mem_inf</span>
<span class="k">#check</span><span class="w"> </span><span class="n">LinearMap.mem_ker</span>

<span class="kd">example</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">K</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">h</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">P</span><span class="w"> </span><span class="n">Q</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">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">P</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</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="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>

<span class="k">#check</span><span class="w"> </span><span class="n">Submodule.add_mem_sup</span>
<span class="k">#check</span><span class="w"> </span><span class="n">map_mul</span>
<span class="k">#check</span><span class="w"> </span><span class="n">End.mul_apply</span>
<span class="k">#check</span><span class="w"> </span><span class="n">LinearMap.ker_le_ker_comp</span>

<span class="kd">example</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">K</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">h</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">P</span><span class="w"> </span><span class="n">Q</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">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">P</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</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">ker</span><span class="w"> </span><span class="o">(</span><span class="n">aeval</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">P</span><span class="bp">*</span><span class="n">Q</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 now move to the discussions of eigenspaces and eigenvalues. The eigenspace
associated to an endomorphism <span class="math notranslate nohighlight">\(&#966;\)</span> and a scalar <span class="math notranslate nohighlight">\(a\)</span> is the kernel of <span class="math notranslate nohighlight">\(&#966; - aId\)</span>.
Eigenspaces are defined for all values of <code class="docutils literal notranslate"><span class="pre">a</span></code>, although
they are interesting only when they are non-zero.
However an eigenvector is, by definition, a non-zero element of an eigenspace. The corresponding
predicate is <code class="docutils literal notranslate"><span class="pre">End.HasEigenvector</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">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.eigenspace</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">LinearMap.ker</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</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">&#8226;</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">End.eigenspace_def</span>
</pre></div>
</div>
<p>Then there is a predicate <code class="docutils literal notranslate"><span class="pre">End.HasEigenvalue</span></code> and the corresponding subtype <code class="docutils literal notranslate"><span class="pre">End.Eigenvalues</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">&#966;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.HasEigenvalue</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">&#966;.eigenspace</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="bp">&#8869;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Iff.rfl</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">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.HasEigenvalue</span><span class="w"> </span><span class="n">a</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">v</span><span class="o">,</span><span class="w"> </span><span class="n">&#966;.HasEigenvector</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">v</span><span class="w">  </span><span class="o">:=</span>
<span class="w">  </span><span class="o">&#10216;</span><span class="n">End.HasEigenvalue.exists_hasEigenvector</span><span class="o">,</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">_</span><span class="o">,</span><span class="w"> </span><span class="n">hv</span><span class="o">&#10217;</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">&#966;.hasEigenvalue_of_hasEigenvector</span><span class="w"> </span><span class="n">hv</span><span class="o">&#10217;</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">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.Eigenvalues</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="bp">//</span><span class="w"> </span><span class="n">&#966;.HasEigenvalue</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="n">rfl</span>

<span class="c1">-- Eigenvalue are roots of the minimal polynomial</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">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#966;.HasEigenvalue</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="o">(</span><span class="n">minpoly</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="bp">.</span><span class="n">IsRoot</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">&#966;.isRoot_of_hasEigenvalue</span>

<span class="c1">-- In finite dimension, the converse is also true (we will discuss dimension below)</span>
<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">K</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">&#966;.HasEigenvalue</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="o">(</span><span class="n">minpoly</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="bp">.</span><span class="n">IsRoot</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">&#966;.hasEigenvalue_iff_isRoot</span>

<span class="c1">--&#8239;Cayley-Hamilton</span>
<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</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">&#966;</span><span class="w"> </span><span class="n">&#966;.charpoly</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">&#966;.aeval_self_charpoly</span>
</pre></div>
</div>
</section>
<section id="matrices-bases-and-dimension">
<span id="matrices-bases-dimension"></span><h2><span class="section-number">10.4. </span>Matrices, bases and dimension<a class="headerlink" href="#matrices-bases-and-dimension" title="Link to this heading">&#61633;</a></h2>
<section id="matrices">
<span id="id2"></span><h3><span class="section-number">10.4.1. </span>Matrices<a class="headerlink" href="#matrices" title="Link to this heading">&#61633;</a></h3>
<p id="index-3">Before introducing bases for abstract vector spaces, we go back to the much more elementary setup
of linear algebra in <span class="math notranslate nohighlight">\(K^n\)</span> for some field <span class="math notranslate nohighlight">\(K\)</span>.
Here the main objects are vectors and matrices.
For concrete vectors, one can use the <code class="docutils literal notranslate"><span class="pre">![&#8230;]</span></code> notation, where components are separated by commas.
For concrete matrices we can use the <code class="docutils literal notranslate"><span class="pre">!![&#8230;]</span></code> notation, lines are separated by semi-colons
and components of lines are separated by colons.
When entries have a computable type such as <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> or <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>, we can use
the <code class="docutils literal notranslate"><span class="pre">eval</span></code> command to play with basic operations.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">matrices</span>

<span class="c1">-- Adding vectors</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!</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="bp">+</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w">  </span><span class="c1">-- ![4, 6]</span>

<span class="c1">-- Adding matrices</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</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="bp">;</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><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="bp">;</span><span class="w"> </span><span class="mi">5</span><span class="o">,</span><span class="w"> </span><span class="mi">6</span><span class="o">]</span><span class="w">  </span><span class="c1">-- !![4, 6; 8, 10]</span>

<span class="c1">-- Multiplying matrices</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</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="bp">;</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><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="bp">;</span><span class="w"> </span><span class="mi">5</span><span class="o">,</span><span class="w"> </span><span class="mi">6</span><span class="o">]</span><span class="w">  </span><span class="c1">-- !![13, 16; 29, 36]</span>
</pre></div>
</div>
<p>It is important to understand that this use of <code class="docutils literal notranslate"><span class="pre">#eval</span></code> is interesting only for
exploration, it is not meant to replace a computer algebra system such as Sage.
The data representation used here for matrices is <em>not</em> computationally
efficient in any way. It uses functions instead of arrays and is optimized for
proving, not computing.
The virtual machine used by <code class="docutils literal notranslate"><span class="pre">#eval</span></code> is also not optimized for this use.</p>
<p>Beware the matrix notation list rows but the vector notation
is neither a row vector nor a column vector. Multiplication of a matrix with a vector
from the left (resp. right) interprets the vector as a row (resp. column) vector.
This corresponds to operations
<code class="docutils literal notranslate"><span class="pre">Matrix.vecMul</span></code>, with notation <code class="docutils literal notranslate"><span class="pre">&#7525;*</span></code> and <code class="docutils literal notranslate"><span class="pre">Matrix.mulVec</span></code>, with notation ` <cite>*&#7525;`</cite>.
Those notations are scoped in the <code class="docutils literal notranslate"><span class="pre">Matrix</span></code> namespace that we therefore need to open.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Matrix</span>

<span class="c1">-- matrices acting on vectors on the left</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</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="bp">;</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><span class="w"> </span><span class="bp">*&#7525;</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w"> </span><span class="c1">-- ![3, 7]</span>

<span class="c1">-- matrices acting on vectors on the left, resulting in a size one matrix</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</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="bp">*&#7525;</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="o">]</span><span class="w">  </span><span class="c1">-- ![3]</span>

<span class="c1">-- matrices acting on vectors on the right</span>
<span class="k">#eval</span><span class="w">  </span><span class="bp">!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</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">&#7525;*</span><span class="w"> </span><span class="bp">!!</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="bp">;</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="bp">;</span><span class="w"> </span><span class="mi">5</span><span class="o">,</span><span class="w"> </span><span class="mi">6</span><span class="o">]</span><span class="w"> </span><span class="c1">-- ![9, 12]</span>
</pre></div>
</div>
<p>In order to generate matrices with identical rows or columns specified by a vector, we
use <code class="docutils literal notranslate"><span class="pre">Matrix.replicateRow</span></code> and <code class="docutils literal notranslate"><span class="pre">Matrix.replicateCol</span></code>, with arguments the type indexing the
rows or columns and the vector.
For instance one can get single row or single column matrixes (more precisely matrices whose rows
or columns are indexed by <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">1</span></code>).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#eval</span><span class="w"> </span><span class="n">replicateRow</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">!</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="c1">-- !![1, 2]</span>

<span class="k">#eval</span><span class="w"> </span><span class="n">replicateCol</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span><span class="w"> </span><span class="bp">!</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="c1">-- !![1; 2]</span>
</pre></div>
</div>
<p>Other familiar operations include the vector dot product, matrix transpose, and,
for square matrices, determinant and trace.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="c1">-- vector dot product</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!</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="bp">&#11037;&#7525;</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="mi">3</span><span class="o">,</span><span class="w"> </span><span class="mi">4</span><span class="o">]</span><span class="w"> </span><span class="c1">-- `11`</span>

<span class="c1">-- matrix transpose</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</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="bp">;</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><span class="bp">&#7488;</span><span class="w"> </span><span class="c1">-- `!![1, 3; 2, 4]`</span>

<span class="c1">-- determinant</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</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><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="c1">-- `-2`</span>

<span class="c1">-- trace</span>
<span class="k">#eval</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</span><span class="mi">1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">),</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</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><span class="bp">.</span><span class="n">trace</span><span class="w"> </span><span class="c1">-- `5`</span>
</pre></div>
</div>
<p>When entries do not have a computable type, for instance if they are real numbers, we cannot
hope that <code class="docutils literal notranslate"><span class="pre">#eval</span></code> can help. Also this kind of evaluation cannot be used in proofs without
considerably expanding the trusted code base (i.e. the part of Lean that you need to trust when
checking proofs).</p>
<p>So it is good to also use the <code class="docutils literal notranslate"><span class="pre">simp</span></code> and <code class="docutils literal notranslate"><span class="pre">norm_num</span></code> tactics in proofs, or
their command counter-part for quick exploration.</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="bp">!!</span><span class="o">[(</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="w"> </span><span class="mi">2</span><span class="bp">;</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><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="c1">-- `4 - 2*3`</span>

<span class="bp">#</span><span class="n">norm_num</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</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="w"> </span><span class="mi">2</span><span class="bp">;</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><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="c1">-- `-2`</span>

<span class="bp">#</span><span class="n">norm_num</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</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="w"> </span><span class="mi">2</span><span class="bp">;</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><span class="bp">.</span><span class="n">trace</span><span class="w"> </span><span class="c1">-- `5`</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="k">in</span>
<span class="bp">#</span><span class="n">simp</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">b</span><span class="bp">;</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">d</span><span class="o">]</span><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="c1">-- `a * d &#8211; b * c`</span>
</pre></div>
</div>
<p>The next important operation on square matrices is inversion.
In the same way as division of numbers is always defined and returns the artificial value
zero for division by zero, the inversion operation is defined on all matrices and returns
the zero matrix for non-invertible matrices.</p>
<p>More precisely, there is general function <code class="docutils literal notranslate"><span class="pre">Ring.inverse</span></code> that does this in any ring,
and, for any matrix <code class="docutils literal notranslate"><span class="pre">A</span></code>, <code class="docutils literal notranslate"><span class="pre">A&#8315;&#185;</span></code> is defined as <code class="docutils literal notranslate"><span class="pre">Ring.inverse</span> <span class="pre">A.det</span> <span class="pre">&#8226;</span> <span class="pre">A.adjugate</span></code>.
According to Cramer&#8217;s rule, this is indeed the inverse of <code class="docutils literal notranslate"><span class="pre">A</span></code> when the determinant of <code class="docutils literal notranslate"><span class="pre">A</span></code> is
not zero.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="bp">#</span><span class="n">norm_num</span><span class="w"> </span><span class="o">[</span><span class="n">Matrix.inv_def</span><span class="o">]</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</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="w"> </span><span class="mi">2</span><span class="bp">;</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><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="c1">-- !![-2, 1; 3 / 2, -(1 / 2)]</span>
</pre></div>
</div>
<p>Of course this definition is really useful only for invertible matrices.
There is a general type class <code class="docutils literal notranslate"><span class="pre">Invertible</span></code> that helps recording this.
For instance, the <code class="docutils literal notranslate"><span class="pre">simp</span></code> call in the next example will use the <code class="docutils literal notranslate"><span class="pre">inv_mul_of_invertible</span></code>
lemma which has an <code class="docutils literal notranslate"><span class="pre">Invertible</span></code> type-class assumption, so it will trigger
only if this can be found by the type-class synthesis system.
Here we make this fact available using a <code class="docutils literal notranslate"><span class="pre">have</span></code> 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="w"> </span><span class="bp">!!</span><span class="o">[(</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="w"> </span><span class="mi">2</span><span class="bp">;</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><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</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="w"> </span><span class="mi">2</span><span class="bp">;</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><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">have</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Invertible</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</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="w"> </span><span class="mi">2</span><span class="bp">;</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><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">Matrix.invertibleOfIsUnitDet</span>
<span class="w">    </span><span class="n">norm_num</span>
<span class="w">  </span><span class="n">simp</span>
</pre></div>
</div>
<p>In this fully concrete case, we could also use the <code class="docutils literal notranslate"><span class="pre">norm_num</span></code> machinery,
and <code class="docutils literal notranslate"><span class="pre">apply?</span></code> to find the final line:</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="bp">!!</span><span class="o">[(</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="w"> </span><span class="mi">2</span><span class="bp">;</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><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">!!</span><span class="o">[(</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="w"> </span><span class="mi">2</span><span class="bp">;</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><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">norm_num</span><span class="w"> </span><span class="o">[</span><span class="n">Matrix.inv_def</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">one_fin_two.symm</span>
</pre></div>
</div>
<p>All the concrete matrices above have their rows and columns indexed by <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">n</span></code> for
some <code class="docutils literal notranslate"><span class="pre">n</span></code> (not necessarily the same for rows and columns).
But sometimes it is more convenient to index matrices using arbitrary finite types.
For instance the adjacency matrix of a finite graph has rows and columns naturally indexed by
the vertices of the graph.</p>
<p>In fact when simply wants to define matrices without defining any operation on them,
finiteness of the indexing types are not even needed, and coefficients can have any type,
without any algebraic structure.
So Mathlib simply defines <code class="docutils literal notranslate"><span class="pre">Matrix</span> <span class="pre">m</span> <span class="pre">n</span> <span class="pre">&#945;</span></code> to be <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">&#8594;</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">&#945;</span></code> for any types <code class="docutils literal notranslate"><span class="pre">m</span></code>, <code class="docutils literal notranslate"><span class="pre">n</span></code> and <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>,
and the matrices we have been using so far had types such as <code class="docutils literal notranslate"><span class="pre">Matrix</span> <span class="pre">(Fin</span> <span class="pre">2)</span> <span class="pre">(Fin</span> <span class="pre">2)</span> <span class="pre">&#8477;</span></code>.
Of course algebraic operations require more assumptions on <code class="docutils literal notranslate"><span class="pre">m</span></code>, <code class="docutils literal notranslate"><span class="pre">n</span></code> and <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>.</p>
<p>Note the main reason why we do not use <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">&#8594;</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">&#945;</span></code> directly is to allow the type class
system to understand what we want. For instance, for a ring <code class="docutils literal notranslate"><span class="pre">R</span></code>, the type <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">R</span></code> is
endowed with the point-wise multiplication operation, and similarly <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">&#8594;</span> <span class="pre">n</span> <span class="pre">&#8594;</span> <span class="pre">R</span></code>
has this operation which is <em>not</em> the multiplication we want on matrices.</p>
<p>In the first example below, we force Lean to see through the definition of <code class="docutils literal notranslate"><span class="pre">Matrix</span></code>
and accept the statement as meaningful, and then prove it by checking all entries.</p>
<p>But then the next two examples reveal that Lean uses the point-wise multiplication
on <code class="docutils literal notranslate"><span class="pre">Fin</span> <span class="pre">2</span> <span class="pre">&#8594;</span> <span class="pre">Fin</span> <span class="pre">2</span> <span class="pre">&#8594;</span> <span class="pre">&#8484;</span></code> but the matrix multiplication on <code class="docutils literal notranslate"><span class="pre">Matrix</span> <span class="pre">(Fin</span> <span class="pre">2)</span> <span class="pre">(Fin</span> <span class="pre">2)</span> <span class="pre">&#8484;</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</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">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="bp">;</span><span class="w"> </span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</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">ext</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span>
<span class="w">  </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&lt;;&gt;</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="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</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">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</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">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Fin</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8484;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="bp">;</span><span class="w"> </span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</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">ext</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">j</span>
<span class="w">  </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="bp">&lt;;&gt;</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="w"> </span><span class="bp">!!</span><span class="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="bp">;</span><span class="w"> </span><span class="mi">1</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="o">[</span><span class="mi">1</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="bp">;</span><span class="w"> </span><span class="mi">1</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="o">[</span><span class="mi">2</span><span class="o">,</span><span class="w"> </span><span class="mi">2</span><span class="bp">;</span><span class="w"> </span><span class="mi">2</span><span class="o">,</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">norm_num</span>
</pre></div>
</div>
<p>In order to define matrices as functions without losing the benefits of <code class="docutils literal notranslate"><span class="pre">Matrix</span></code>
for type class synthesis, we can use the equivalence <code class="docutils literal notranslate"><span class="pre">Matrix.of</span></code> between functions
and matrices.&#8239;This equivalence is secretly defined using <code class="docutils literal notranslate"><span class="pre">Equiv.refl</span></code>.</p>
<p>For instance we can define Vandermonde matrices corresponding to a vector <code class="docutils literal notranslate"><span class="pre">v</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">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">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Fin</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">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Matrix.vandermonde</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Matrix.of</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </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">Fin</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">^</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">&#8469;</span><span class="o">))</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>
<span class="kd">end</span>
<span class="kd">end</span><span class="w"> </span><span class="n">matrices</span>
</pre></div>
</div>
</section>
<section id="bases">
<h3><span class="section-number">10.4.2. </span>Bases<a class="headerlink" href="#bases" title="Link to this heading">&#61633;</a></h3>
<p>We now want to discuss bases of vector spaces. Informally there are many ways to define this notion.
One can use a universal property.
One can say a basis is a family of vectors that is linearly independent and spanning.
Or one can combine those properties and directly say that a basis is a family of vectors
such that every vectors can be written uniquely as a linear combination of bases vectors.
Yet another way to say it is that a basis provides a linear isomorphism with a power of
the base field <code class="docutils literal notranslate"><span class="pre">K</span></code>, seen as a vector space over <code class="docutils literal notranslate"><span class="pre">K</span></code>.</p>
<p>This isomorphism version is actually the one that Mathlib uses as a definition under the hood, and
other characterizations are proven from it.
One must be slightly careful with the &#8220;power of <code class="docutils literal notranslate"><span class="pre">K</span></code>&#8221; idea in the case of infinite bases.
Indeed only finite linear combinations make sense in this algebraic context. So what we need
as a reference vector space is not a direct product of copies of <code class="docutils literal notranslate"><span class="pre">K</span></code> but a direct sum.
We could use <code class="docutils literal notranslate"><span class="pre">&#10753;</span> <span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#953;,</span> <span class="pre">K</span></code> for some type <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> indexing the basis
But we rather use the more specialized spelling <code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;&#8320;</span> <span class="pre">K</span></code> which means
&#8220;functions from <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> to <code class="docutils literal notranslate"><span class="pre">K</span></code> with finite support&#8221;, i.e. functions which vanish outside a finite set
in <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> (this finite set is not fixed, it depends on the function).
Evaluating such a function coming from a basis <code class="docutils literal notranslate"><span class="pre">B</span></code> at a vector <code class="docutils literal notranslate"><span class="pre">v</span></code> and
<code class="docutils literal notranslate"><span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#953;</span></code> returns the component (or coordinate) of <code class="docutils literal notranslate"><span class="pre">v</span></code> on the <code class="docutils literal notranslate"><span class="pre">i</span></code>-th basis vector.</p>
<p>The type of bases indexed by a type <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> of <code class="docutils literal notranslate"><span class="pre">V</span></code> as a <code class="docutils literal notranslate"><span class="pre">K</span></code> vector space is <code class="docutils literal notranslate"><span class="pre">Basis</span> <span class="pre">&#953;</span> <span class="pre">K</span> <span class="pre">V</span></code>.
The isomorphism is called <code class="docutils literal notranslate"><span class="pre">Basis.repr</span></code>.</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">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">Field</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">V</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">V</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>

<span class="kn">section</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="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">B</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</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="c1">-- The basis vector with index ``i``</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B</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">V</span><span class="o">)</span>

<span class="c1">-- the linear isomorphism with the model space given by ``B``</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;&#8320;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>

<span class="c1">-- the component function of ``v``</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</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;&#8320;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>

<span class="c1">-- the component of ``v`` with index ``i``</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</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">K</span><span class="o">)</span>
</pre></div>
</div>
<p>Instead of starting with such an isomorphism, one can start with a family <code class="docutils literal notranslate"><span class="pre">b</span></code> of vectors that is
linearly independent and spanning, this is <code class="docutils literal notranslate"><span class="pre">Basis.mk</span></code>.</p>
<p>The assumption that the family is spanning is spelled out as <code class="docutils literal notranslate"><span class="pre">&#8868;</span> <span class="pre">&#8804;</span> <span class="pre">Submodule.span</span> <span class="pre">K</span> <span class="pre">(Set.range</span> <span class="pre">b)</span></code>.
Here <code class="docutils literal notranslate"><span class="pre">&#8868;</span></code> is the top submodule of <code class="docutils literal notranslate"><span class="pre">V</span></code>, i.e. <code class="docutils literal notranslate"><span class="pre">V</span></code> seen as submodule of itself.
This spelling looks a bit tortuous, but we will see below that it is almost equivalent by definition
to the more readable <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">v,</span> <span class="pre">v</span> <span class="pre">&#8712;</span> <span class="pre">Submodule.span</span> <span class="pre">K</span> <span class="pre">(Set.range</span> <span class="pre">b)</span></code> (the underscores in the snippet
below refers to the useless information <code class="docutils literal notranslate"><span class="pre">v</span> <span class="pre">&#8712;</span> <span class="pre">&#8868;</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="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">b</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">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">b_indep</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearIndependent</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">b_spans</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">v</span><span class="o">,</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">Set.range</span><span class="w"> </span><span class="n">b</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Basis.mk</span><span class="w"> </span><span class="n">b_indep</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">b_spans</span><span class="w"> </span><span class="n">v</span><span class="o">)</span>

<span class="c1">-- The family of vectors underlying the above basis is indeed ``b``.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">b</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">V</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">b_indep</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">LinearIndependent</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">b_spans</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">v</span><span class="o">,</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">Submodule.span</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">Set.range</span><span class="w"> </span><span class="n">b</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">Basis.mk</span><span class="w"> </span><span class="n">b_indep</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">b_spans</span><span class="w"> </span><span class="n">v</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">b</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">Basis.mk_apply</span><span class="w"> </span><span class="n">b_indep</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">b_spans</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="n">i</span>
</pre></div>
</div>
<p>In particular the model vector space <code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;&#8320;</span> <span class="pre">K</span></code> has a so-called canonical basis whose <code class="docutils literal notranslate"><span class="pre">repr</span></code>
function evaluated on any vector is the identity isomorphism. It is called
<code class="docutils literal notranslate"><span class="pre">Finsupp.basisSingleOne</span></code> where <code class="docutils literal notranslate"><span class="pre">Finsupp</span></code> means function with finite support and
<code class="docutils literal notranslate"><span class="pre">basisSingleOne</span></code> refers to the fact that basis vectors are functions which
vanish expect for a single input value. More precisely the basis vector indexed by <code class="docutils literal notranslate"><span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#953;</span></code>
is <code class="docutils literal notranslate"><span class="pre">Finsupp.single</span> <span class="pre">i</span> <span class="pre">1</span></code> which is the finitely supported function taking value <code class="docutils literal notranslate"><span class="pre">1</span></code> at <code class="docutils literal notranslate"><span class="pre">i</span></code>
and <code class="docutils literal notranslate"><span class="pre">0</span></code> everywhere else.</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">DecidableEq</span><span class="w"> </span><span class="n">&#953;</span><span class="o">]</span>
</pre></div>
</div>
<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">Finsupp.basisSingleOne.repr</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">LinearEquiv.refl</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;&#8320;</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">rfl</span>

<span class="kd">example</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">Finsupp.basisSingleOne</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">Finsupp.single</span><span class="w"> </span><span class="n">i</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">rfl</span>
</pre></div>
</div>
<p>The story of finitely supported functions is unneeded when the indexing type is finite.
In this case we can use the simpler <code class="docutils literal notranslate"><span class="pre">Pi.basisFun</span></code> which gives a basis of the whole
<code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;</span> <span class="pre">K</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">Finite</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">x</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">K</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="o">(</span><span class="k">Pi</span><span class="bp">.</span><span class="n">basisFun</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="bp">.</span><span class="n">repr</span><span class="w"> </span><span class="n">x</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">x</span><span class="w"> </span><span class="n">i</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>Going back to the general case of bases of abstract vector spaces, we can express
any vector as a linear combination of basis vectors.
Let us first see the easy case of finite bases.</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">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="w"> </span><span class="bp">&#8721;</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="o">,</span><span class="w"> </span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="o">(</span><span class="n">B</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="n">v</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">B.sum_repr</span><span class="w"> </span><span class="n">v</span>
</pre></div>
</div>
<p>When <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> is not finite, the above statement makes no sense a priori: we cannot take a sum over <code class="docutils literal notranslate"><span class="pre">&#953;</span></code>.
However the support of the function being summed is finite (it is the support of <code class="docutils literal notranslate"><span class="pre">B.repr</span> <span class="pre">v</span></code>).
But we need to apply a construction that takes this into account.
Here Mathlib uses a special purpose function that requires some time to get used to:
<code class="docutils literal notranslate"><span class="pre">Finsupp.linearCombination</span></code> (which is built on top of the more general <code class="docutils literal notranslate"><span class="pre">Finsupp.sum</span></code>).
Given a finitely supported function <code class="docutils literal notranslate"><span class="pre">c</span></code> from a type <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> to the base field <code class="docutils literal notranslate"><span class="pre">K</span></code> and any
function <code class="docutils literal notranslate"><span class="pre">f</span></code> from <code class="docutils literal notranslate"><span class="pre">&#953;</span></code> to <code class="docutils literal notranslate"><span class="pre">V</span></code>, <code class="docutils literal notranslate"><span class="pre">Finsupp.linearCombination</span> <span class="pre">K</span> <span class="pre">f</span> <span class="pre">c</span></code> is the
sum over the support of <code class="docutils literal notranslate"><span class="pre">c</span></code> of the scalar multiplication <code class="docutils literal notranslate"><span class="pre">c</span> <span class="pre">&#8226;</span> <span class="pre">f</span></code>. In
particular, we can replace it by a sum over any finite set containing the
support of <code class="docutils literal notranslate"><span class="pre">c</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">c</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;&#8320;</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">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">V</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">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c.support</span><span class="w"> </span><span class="bp">&#8838;</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">Finsupp.linearCombination</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8721;</span><span class="w"> </span><span class="n">i</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">c</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8226;</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">Finsupp.linearCombination_apply_of_mem_supported</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>One could also assume that <code class="docutils literal notranslate"><span class="pre">f</span></code> is finitely supported and still get a well defined sum.
But the choice made by <code class="docutils literal notranslate"><span class="pre">Finsupp.linearCombination</span></code> is the one relevant to our basis discussion since it allows
to state the generalization of <code class="docutils literal notranslate"><span class="pre">Basis.sum_repr</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">Finsupp.linearCombination</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">B.linearCombination_repr</span><span class="w"> </span><span class="n">v</span>
</pre></div>
</div>
<p>One could wonder why <code class="docutils literal notranslate"><span class="pre">K</span></code> is an explicit argument here, despite the fact it can be inferred from
the type of <code class="docutils literal notranslate"><span class="pre">c</span></code>. The point is that the partially applied <code class="docutils literal notranslate"><span class="pre">Finsupp.linearCombination</span> <span class="pre">K</span> <span class="pre">f</span></code>
is interesting in itself. It is not a bare function from <code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;&#8320;</span> <span class="pre">K</span></code> to <code class="docutils literal notranslate"><span class="pre">V</span></code> but a
<code class="docutils literal notranslate"><span class="pre">K</span></code>-linear map.</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">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">V</span><span class="o">)</span><span class="w"> </span><span class="k">in</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Finsupp.linearCombination</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;&#8320;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
</pre></div>
</div>
<p>Returning to the mathematical discussion, it is important to understand that the
representation of vectors in a basis is less useful in formalized
mathematics than you may think.
Indeed it is very often more efficient to directly use more abstract properties of bases.
In particular the universal property of bases connecting them to other free objects in algebra
allows to construct linear maps by specifying the images of basis vectors.
This is <code class="docutils literal notranslate"><span class="pre">Basis.constr</span></code>. For any <code class="docutils literal notranslate"><span class="pre">K</span></code>-vector space <code class="docutils literal notranslate"><span class="pre">W</span></code>, our basis <code class="docutils literal notranslate"><span class="pre">B</span></code>
gives a linear isomorphism <code class="docutils literal notranslate"><span class="pre">Basis.constr</span> <span class="pre">B</span> <span class="pre">K</span></code> from <code class="docutils literal notranslate"><span class="pre">&#953;</span> <span class="pre">&#8594;</span> <span class="pre">W</span></code> to <code class="docutils literal notranslate"><span class="pre">V</span> <span class="pre">&#8594;&#8343;[K]</span> <span class="pre">W</span></code>.
This isomorphism is characterized by the fact that it sends any function <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">:</span> <span class="pre">&#953;</span> <span class="pre">&#8594;</span> <span class="pre">W</span></code>
to a linear map sending the basis vector <code class="docutils literal notranslate"><span class="pre">B</span> <span class="pre">i</span></code> to <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">i</span></code>, for every <code class="docutils literal notranslate"><span class="pre">i</span> <span class="pre">:</span> <span class="pre">&#953;</span></code>.</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">W</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">W</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">Module</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</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">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.constr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">))</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">B.constr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span>

<span class="kd">example</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">B.constr</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="o">(</span><span class="n">B</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="n">u</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">B.constr_basis</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">i</span>
</pre></div>
</div>
<p>This property is indeed characteristic because linear maps are determined by their values
on bases:</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">&#966;</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">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="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="n">&#966;</span><span class="w"> </span><span class="o">(</span><span class="n">B</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="n">&#968;</span><span class="w"> </span><span class="o">(</span><span class="n">B</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">&#966;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">&#968;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">B.ext</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>If we also have a basis <code class="docutils literal notranslate"><span class="pre">B'</span></code> on the target space then we can identify linear maps
with matrices. This identification is a <code class="docutils literal notranslate"><span class="pre">K</span></code>-linear 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">&#953;&#39;</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">B&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</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">DecidableEq</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">Fintype</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="o">]</span>

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

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8771;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">Matrix</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="o">)</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Matrix</span><span class="w"> </span><span class="c1">-- get access to the ``*&#7525;`` notation for multiplication between matrices and vectors.</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">v</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="bp">*&#7525;</span><span class="w"> </span><span class="o">(</span><span class="n">B.repr</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">B&#39;.repr</span><span class="w"> </span><span class="o">(</span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">toMatrix_mulVec_repr</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="w"> </span><span class="n">v</span>


<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;&#39;&#39;</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">B&#39;&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;&#39;&#39;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">W</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;&#39;&#39;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">DecidableEq</span><span class="w"> </span><span class="n">&#953;&#39;&#39;</span><span class="o">]</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">V</span><span class="w"> </span><span class="bp">&#8594;&#8343;</span><span class="o">[</span><span class="n">K</span><span class="o">]</span><span class="w"> </span><span class="n">W</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">B&#39;&#39;</span><span class="w"> </span><span class="bp">.</span><span class="n">id</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</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="n">simp</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>As an exercise on this topic, we will prove part of the theorem which guarantees that
endomorphisms have a well-defined determinant.
Namely we want to prove that when two bases are indexed by the same type, the matrices
they attach to any endomorphism have the same determinant.
This would then need to be complemented using that bases all have isomorphic indexing types to
get the full result.</p>
<p>Of course Mathlib already knows this, and <code class="docutils literal notranslate"><span class="pre">simp</span></code> can close the goal immediately, so you
shouldn&#8217;t use it too soon, but rather use the provided lemmas.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Module</span><span class="w"> </span><span class="n">LinearMap</span><span class="w"> </span><span class="n">Matrix</span>

<span class="c1">-- Some lemmas coming from the fact that `LinearMap.toMatrix` is an algebra morphism.</span>
<span class="k">#check</span><span class="w"> </span><span class="n">toMatrix_comp</span>
<span class="k">#check</span><span class="w"> </span><span class="n">id_comp</span>
<span class="k">#check</span><span class="w"> </span><span class="n">comp_id</span>
<span class="k">#check</span><span class="w"> </span><span class="n">toMatrix_id</span>

<span class="c1">-- Some lemmas coming from the fact that ``Matrix.det`` is a multiplicative monoid morphism.</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Matrix.det_mul</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Matrix.det_one</span>

<span class="kd">example</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">B&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">End</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="bp">.</span><span class="n">det</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">&#966;</span><span class="o">)</span><span class="bp">.</span><span class="n">det</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">set</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">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">&#966;</span>
<span class="w">  </span><span class="n">set</span><span class="w"> </span><span class="n">M&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">&#966;</span>
<span class="w">  </span><span class="n">set</span><span class="w"> </span><span class="n">P</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span><span class="o">)</span><span class="w"> </span><span class="n">LinearMap.id</span>
<span class="w">  </span><span class="n">set</span><span class="w"> </span><span class="n">P&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="o">(</span><span class="n">toMatrix</span><span class="w"> </span><span class="n">B&#39;</span><span class="w"> </span><span class="n">B</span><span class="o">)</span><span class="w"> </span><span class="n">LinearMap.id</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">end</span>
</pre></div>
</div>
</section>
<section id="dimension">
<h3><span class="section-number">10.4.3. </span>Dimension<a class="headerlink" href="#dimension" title="Link to this heading">&#61633;</a></h3>
<p>Returning to the case of a single vector space, bases are also useful to define the concept of
dimension.
Here again, there is the elementary case of finite-dimensional vector spaces.
For such spaces we expect a dimension which is a natural number.
This is <code class="docutils literal notranslate"><span class="pre">Module.finrank</span></code>. It takes the base field as an explicit argument
since a given abelian group can be a vector space over different fields.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span>

<span class="c1">-- `Fin n &#8594; K` is the archetypical space with dimension `n` over `K`.</span>
<span class="kd">example</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="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">Fin</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">K</span><span class="o">)</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">Module.finrank_fin_fun</span><span class="w"> </span><span class="n">K</span>

<span class="c1">-- Seen as a vector space over itself, `&#8450;` has dimension one.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">&#8450;</span><span class="w"> </span><span class="n">&#8450;</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">Module.finrank_self</span><span class="w"> </span><span class="n">&#8450;</span>

<span class="c1">-- But as a real vector space it has dimension two.</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">&#8450;</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="n">Complex.finrank_real_complex</span>
</pre></div>
</div>
<p>Note that <code class="docutils literal notranslate"><span class="pre">Module.finrank</span></code> is defined for any vector space. It returns
zero for infinite dimensional vector spaces, just as division by zero returns zero.</p>
<p>Of course many lemmas require a finite dimension assumption. This is the role of
the <code class="docutils literal notranslate"><span class="pre">FiniteDimensional</span></code> typeclass. For instance, think about how the next
example fails without this assumption.</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">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">Nontrivial</span><span class="w"> </span><span class="n">V</span><span class="w">  </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Module.finrank_pos_iff</span>
</pre></div>
</div>
<p>In the above statement, <code class="docutils literal notranslate"><span class="pre">Nontrivial</span> <span class="pre">V</span></code> means <code class="docutils literal notranslate"><span class="pre">V</span></code> has at least two different elements.
Note that <code class="docutils literal notranslate"><span class="pre">Module.finrank_pos_iff</span></code> has no explicit argument.
This is fine when using it from left to right, but not when using it from right to left
because Lean has no way to guess <code class="docutils literal notranslate"><span class="pre">K</span></code> from the statement <code class="docutils literal notranslate"><span class="pre">Nontrivial</span> <span class="pre">V</span></code>.
In that case it is useful to use the name argument syntax, after checking that the lemma
is stated over a ring named <code class="docutils literal notranslate"><span class="pre">R</span></code>. So we can write:</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">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nontrivial</span><span class="w"> </span><span class="n">V</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">apply</span><span class="w"> </span><span class="o">(</span><span class="n">Module.finrank_pos_iff</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">K</span><span class="o">))</span><span class="bp">.</span><span class="mi">1</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>The above spelling is strange because we already have <code class="docutils literal notranslate"><span class="pre">h</span></code> as an assumption, so we could
just as well give the full proof <code class="docutils literal notranslate"><span class="pre">Module.finrank_pos_iff.1</span> <span class="pre">h</span></code> but it
is good to know for more complicated cases.</p>
<p>By definition, <code class="docutils literal notranslate"><span class="pre">FiniteDimensional</span> <span class="pre">K</span> <span class="pre">V</span></code> can be read from any basis.</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="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">B</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">Finite</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">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">FiniteDimensional.of_fintype_basis</span><span class="w"> </span><span class="n">B</span>

<span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Finite</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">FiniteDimensional.fintypeBasisIndex</span><span class="w"> </span><span class="n">B</span><span class="o">)</span><span class="bp">.</span><span class="n">finite</span>
<span class="kd">end</span>
</pre></div>
</div>
<p>Using that the subtype corresponding to a linear subspace has a vector space structure,
we can talk about the dimension of a subspace.</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">E</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span>

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

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span>
<span class="w">    </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Submodule.finrank_sup_add_finrank_inf_eq</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="n">F</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">Submodule.finrank_le</span><span class="w"> </span><span class="n">E</span>
</pre></div>
</div>
<p>In the first statement above, the purpose of the type ascriptions is to make sure that
coercion to <code class="docutils literal notranslate"><span class="pre">Type*</span></code> does not trigger too early.</p>
<p>We are now ready for an exercise about <code class="docutils literal notranslate"><span class="pre">finrank</span></code> and subspaces.</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">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">finrank</span><span class="w"> </span><span class="n">K</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">Nontrivial</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Submodule</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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>
</pre></div>
</div>
<p>Let us now move to the general case of dimension theory. In this case
<code class="docutils literal notranslate"><span class="pre">finrank</span></code> is useless, but we still have that, for any two bases of the same
vector space, there is a bijection between the types indexing those bases. So we
can still hope to define the rank as a cardinal, i.e. an element of the &#8220;quotient of
the collection of types under the existence of a bijection equivalence
relation&#8221;.</p>
<p>When discussing cardinal, it gets harder to ignore foundational issues around Russel&#8217;s paradox
like we do everywhere else in this book.
There is no type of all types because it would lead to logical inconsistencies.
This issue is solved by the hierarchy of universes that
we usually try to ignore.</p>
<p>Each type has a universe level, and those levels behave similarly to natural
numbers.&#8239;In particular there is zeroth level, and the corresponding universe
<code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">0</span></code> is simply denoted by <code class="docutils literal notranslate"><span class="pre">Type</span></code>. This universe is enough to hold
almost all of classical mathematics. For instance <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> have type <code class="docutils literal notranslate"><span class="pre">Type</span></code>.
Each level <code class="docutils literal notranslate"><span class="pre">u</span></code> has a successor denoted
by <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">+</span> <span class="pre">1</span></code>, and <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">u</span></code> has type <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">(u+1)</span></code>.</p>
<p>But universe levels are not natural numbers, they have a really different nature and don&#8217;t
have a type. In particular you cannot state in Lean something like <code class="docutils literal notranslate"><span class="pre">u</span> <span class="pre">&#8800;</span> <span class="pre">u</span> <span class="pre">+</span> <span class="pre">1</span></code>.
There is simply no type where this would take place. Even stating
<code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">u</span> <span class="pre">&#8800;</span> <span class="pre">Type</span> <span class="pre">(u+1)</span></code> does not make any sense since <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">u</span></code> and <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">(u+1)</span></code>
have different types.</p>
<p>Whenever we write <code class="docutils literal notranslate"><span class="pre">Type*</span></code>, Lean inserts a universe level variable named <code class="docutils literal notranslate"><span class="pre">u_n</span></code> where <code class="docutils literal notranslate"><span class="pre">n</span></code> is a
number. This allows definitions and statements to live in all universes.</p>
<p>Given a universe level <code class="docutils literal notranslate"><span class="pre">u</span></code>, we can define an equivalence relation on <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">u</span></code> saying
two types <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#946;</span></code> are equivalent if there is a bijection between them.
The quotient type <code class="docutils literal notranslate"><span class="pre">Cardinal.{u}</span></code> lives in <code class="docutils literal notranslate"><span class="pre">Type</span> <span class="pre">(u+1)</span></code>. The curly braces
denote a universe variable. The image of <code class="docutils literal notranslate"><span class="pre">&#945;</span> <span class="pre">:</span> <span class="pre">Type</span> <span class="pre">u</span></code> in this quotient is
<code class="docutils literal notranslate"><span class="pre">Cardinal.mk</span> <span class="pre">&#945;</span> <span class="pre">:</span> <span class="pre">Cardinal.{u}</span></code>.</p>
<p>But we cannot directly compare cardinals in different universes. So technically we
cannot define the rank of a vector space <code class="docutils literal notranslate"><span class="pre">V</span></code> as the cardinal of all types indexing
a basis of <code class="docutils literal notranslate"><span class="pre">V</span></code>.
So instead it is defined as the supremum <code class="docutils literal notranslate"><span class="pre">Module.rank</span> <span class="pre">K</span> <span class="pre">V</span></code> of cardinals of
all linearly independent sets in <code class="docutils literal notranslate"><span class="pre">V</span></code>. If <code class="docutils literal notranslate"><span class="pre">V</span></code> has universe level <code class="docutils literal notranslate"><span class="pre">u</span></code> then
its rank has type <code class="docutils literal notranslate"><span class="pre">Cardinal.{u}</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="c1">-- Type u_2</span>
<span class="k">#check</span><span class="w"> </span><span class="n">Module.rank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="c1">-- Cardinal.{u_2}</span>
</pre></div>
</div>
<p>One can still relate this definition to bases. Indeed there is also a commutative <code class="docutils literal notranslate"><span class="pre">max</span></code>
operation on universe levels, and given two universe levels <code class="docutils literal notranslate"><span class="pre">u</span></code> and <code class="docutils literal notranslate"><span class="pre">v</span></code>
there is an operation <code class="docutils literal notranslate"><span class="pre">Cardinal.lift.{u,</span> <span class="pre">v}</span> <span class="pre">:</span> <span class="pre">Cardinal.{v}</span> <span class="pre">&#8594;</span> <span class="pre">Cardinal.{max</span> <span class="pre">v</span> <span class="pre">u}</span></code>
that allows to put cardinals in a common universe and state the dimension theorem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">universe</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">v</span><span class="w"> </span><span class="c1">-- `u` and `v` will denote universe levels</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="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="w"> </span><span class="n">u</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">B</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">)</span>
<span class="w">         </span><span class="o">{</span><span class="n">&#953;&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="w"> </span><span class="n">v</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">B&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Basis</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</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">Cardinal.lift</span><span class="bp">.</span><span class="o">{</span><span class="n">v</span><span class="o">,</span><span class="w"> </span><span class="n">u</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="bp">.</span><span class="n">mk</span><span class="w"> </span><span class="n">&#953;</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Cardinal.lift</span><span class="bp">.</span><span class="o">{</span><span class="n">u</span><span class="o">,</span><span class="w"> </span><span class="n">v</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="bp">.</span><span class="n">mk</span><span class="w"> </span><span class="n">&#953;&#39;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">mk_eq_mk_of_basis</span><span class="w"> </span><span class="n">B</span><span class="w"> </span><span class="n">B&#39;</span>
</pre></div>
</div>
<p>We can relate the finite dimensional case to this discussion using the coercion
from natural numbers to finite cardinals (or more precisely the finite cardinals which live in <code class="docutils literal notranslate"><span class="pre">Cardinal.{v}</span></code> where <code class="docutils literal notranslate"><span class="pre">v</span></code> is the universe level of <code class="docutils literal notranslate"><span class="pre">V</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">FiniteDimensional</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="o">]</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="o">(</span><span class="n">Module.finrank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Cardinal</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Module.rank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Module.finrank_eq_rank</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">V</span>
</pre></div>
</div>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C09_Groups_and_Rings.html" class="btn btn-neutral float-left" title="9. Groups and Rings" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C11_Topology.html" class="btn btn-neutral float-right" title="11. Topology" 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-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</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>