OAI/AlgebraicGeometry/SurfaceCones/KummerTripleDiagonalCoordinates.lean

GitHub source file

180 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KummerTripleDiagonal.root line 12
2. lemma OAI.KummerTripleDiagonal.root_pow line 13
3. lemma OAI.KummerTripleDiagonal.root_ne_zero line 15
4. def OAI.KummerTripleDiagonal.coordinateRoot line 26

   Source documentation

   Coordinates at the exceptional divisor over the actual triple point (0,0): u is the original root of x, v is root(x−y)/root(x).

   def coordinateRoot : Fin 2 → L p := ![root p 0, root p 4 / root p 0]

   Mentions: OAI.KummerTripleDiagonal.root

5. lemma OAI.KummerTripleDiagonal.coordinateRoot_zero_pow line 27
6. lemma OAI.KummerTripleDiagonal.coordinateRoot_one_pow line 29
7. lemma OAI.KummerTripleDiagonal.original_root_one line 34
8. lemma OAI.KummerTripleDiagonal.coordinateRoot_independent line 38
9. def OAI.KummerTripleDiagonal.C line 66

   Source documentation

   The x-chart of the blowup of the original plane at (0,0). Its coordinates s,t map to x,(x−y)/x, and the blowdown is x=s,y=s−st.

   def C := MvPolynomial (Fin 2) ℂ

10. instance OAI.KummerTripleDiagonal.(instance at line 67) line 67
11. instance OAI.KummerTripleDiagonal.(instance at line 68) line 68
12. instance OAI.KummerTripleDiagonal.(instance at line 69) line 69
13. instance OAI.KummerTripleDiagonal.(instance at line 70) line 70
14. def OAI.KummerTripleDiagonal.blowdown line 71
15. instance OAI.KummerTripleDiagonal.(instance at line 72) line 72
16. instance OAI.KummerTripleDiagonal.(instance at line 73) line 73
17. def OAI.KummerTripleDiagonal.chartMap line 76
18. instance OAI.KummerTripleDiagonal.(instance at line 78) line 78
19. instance OAI.KummerTripleDiagonal.(instance at line 79) line 79
20. lemma OAI.KummerTripleDiagonal.chartMap_blowdown line 81
21. instance OAI.KummerTripleDiagonal.(instance at line 106) line 106
22. lemma OAI.KummerTripleDiagonal.chartMap_injective line 109
23. def OAI.KummerTripleDiagonal.coordinateAlgebra line 139

    Source documentation

    The two ramified coordinates form an actual polynomial plane in the original field. No independent auxiliary Kummer field is substituted.

    def coordinateAlgebra : Subalgebra ℂ (L p) :=
    …

24. abbrev OAI.KummerTripleDiagonal.B line 141
25. def OAI.KummerTripleDiagonal.planeEquiv line 142
26. instance OAI.KummerTripleDiagonal.(instance at line 143) line 143
27. instance OAI.KummerTripleDiagonal.(instance at line 145) line 145
28. def OAI.KummerTripleDiagonal.bRoot line 150
29. def OAI.KummerTripleDiagonal.planeMap line 152
30. lemma OAI.KummerTripleDiagonal.planeMap_comp line 153
31. instance OAI.KummerTripleDiagonal.(instance at line 161) line 161
32. instance OAI.KummerTripleDiagonal.(instance at line 162) line 162
33. instance OAI.KummerTripleDiagonal.(instance at line 164) line 164
34. lemma OAI.KummerTripleDiagonal.coordinateRoot_pow line 167
35. lemma OAI.KummerTripleDiagonal.coordinateRoot_integral line 174
36. instance OAI.KummerTripleDiagonal.(instance at line 181) line 181
37. instance OAI.KummerTripleDiagonal.(instance at line 191) line 191
38. instance OAI.KummerTripleDiagonal.(instance at line 193) line 193
39. instance OAI.KummerTripleDiagonal.(instance at line 194) line 194
40. def OAI.KummerTripleDiagonal.cX line 209

    Source documentation

    The actual blowup chart open containing s=t=0 (the intersection of its exceptional divisor with the strict transform of x−y=0).

    def cX (i : Fin 2) : C := X i

    Mentions: OAI.KummerTripleDiagonal.C

