OAI/GroupTheory/BooneHigman/Corners.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.U line 14
2. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.V line 15
3. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.UI line 16
4. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.VI line 17
5. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.E0 line 18
6. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.E1 line 19
7. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Eh line 20
8. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.U_apply line 22
9. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.V_apply line 24
10. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.UI_apply line 26
11. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.VI_apply line 28
12. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E0_val line 30
13. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E1_val line 32
14. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.U_UI line 35
15. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.UI_U line 40
16. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.V_VI line 46
17. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.VI_V line 51
18. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.U_tail line 58
19. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.V_tail line 73
20. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Eh_val line 88
21. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.U_E0_UI line 91
22. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.U_E1_UI line 96
23. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.V_E0_VI line 97
24. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.V_E1_VI line 102
25. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.tails_mul line 108
26. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E0_E0 line 114
27. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E0_Eh line 115
28. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E0_E1 line 116
29. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Eh_E0 line 117
30. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Eh_Eh line 118
31. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Eh_E1 line 119
32. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E1_E0 line 120
33. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E1_Eh line 121
34. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E1_E1 line 122
35. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E0_ne_E1 line 124
36. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.E0_ne_one line 130
37. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.b line 141
38. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.b_mul line 142
39. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.b_one line 143
40. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q line 145
41. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q0 line 146
42. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q1 line 147
43. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q_idem line 149
44. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q0_idem line 152
45. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q1_idem line 155
46. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q0_q1 line 158
47. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q1_q0 line 161
48. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q0_add_q1 line 164
49. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q_q0 line 165
50. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q0_q line 166
51. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q_q1 line 167
52. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q1_q line 168
53. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q_ne_zero line 170
54. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q_ne_one line 175
55. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.s0 line 180
56. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.s1 line 181
57. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t0 line 182
58. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t1 line 183
59. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.conjugate0 line 185
60. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.conjugate1 line 187
61. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t0_s0 line 190
62. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t1_s1 line 195
63. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.s0_t0 line 200
64. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.s1_t1 line 203
65. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.s0_q line 207
66. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.s1_q line 208
67. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q_t0 line 209
68. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q_t1 line 210
69. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q0_s0 line 211
70. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q1_s1 line 212
71. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t0_q0 line 213
72. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t1_q1 line 214
73. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q_s0 line 215
74. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.q_s1 line 216
75. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t0_q line 217
76. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t1_q line 218
77. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t0_s1 line 219
78. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.t1_s0 line 224
79. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.s0_t0_add_s1_t1 line 229
80. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.cornerTensor line 238
81. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.coefficient0 line 245
82. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.coefficient0_q line 250
83. def OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.cornerRetract line 254
84. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.cornerRetract_cornerTensor line 257
85. theorem OAI.FiniteAlgebraicEnvelopes.PartialAffine.Corner.cornerTensor_injective line 262
86. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.rho line 273

    Source documentation

    The actual unital tensor embedding from the algebra construction, not supplied as a hypothesis.

    def rho : BigAlgebra s h k ⊗[k] MonoidAlgebra k PartialAffine.monoid →ₐ[k] SmallAlgebra s h k :=
    …

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.BigAlgebra, OAI.FiniteAlgebraicEnvelopes.PartialAffine.monoid, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.SmallAlgebra

87. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.rho_injective line 276
88. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.j line 279
89. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.j_injective line 282
90. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.phi line 285
91. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.phi_injective line 288
92. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.phi_one_ne_one line 291
93. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.map line 303
94. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.map_tmul line 316
95. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.map_injective line 319
96. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.op line 324
97. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.op_apply line 331
98. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.op_injective line 333
99. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.xi line 348
100. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.phi_eq line 351
101. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.xi_constant_commute line 353
102. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.supported line 360
103. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.pair0 line 383
104. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.pair1 line 385
105. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.pair0_pair1 line 388
106. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.pair1_pair0 line 391
107. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.pairs_sum line 395
108. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.TAlgebra line 409
109. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separatingElement line 411
110. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separationBilinear line 413
111. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separationLinear line 420
112. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separationLinear_tmul line 423
113. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separatorIndex line 426
114. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separatorIndex_injective line 429
115. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separationLinear_basis line 433
116. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.separationLinear_injective line 440
117. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.jT line 454

     Source documentation

     The map j before the final κ extension, with image in the actual T algebra.

     def jT : BigAlgebra s h k →ₙₐ[k] TAlgebra s h k :=
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.BigAlgebra, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.TAlgebra

118. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.jT_injective line 458
119. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.jT_apply line 462
120. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.linear line 470
121. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.linear_apply line 471
122. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.coefficient line 476
123. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.ringHom line 478
124. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.ringHom_apply line 480
125. def OAI.FiniteAlgebraicEnvelopes.Enveloping.act line 488
126. theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.act_eq_smul line 490
127. theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.act_zero line 491
128. theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.act_add line 492
129. theorem OAI.FiniteAlgebraicEnvelopes.Enveloping.act_tmul line 493
130. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.actingLinear line 500
131. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.actingLinear_apply line 503
132. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.actingLinear_tmul line 506
133. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.R line 516
134. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.psi line 520
135. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.psi_injective line 527
136. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.psi_tmul line 530
137. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.detectionInput line 533
138. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.detectionInput_injective line 538
139. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.detectionLinear line 542
140. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.detectionLinear_injective line 546
141. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.detectingElement line 550
142. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.detectionLinear_eq line 552
143. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.detectionLinear_apply line 562
144. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.tensor_detection line 567

     Source documentation

     The actual separator proves tensor detection, with a single fixed detecting vector.

     theorem tensor_detection [Nontrivial k] (r : R s h k) (hr : ∀ b : BigAlgebra s h k, Enveloping.act k (BigAlgebra s h k) (psi s h k r) b=0) : r=0 := by
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.R, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.BigAlgebra, OAI.FiniteAlgebraicEnvelopes.Enveloping.act, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.psi

145. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.coefficientRing line 583
146. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.image_left line 589
147. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.image_right line 590
148. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.coefficient_one line 591
149. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.tensor_constant_commute line 595
150. def OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.supportedPair line 604
151. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.supportedPair_cross line 635
152. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.supportedPair_sum line 640
153. theorem OAI.FiniteAlgebraicEnvelopes.NonunitalTensor.annihilation line 651
154. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringPsi line 672
155. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringPair0 line 674
156. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringPair1 line 676
157. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringPair01 line 679
158. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringPair10 line 681
159. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringPairSum line 683
160. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.source_kernel_annihilation line 689

     Source documentation

     Actual coefficient endomorphism kills the whole Steinberg kernel in one step.

     theorem source_kernel_annihilation
         (kernelElement : Steinberg.Group (Fin 6) (R s h k))
         (inKernel : Steinberg.matrixMap kernelElement = 1) :
         Steinberg.coefficientMap (ringPsi s h k) kernelElement = 1 :=
     …

     Mentions: OAI.FiniteAlgebraicEnvelopes.Steinberg.Group, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.R, OAI.FiniteAlgebraicEnvelopes.Steinberg.matrixMap, OAI.FiniteAlgebraicEnvelopes.Steinberg.coefficientMap, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Source.ringPsi