OAI/AlgebraicGeometry/SurfaceCones/KummerShiftedOpen.lean

GitHub source file

174 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KummerShifted.cX line 14

   Source documentation

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

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

   Mentions: OAI.KummerShifted.C

2. def OAI.KummerShifted.chartDenominator line 15
3. lemma OAI.KummerShifted.chartDenominator_ne_zero line 16
4. lemma OAI.KummerShifted.planeMap_injective line 24
5. def OAI.KummerShifted.bDenominator line 31
6. lemma OAI.KummerShifted.bDenominator_ne_zero line 32
7. lemma OAI.KummerShifted.bPowers_le line 34
8. def OAI.KummerShifted.S line 38
9. instance OAI.KummerShifted.(instance at line 39) line 39
10. instance OAI.KummerShifted.(instance at line 40) line 40
11. instance OAI.KummerShifted.(instance at line 43) line 43
12. instance OAI.KummerShifted.(instance at line 44) line 44
13. instance OAI.KummerShifted.(instance at line 46) line 46
14. instance OAI.KummerShifted.(instance at line 48) line 48
15. instance OAI.KummerShifted.(instance at line 50) line 50
16. lemma OAI.KummerShifted.bDenominator_unit_in_L line 52
17. instance OAI.KummerShifted.(instance at line 56) line 56
18. instance OAI.KummerShifted.(instance at line 58) line 58
19. instance OAI.KummerShifted.(instance at line 61) line 61
20. instance OAI.KummerShifted.(instance at line 69) line 69
21. instance OAI.KummerShifted.(instance at line 70) line 70
22. instance OAI.KummerShifted.(instance at line 72) line 72
23. def OAI.KummerShifted.remainingRoot line 77
24. def OAI.KummerShifted.remainingForm line 78
25. lemma OAI.KummerShifted.remaining_dvd line 79
26. lemma OAI.KummerShifted.remaining_unit line 84
27. lemma OAI.KummerShifted.chartMap_X line 87
28. lemma OAI.KummerShifted.remainingRoot_pow line 92
29. lemma OAI.KummerShifted.exponent_unit line 114
30. def OAI.KummerShifted.remainingRoots line 119
31. abbrev OAI.KummerShifted.chartRootAlgebra line 122
32. theorem OAI.KummerShifted.chartRootAlgebra_finiteFreeEtale line 124
33. theorem OAI.KummerShifted.chartRootAlgebra_regular line 138
34. instance OAI.KummerShifted.(instance at line 152) line 152
35. instance OAI.KummerShifted.(instance at line 153) line 153
36. def OAI.KummerShifted.T line 157

    Source documentation

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

    def T := Localization.Away chartDenominator

    Mentions: OAI.KummerShifted.chartDenominator

37. instance OAI.KummerShifted.(instance at line 158) line 158
38. instance OAI.KummerShifted.(instance at line 159) line 159
39. instance OAI.KummerShifted.(instance at line 161) line 161
40. instance OAI.KummerShifted.coordinateMappedLocalization line 162
41. instance OAI.KummerShifted.(instance at line 167) line 167
42. instance OAI.KummerShifted.(instance at line 168) line 168
43. instance OAI.KummerShifted.(instance at line 170) line 170
44. instance OAI.KummerShifted.(instance at line 171) line 171
45. instance OAI.KummerShifted.(instance at line 173) line 173
46. instance OAI.KummerShifted.(instance at line 177) line 177
47. instance OAI.KummerShifted.(instance at line 178) line 178
48. instance OAI.KummerShifted.(instance at line 182) line 182
49. instance OAI.KummerShifted.(instance at line 184) line 184
50. instance OAI.KummerShifted.(instance at line 186) line 186
51. instance OAI.KummerShifted.(instance at line 191) line 191
52. instance OAI.KummerShifted.(instance at line 193) line 193
53. instance OAI.KummerShifted.(instance at line 195) line 195
54. instance OAI.KummerShifted.(instance at line 200) line 200
55. instance OAI.KummerShifted.(instance at line 201) line 201
56. instance OAI.KummerShifted.(instance at line 202) line 202
57. lemma OAI.KummerShifted.coordinateRoot_mem_chartRootAlgebra line 204
58. lemma OAI.KummerShifted.remainingRoot_mem_chartRootAlgebra line 209
59. lemma OAI.KummerShifted.allRoots_mem_chartRootAlgebra line 214
60. instance OAI.KummerShifted.(instance at line 234) line 234

    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.KummerShifted.S

61. instance OAI.KummerShifted.(instance at line 236) line 236
62. instance OAI.KummerShifted.(instance at line 238) line 238
63. instance OAI.KummerShifted.(instance at line 242) line 242
64. instance OAI.KummerShifted.(instance at line 244) line 244
65. instance OAI.KummerShifted.(instance at line 246) line 246
66. instance OAI.KummerShifted.(instance at line 251) line 251
67. theorem OAI.KummerShifted.chart_normalization line 260

    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.KummerShifted.T, OAI.KummerShifted.chartRootAlgebra