41. def OAI.KummerTripleDiagonal.chartDenominator line 210
42. lemma OAI.KummerTripleDiagonal.chartDenominator_ne_zero line 211
43. lemma OAI.KummerTripleDiagonal.planeMap_injective line 219
44. def OAI.KummerTripleDiagonal.bDenominator line 226
45. lemma OAI.KummerTripleDiagonal.bDenominator_ne_zero line 227
46. lemma OAI.KummerTripleDiagonal.bPowers_le line 229
47. def OAI.KummerTripleDiagonal.S line 233
48. instance OAI.KummerTripleDiagonal.(instance at line 234) line 234
49. instance OAI.KummerTripleDiagonal.(instance at line 235) line 235
50. instance OAI.KummerTripleDiagonal.(instance at line 238) line 238
51. instance OAI.KummerTripleDiagonal.(instance at line 239) line 239
52. instance OAI.KummerTripleDiagonal.(instance at line 241) line 241
53. instance OAI.KummerTripleDiagonal.(instance at line 243) line 243
54. instance OAI.KummerTripleDiagonal.(instance at line 245) line 245
55. lemma OAI.KummerTripleDiagonal.bDenominator_unit_in_L line 247
56. instance OAI.KummerTripleDiagonal.(instance at line 251) line 251
57. instance OAI.KummerTripleDiagonal.(instance at line 253) line 253
58. instance OAI.KummerTripleDiagonal.(instance at line 256) line 256
59. instance OAI.KummerTripleDiagonal.(instance at line 264) line 264
60. instance OAI.KummerTripleDiagonal.(instance at line 265) line 265
61. instance OAI.KummerTripleDiagonal.(instance at line 267) line 267
62. def OAI.KummerTripleDiagonal.remainingRoot line 272
63. def OAI.KummerTripleDiagonal.remainingForm line 273
64. lemma OAI.KummerTripleDiagonal.remaining_dvd line 274
65. lemma OAI.KummerTripleDiagonal.remaining_unit line 279
66. lemma OAI.KummerTripleDiagonal.chartMap_X line 282
67. lemma OAI.KummerTripleDiagonal.remainingRoot_pow line 287
68. lemma OAI.KummerTripleDiagonal.exponent_unit line 319
69. def OAI.KummerTripleDiagonal.remainingRoots line 324
70. abbrev OAI.KummerTripleDiagonal.chartRootAlgebra line 327
71. theorem OAI.KummerTripleDiagonal.chartRootAlgebra_finiteFreeEtale line 329
72. theorem OAI.KummerTripleDiagonal.chartRootAlgebra_regular line 343
73. instance OAI.KummerTripleDiagonal.(instance at line 357) line 357
74. instance OAI.KummerTripleDiagonal.(instance at line 358) line 358
75. def OAI.KummerTripleDiagonal.T line 362

    Source documentation

    The actual open D((s−1)(st−1)(1−t)) of the blowup chart.

    def T := Localization.Away chartDenominator

    Mentions: OAI.KummerTripleDiagonal.chartDenominator

76. instance OAI.KummerTripleDiagonal.(instance at line 363) line 363
77. instance OAI.KummerTripleDiagonal.(instance at line 364) line 364
78. instance OAI.KummerTripleDiagonal.(instance at line 366) line 366
79. instance OAI.KummerTripleDiagonal.coordinateMappedLocalization line 367
80. instance OAI.KummerTripleDiagonal.(instance at line 372) line 372
81. instance OAI.KummerTripleDiagonal.(instance at line 373) line 373
82. instance OAI.KummerTripleDiagonal.(instance at line 375) line 375
83. instance OAI.KummerTripleDiagonal.(instance at line 376) line 376
84. instance OAI.KummerTripleDiagonal.(instance at line 378) line 378
85. instance OAI.KummerTripleDiagonal.(instance at line 382) line 382
86. instance OAI.KummerTripleDiagonal.(instance at line 383) line 383
87. instance OAI.KummerTripleDiagonal.(instance at line 387) line 387
88. instance OAI.KummerTripleDiagonal.(instance at line 389) line 389
89. instance OAI.KummerTripleDiagonal.(instance at line 391) line 391
90. instance OAI.KummerTripleDiagonal.(instance at line 396) line 396
91. instance OAI.KummerTripleDiagonal.(instance at line 398) line 398
92. instance OAI.KummerTripleDiagonal.(instance at line 400) line 400
93. instance OAI.KummerTripleDiagonal.(instance at line 405) line 405
94. instance OAI.KummerTripleDiagonal.(instance at line 406) line 406
95. instance OAI.KummerTripleDiagonal.(instance at line 407) line 407
96. lemma OAI.KummerTripleDiagonal.coordinateRoot_mem_chartRootAlgebra line 409
97. lemma OAI.KummerTripleDiagonal.remainingRoot_mem_chartRootAlgebra line 414
98. lemma OAI.KummerTripleDiagonal.allRoots_mem_chartRootAlgebra line 419
99. instance OAI.KummerTripleDiagonal.(instance at line 439) line 439

    Source comment

    The fraction field is the SAME original Kummer field, not a proper subcover of it. The blowdown supplies the original plane action.

    instance : Algebra R (S p) :=
    …

    Mentions: OAI.KummerTripleDiagonal.S