68. theorem OAI.KummerShifted.chart_normalization_regular line 277

    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.KummerShifted.T

69. def OAI.KummerShifted.chartRestrictionEquiv line 284

    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.KummerShifted.T, OAI.KummerShifted.C

70. theorem OAI.KummerShifted.normalization_chart_regular line 291
71. lemma OAI.KummerShifted.remainingRoot_inv_mem line 307
72. def OAI.ExplicitCone.shiftedSectionDenominator line 322
73. lemma OAI.ExplicitCone.shiftedSectionDenominator_ne_zero line 325
74. def OAI.ExplicitCone.shiftedSectionOpen line 329
75. def OAI.ExplicitCone.shiftedRegularAlgebra line 332
76. lemma OAI.ExplicitCone.y_mem_shiftedRegular line 341
77. lemma OAI.ExplicitCone.unitRoot_inv_mem_shiftedRegular line 343
78. lemma OAI.ExplicitCone.ratioQ_mem_shiftedRegular line 347
79. lemma OAI.ExplicitCone.ratioR_mem_shiftedRegular line 357
80. lemma OAI.ExplicitCone.sectionChart_le_shiftedRegular line 366
81. lemma OAI.ExplicitCone.ratioR_inv_mem_shiftedRegular line 374
82. lemma OAI.ExplicitCone.shiftedSectionOpen_le line 381
83. lemma OAI.ExplicitCone.sectionChart_le_shiftedOpen line 391
84. lemma OAI.ExplicitCone.y_mem_shiftedOpen line 393
85. lemma OAI.ExplicitCone.ratioQ_mem_shiftedOpen line 395
86. lemma OAI.ExplicitCone.ratioR_mem_shiftedOpen line 397
87. lemma OAI.ExplicitCone.shiftedProduct_inv_mem line 399
88. lemma OAI.ExplicitCone.y0_inv_mem_shiftedOpen line 401
89. lemma OAI.ExplicitCone.y1_inv_mem_shiftedOpen line 406
90. lemma OAI.ExplicitCone.ratioR_inv_mem_shiftedOpen line 411
91. lemma OAI.ExplicitCone.coordinateRoot_mem_shiftedOpen line 417
92. lemma OAI.ExplicitCone.B_mem_shiftedOpen line 429
93. lemma OAI.ExplicitCone.remainingRoot_mem_shiftedOpen line 433
94. lemma OAI.ExplicitCone.remainingRoot_inv_mem_shiftedOpen line 444
95. lemma OAI.ExplicitCone.shifted_bDenominator_image line 456
96. lemma OAI.ExplicitCone.bDenominator_inv_mem_shiftedOpen line 466
97. lemma OAI.ExplicitCone.S_mem_shiftedOpen line 472
98. lemma OAI.ExplicitCone.shiftedRegular_le_sectionOpen line 477
99. theorem OAI.ExplicitCone.shiftedSectionOpen_eq line 492

    Source documentation

    The literal polarization chart, localized at a*b*r, is exactly the regular normalization of the literal shifted-point blowup open, within the same original function field.

    theorem shiftedSectionOpen_eq : shiftedSectionOpen = shiftedRegularAlgebra :=
    …

    Mentions: OAI.ExplicitCone.shiftedSectionOpen, OAI.ExplicitCone.shiftedRegularAlgebra

100. theorem OAI.ExplicitCone.sectionChart_shiftedOpen_regular line 495
101. abbrev OAI.KummerShiftedDiagonal.root line 512
102. lemma OAI.KummerShiftedDiagonal.root_pow line 513
103. lemma OAI.KummerShiftedDiagonal.root_ne_zero line 515
104. def OAI.KummerShiftedDiagonal.coordinateRoot line 518

     Source documentation

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

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

     Mentions: OAI.KummerShiftedDiagonal.root

105. lemma OAI.KummerShiftedDiagonal.coordinateRoot_zero_pow line 519
106. lemma OAI.KummerShiftedDiagonal.coordinateRoot_one_pow line 521
107. lemma OAI.KummerShiftedDiagonal.original_root_four line 526
108. lemma OAI.KummerShiftedDiagonal.original_x line 529
109. lemma OAI.KummerShiftedDiagonal.original_y line 536
110. lemma OAI.KummerShiftedDiagonal.coordinateRoot_independent line 538
111. def OAI.KummerShiftedDiagonal.C line 560
112. instance OAI.KummerShiftedDiagonal.(instance at line 561) line 561
113. instance OAI.KummerShiftedDiagonal.(instance at line 562) line 562
114. instance OAI.KummerShiftedDiagonal.(instance at line 563) line 563
115. instance OAI.KummerShiftedDiagonal.(instance at line 564) line 564
116. def OAI.KummerShiftedDiagonal.blowdown line 565
117. instance OAI.KummerShiftedDiagonal.(instance at line 566) line 566
118. instance OAI.KummerShiftedDiagonal.(instance at line 567) line 567
119. def OAI.KummerShiftedDiagonal.chartMap line 570
120. instance OAI.KummerShiftedDiagonal.(instance at line 573) line 573
121. instance OAI.KummerShiftedDiagonal.(instance at line 574) line 574
122. lemma OAI.KummerShiftedDiagonal.chartMap_blowdown line 576
123. instance OAI.KummerShiftedDiagonal.(instance at line 610) line 610
124. lemma OAI.KummerShiftedDiagonal.chartMap_injective line 613
125. def OAI.KummerShiftedDiagonal.coordinateAlgebra line 653

     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) :=
     …