100. instance OAI.KummerTripleDiagonal.(instance at line 441) line 441
101. instance OAI.KummerTripleDiagonal.(instance at line 443) line 443
102. instance OAI.KummerTripleDiagonal.(instance at line 447) line 447
103. instance OAI.KummerTripleDiagonal.(instance at line 449) line 449
104. instance OAI.KummerTripleDiagonal.(instance at line 451) line 451
105. instance OAI.KummerTripleDiagonal.(instance at line 456) line 456
106. theorem OAI.KummerTripleDiagonal.chart_normalization line 465

     Source documentation

     The entire normalization over this actual triple-point blowup open is the regular algebra of the two ramified coordinates and three unit roots.

     theorem chart_normalization : integralClosure T (L p) =
         (chartRootAlgebra p).restrictScalars T := by
     …

     Mentions: OAI.KummerTripleDiagonal.T, OAI.KummerTripleDiagonal.chartRootAlgebra

107. theorem OAI.KummerTripleDiagonal.chart_normalization_regular line 482

     Source documentation

     Regularity is asserted for the actual integral closure, not just a subextension or the conditional diagonal coordinate algebra.

     theorem chart_normalization_regular : IsRegularRing (integralClosure T (L p)) := by
     …

     Mentions: OAI.KummerTripleDiagonal.T

108. def OAI.KummerTripleDiagonal.chartRestrictionEquiv line 489

     Source documentation

     This normalization is the actual restriction of the normalization of the blowup chart in the original five-root field.

     def chartRestrictionEquiv :
         T ⊗[C] integralClosure C (L p) ≃ₐ[T] integralClosure T (L p) := by
     …

     Mentions: OAI.KummerTripleDiagonal.T, OAI.KummerTripleDiagonal.C

109. theorem OAI.KummerTripleDiagonal.normalization_chart_regular line 496
110. lemma OAI.KummerTripleDiagonal.remainingRoot_inv_mem line 512
111. def OAI.ExplicitCone.diagonalSectionDenominator line 527
112. lemma OAI.ExplicitCone.diagonalSectionDenominator_ne_zero line 530
113. def OAI.ExplicitCone.diagonalSectionOpen line 534
114. def OAI.ExplicitCone.diagonalRegularAlgebra line 537
115. lemma OAI.ExplicitCone.y_mem_diagonalRegular line 546
116. lemma OAI.ExplicitCone.unitRoot_inv_mem_diagonalRegular line 548
117. lemma OAI.ExplicitCone.ratioQ_mem_diagonalRegular line 552
118. lemma OAI.ExplicitCone.ratioR_mem_diagonalRegular line 562
119. lemma OAI.ExplicitCone.sectionChart_le_diagonalRegular line 571
120. lemma OAI.ExplicitCone.ratioQ_inv_mem_diagonalRegular line 579
121. lemma OAI.ExplicitCone.diagonalSectionOpen_le line 588
122. lemma OAI.ExplicitCone.sectionChart_le_diagonalOpen line 598
123. lemma OAI.ExplicitCone.y_mem_diagonalOpen line 600
124. lemma OAI.ExplicitCone.ratioQ_mem_diagonalOpen line 602
125. lemma OAI.ExplicitCone.ratioR_mem_diagonalOpen line 604
126. lemma OAI.ExplicitCone.diagonalProduct_inv_mem line 606
127. lemma OAI.ExplicitCone.y2_inv_mem_diagonalOpen line 608
128. lemma OAI.ExplicitCone.y3_inv_mem_diagonalOpen line 613
129. lemma OAI.ExplicitCone.ratioQ_inv_mem_diagonalOpen line 618
130. lemma OAI.ExplicitCone.coordinateRoot_mem_diagonalOpen line 624
131. lemma OAI.ExplicitCone.B_mem_diagonalOpen line 634
132. lemma OAI.ExplicitCone.remainingRoot_mem_diagonalOpen line 638
133. lemma OAI.ExplicitCone.remainingRoot_inv_mem_diagonalOpen line 651
134. lemma OAI.ExplicitCone.diagonal_bDenominator_image line 665
135. lemma OAI.ExplicitCone.bDenominator_inv_mem_diagonalOpen line 675
136. lemma OAI.ExplicitCone.S_mem_diagonalOpen line 681
137. lemma OAI.ExplicitCone.diagonalRegular_le_sectionOpen line 686
138. theorem OAI.ExplicitCone.diagonalSectionOpen_eq line 701

     Source documentation

     The literal polarization chart, localized at c*d*q, is exactly the regular normalization of the literal diagonal-point blowup open, within the same original function field.

     theorem diagonalSectionOpen_eq : diagonalSectionOpen = diagonalRegularAlgebra :=
     …

     Mentions: OAI.ExplicitCone.diagonalSectionOpen, OAI.ExplicitCone.diagonalRegularAlgebra