126. abbrev OAI.KummerShiftedDiagonal.B line 655
127. def OAI.KummerShiftedDiagonal.planeEquiv line 656
128. instance OAI.KummerShiftedDiagonal.(instance at line 657) line 657
129. instance OAI.KummerShiftedDiagonal.(instance at line 659) line 659
130. def OAI.KummerShiftedDiagonal.bRoot line 664
131. def OAI.KummerShiftedDiagonal.planeMap line 666
132. lemma OAI.KummerShiftedDiagonal.planeMap_comp line 667
133. instance OAI.KummerShiftedDiagonal.(instance at line 675) line 675
134. instance OAI.KummerShiftedDiagonal.(instance at line 676) line 676
135. instance OAI.KummerShiftedDiagonal.(instance at line 678) line 678
136. lemma OAI.KummerShiftedDiagonal.coordinateRoot_pow line 681
137. lemma OAI.KummerShiftedDiagonal.coordinateRoot_integral line 688
138. instance OAI.KummerShiftedDiagonal.(instance at line 695) line 695
139. instance OAI.KummerShiftedDiagonal.(instance at line 705) line 705
140. instance OAI.KummerShiftedDiagonal.(instance at line 707) line 707
141. instance OAI.KummerShiftedDiagonal.(instance at line 708) line 708
142. def OAI.KummerShiftedDiagonal.cX line 723

     Source documentation

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

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

     Mentions: OAI.KummerShiftedDiagonal.C

143. def OAI.KummerShiftedDiagonal.chartDenominator line 724
144. lemma OAI.KummerShiftedDiagonal.chartDenominator_ne_zero line 725
145. lemma OAI.KummerShiftedDiagonal.planeMap_injective line 733
146. def OAI.KummerShiftedDiagonal.bDenominator line 740
147. lemma OAI.KummerShiftedDiagonal.bDenominator_ne_zero line 741
148. lemma OAI.KummerShiftedDiagonal.bPowers_le line 743
149. def OAI.KummerShiftedDiagonal.S line 747
150. instance OAI.KummerShiftedDiagonal.(instance at line 748) line 748
151. instance OAI.KummerShiftedDiagonal.(instance at line 749) line 749
152. instance OAI.KummerShiftedDiagonal.(instance at line 752) line 752
153. instance OAI.KummerShiftedDiagonal.(instance at line 753) line 753
154. instance OAI.KummerShiftedDiagonal.(instance at line 755) line 755
155. instance OAI.KummerShiftedDiagonal.(instance at line 757) line 757
156. instance OAI.KummerShiftedDiagonal.(instance at line 759) line 759
157. lemma OAI.KummerShiftedDiagonal.bDenominator_unit_in_L line 761
158. instance OAI.KummerShiftedDiagonal.(instance at line 765) line 765
159. instance OAI.KummerShiftedDiagonal.(instance at line 767) line 767
160. instance OAI.KummerShiftedDiagonal.(instance at line 770) line 770
161. instance OAI.KummerShiftedDiagonal.(instance at line 778) line 778
162. instance OAI.KummerShiftedDiagonal.(instance at line 779) line 779
163. instance OAI.KummerShiftedDiagonal.(instance at line 781) line 781
164. def OAI.KummerShiftedDiagonal.remainingRoot line 786
165. def OAI.KummerShiftedDiagonal.remainingForm line 787
166. lemma OAI.KummerShiftedDiagonal.remaining_dvd line 788
167. lemma OAI.KummerShiftedDiagonal.remaining_unit line 793
168. lemma OAI.KummerShiftedDiagonal.chartMap_X line 796
169. lemma OAI.KummerShiftedDiagonal.remainingRoot_pow line 801
170. lemma OAI.KummerShiftedDiagonal.exponent_unit line 825
171. def OAI.KummerShiftedDiagonal.remainingRoots line 830
172. abbrev OAI.KummerShiftedDiagonal.chartRootAlgebra line 833
173. theorem OAI.KummerShiftedDiagonal.chartRootAlgebra_finiteFreeEtale line 835
174. theorem OAI.KummerShiftedDiagonal.chartRootAlgebra_regular line 849