139. theorem OAI.ExplicitCone.sectionChart_diagonalOpen_regular line 704
140. abbrev OAI.KummerShifted.root line 721
141. lemma OAI.KummerShifted.root_pow line 722
142. lemma OAI.KummerShifted.root_ne_zero line 724
143. def OAI.KummerShifted.coordinateRoot line 727

     Source documentation

     Literal y-chart over the other affine triple point (1,1).

     def coordinateRoot : Fin 2 → L p := ![root p 3, root p 2 / root p 3]

     Mentions: OAI.KummerShifted.root

144. lemma OAI.KummerShifted.coordinateRoot_zero_pow line 728
145. lemma OAI.KummerShifted.coordinateRoot_one_pow line 730
146. lemma OAI.KummerShifted.original_root_two line 735
147. lemma OAI.KummerShifted.original_x line 738
148. lemma OAI.KummerShifted.original_y line 743
149. lemma OAI.KummerShifted.coordinateRoot_independent line 745
150. def OAI.KummerShifted.C line 765
151. instance OAI.KummerShifted.(instance at line 766) line 766
152. instance OAI.KummerShifted.(instance at line 767) line 767
153. instance OAI.KummerShifted.(instance at line 768) line 768
154. instance OAI.KummerShifted.(instance at line 769) line 769
155. def OAI.KummerShifted.blowdown line 770
156. instance OAI.KummerShifted.(instance at line 771) line 771
157. instance OAI.KummerShifted.(instance at line 772) line 772
158. def OAI.KummerShifted.chartMap line 775
159. instance OAI.KummerShifted.(instance at line 778) line 778
160. instance OAI.KummerShifted.(instance at line 779) line 779
161. lemma OAI.KummerShifted.chartMap_blowdown line 781
162. instance OAI.KummerShifted.(instance at line 810) line 810
163. lemma OAI.KummerShifted.chartMap_injective line 813
164. def OAI.KummerShifted.coordinateAlgebra line 851

     Source documentation

     The two ramified coordinates form an actual polynomial plane in the original field. No independent auxiliary Kummer field is substituted.

     def coordinateAlgebra : Subalgebra ℂ (L p) :=
     …

165. abbrev OAI.KummerShifted.B line 853
166. def OAI.KummerShifted.planeEquiv line 854
167. instance OAI.KummerShifted.(instance at line 855) line 855
168. instance OAI.KummerShifted.(instance at line 857) line 857
169. def OAI.KummerShifted.bRoot line 862
170. def OAI.KummerShifted.planeMap line 864
171. lemma OAI.KummerShifted.planeMap_comp line 865
172. instance OAI.KummerShifted.(instance at line 873) line 873
173. instance OAI.KummerShifted.(instance at line 874) line 874
174. instance OAI.KummerShifted.(instance at line 876) line 876
175. lemma OAI.KummerShifted.coordinateRoot_pow line 879
176. lemma OAI.KummerShifted.coordinateRoot_integral line 886
177. instance OAI.KummerShifted.(instance at line 893) line 893
178. instance OAI.KummerShifted.(instance at line 903) line 903
179. instance OAI.KummerShifted.(instance at line 905) line 905
180. instance OAI.KummerShifted.(instance at line 906) line 906