OAI/AlgebraicGeometry/SurfaceCones/KummerShiftedDiagonalNormalization.lean

GitHub source file

168 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.KummerShiftedDiagonal.(instance at line 11) line 11
2. instance OAI.KummerShiftedDiagonal.(instance at line 12) line 12
3. def OAI.KummerShiftedDiagonal.T line 16

   Source documentation

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

   def T := Localization.Away chartDenominator

   Mentions: OAI.KummerShiftedDiagonal.chartDenominator

4. instance OAI.KummerShiftedDiagonal.(instance at line 17) line 17
5. instance OAI.KummerShiftedDiagonal.(instance at line 18) line 18
6. instance OAI.KummerShiftedDiagonal.(instance at line 20) line 20
7. instance OAI.KummerShiftedDiagonal.coordinateMappedLocalization line 21
8. instance OAI.KummerShiftedDiagonal.(instance at line 26) line 26
9. instance OAI.KummerShiftedDiagonal.(instance at line 27) line 27
10. instance OAI.KummerShiftedDiagonal.(instance at line 29) line 29
11. instance OAI.KummerShiftedDiagonal.(instance at line 30) line 30
12. instance OAI.KummerShiftedDiagonal.(instance at line 32) line 32
13. instance OAI.KummerShiftedDiagonal.(instance at line 36) line 36
14. instance OAI.KummerShiftedDiagonal.(instance at line 37) line 37
15. instance OAI.KummerShiftedDiagonal.(instance at line 41) line 41
16. instance OAI.KummerShiftedDiagonal.(instance at line 43) line 43
17. instance OAI.KummerShiftedDiagonal.(instance at line 45) line 45
18. instance OAI.KummerShiftedDiagonal.(instance at line 50) line 50
19. instance OAI.KummerShiftedDiagonal.(instance at line 52) line 52
20. instance OAI.KummerShiftedDiagonal.(instance at line 54) line 54
21. instance OAI.KummerShiftedDiagonal.(instance at line 59) line 59
22. instance OAI.KummerShiftedDiagonal.(instance at line 60) line 60
23. instance OAI.KummerShiftedDiagonal.(instance at line 61) line 61
24. lemma OAI.KummerShiftedDiagonal.coordinateRoot_mem_chartRootAlgebra line 63
25. lemma OAI.KummerShiftedDiagonal.remainingRoot_mem_chartRootAlgebra line 68
26. lemma OAI.KummerShiftedDiagonal.allRoots_mem_chartRootAlgebra line 73
27. instance OAI.KummerShiftedDiagonal.(instance at line 93) line 93

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

28. instance OAI.KummerShiftedDiagonal.(instance at line 95) line 95
29. instance OAI.KummerShiftedDiagonal.(instance at line 97) line 97
30. instance OAI.KummerShiftedDiagonal.(instance at line 101) line 101
31. instance OAI.KummerShiftedDiagonal.(instance at line 103) line 103
32. instance OAI.KummerShiftedDiagonal.(instance at line 105) line 105
33. instance OAI.KummerShiftedDiagonal.(instance at line 110) line 110
34. theorem OAI.KummerShiftedDiagonal.chart_normalization line 119

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

35. theorem OAI.KummerShiftedDiagonal.chart_normalization_regular line 136

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

36. def OAI.KummerShiftedDiagonal.chartRestrictionEquiv line 143

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

37. theorem OAI.KummerShiftedDiagonal.normalization_chart_regular line 150
38. lemma OAI.KummerShiftedDiagonal.remainingRoot_inv_mem line 166
39. def OAI.ExplicitCone.shiftedDiagonalSectionDenominator line 181
40. lemma OAI.ExplicitCone.shiftedDiagonalSectionDenominator_ne_zero line 184
41. def OAI.ExplicitCone.shiftedDiagonalSectionOpen line 188
42. def OAI.ExplicitCone.shiftedDiagonalRegularAlgebra line 191
43. lemma OAI.ExplicitCone.y_mem_shiftedDiagonalRegular line 200
44. lemma OAI.ExplicitCone.unitRoot_inv_mem_shiftedDiagonalRegular line 202
45. lemma OAI.ExplicitCone.ratioQ_mem_shiftedDiagonalRegular line 206
46. lemma OAI.ExplicitCone.ratioR_mem_shiftedDiagonalRegular line 216
47. lemma OAI.ExplicitCone.sectionChart_le_shiftedDiagonalRegular line 225
48. lemma OAI.ExplicitCone.ratioQ_inv_mem_shiftedDiagonalRegular line 233
49. lemma OAI.ExplicitCone.shiftedDiagonalSectionOpen_le line 242
50. lemma OAI.ExplicitCone.sectionChart_le_shiftedDiagonalOpen line 252
51. lemma OAI.ExplicitCone.y_mem_shiftedDiagonalOpen line 254
52. lemma OAI.ExplicitCone.ratioQ_mem_shiftedDiagonalOpen line 256
53. lemma OAI.ExplicitCone.ratioR_mem_shiftedDiagonalOpen line 258
54. lemma OAI.ExplicitCone.shiftedDiagonalProduct_inv_mem line 260
55. lemma OAI.ExplicitCone.y0_inv_mem_shiftedDiagonalOpen line 262
56. lemma OAI.ExplicitCone.y1_inv_mem_shiftedDiagonalOpen line 267
57. lemma OAI.ExplicitCone.ratioQ_inv_mem_shiftedDiagonalOpen line 272
58. lemma OAI.ExplicitCone.coordinateRoot_mem_shiftedDiagonalOpen line 278
59. lemma OAI.ExplicitCone.B_mem_shiftedDiagonalOpen line 288
60. lemma OAI.ExplicitCone.remainingRoot_mem_shiftedDiagonalOpen line 292
61. lemma OAI.ExplicitCone.remainingRoot_inv_mem_shiftedDiagonalOpen line 305
62. lemma OAI.ExplicitCone.shiftedDiagonal_bDenominator_image line 319
63. lemma OAI.ExplicitCone.bDenominator_inv_mem_shiftedDiagonalOpen line 329
64. lemma OAI.ExplicitCone.S_mem_shiftedDiagonalOpen line 335
65. lemma OAI.ExplicitCone.shiftedDiagonalRegular_le_sectionOpen line 340
66. theorem OAI.ExplicitCone.shiftedDiagonalSectionOpen_eq line 355

    Source documentation

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

    theorem shiftedDiagonalSectionOpen_eq : shiftedDiagonalSectionOpen = shiftedDiagonalRegularAlgebra :=
    …

    Mentions: OAI.ExplicitCone.shiftedDiagonalSectionOpen, OAI.ExplicitCone.shiftedDiagonalRegularAlgebra

67. theorem OAI.ExplicitCone.sectionChart_shiftedDiagonalOpen_regular line 358
68. def OAI.KummerNode.coordinateRoot line 375
69. def OAI.KummerNode.shiftedCoordinate line 378
70. lemma OAI.KummerNode.shiftedCoordinate_independent line 379
71. lemma OAI.KummerNode.coordinateRoot_pow line 388
72. lemma OAI.KummerNode.coordinateRoot_independent line 394
73. def OAI.KummerNode.coordinateAlgebra line 407

    Source documentation

    The ramified coordinate part of the literal cover at (x,y)=(0,1).

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

74. abbrev OAI.KummerNode.B line 409
75. def OAI.KummerNode.planeEquiv line 411
76. instance OAI.KummerNode.(instance at line 412) line 412
77. instance OAI.KummerNode.(instance at line 414) line 414
78. def OAI.KummerNode.bRoot line 418
79. def OAI.KummerNode.planeMap line 423

    Source documentation

    The original plane map sends x to u^p and y to v^p+1; its inclusion in the original five-root field is exactly the source one.

    def planeMap : R →ₐ[ℂ] B p := MvPolynomial.aeval ![bRoot p 0 ^ p, bRoot p 1 ^ p + 1]

    Mentions: OAI.KummerNode.B, OAI.KummerNode.bRoot

80. lemma OAI.KummerNode.planeMap_comp line 424
81. instance OAI.KummerNode.(instance at line 437) line 437
82. instance OAI.KummerNode.(instance at line 438) line 438
83. instance OAI.KummerNode.(instance at line 440) line 440
84. lemma OAI.KummerNode.root_integral line 443
85. instance OAI.KummerNode.(instance at line 452) line 452
86. instance OAI.KummerNode.(instance at line 465) line 465
87. instance OAI.KummerNode.(instance at line 467) line 467
88. instance OAI.KummerNode.(instance at line 468) line 468
89. def OAI.KummerAffineExtra.coordinateIndex line 484

    Source documentation

    The other ordinary affine node, and the open part of the diagonal. Together with the node (0,1), these will cover the complement of the two actual affine triple points.

    def coordinateIndex : Fin 2 → Fin 2 → Fin 5 := ![![1, 2], ![0, 4]]

90. def OAI.KummerAffineExtra.coordinateRoot line 485
91. def OAI.KummerAffineExtra.coordinateForm line 487
92. lemma OAI.KummerAffineExtra.coordinateForm_independent line 488
93. lemma OAI.KummerAffineExtra.coordinateRoot_pow line 506
94. lemma OAI.KummerAffineExtra.coordinateRoot_independent line 509
95. def OAI.KummerAffineExtra.coordinateAlgebra line 522
96. abbrev OAI.KummerAffineExtra.B line 524
97. def OAI.KummerAffineExtra.planeEquiv line 525
98. instance OAI.KummerAffineExtra.(instance at line 526) line 526
99. instance OAI.KummerAffineExtra.(instance at line 528) line 528
100. def OAI.KummerAffineExtra.bRoot line 532
101. def OAI.KummerAffineExtra.planeMap line 534
102. lemma OAI.KummerAffineExtra.planeMap_comp line 537
103. instance OAI.KummerAffineExtra.(instance at line 558) line 558
104. instance OAI.KummerAffineExtra.(instance at line 559) line 559
105. instance OAI.KummerAffineExtra.(instance at line 561) line 561
106. instance OAI.KummerAffineExtra.(instance at line 563) line 563
107. instance OAI.KummerAffineExtra.(instance at line 573) line 573
108. instance OAI.KummerAffineExtra.(instance at line 575) line 575
109. instance OAI.KummerAffineExtra.(instance at line 577) line 577
110. def OAI.KummerAffineExtra.remainingIndex line 591
111. def OAI.KummerAffineExtra.chartDenominator line 592
112. lemma OAI.KummerAffineExtra.chartDenominator_ne_zero line 594
113. lemma OAI.KummerAffineExtra.planeMap_injective line 597
114. def OAI.KummerAffineExtra.bDenominator line 607
115. lemma OAI.KummerAffineExtra.bDenominator_ne_zero line 608
116. lemma OAI.KummerAffineExtra.bPowers_le line 610
117. def OAI.KummerAffineExtra.S line 614
118. instance OAI.KummerAffineExtra.(instance at line 615) line 615
119. instance OAI.KummerAffineExtra.(instance at line 616) line 616
120. instance OAI.KummerAffineExtra.(instance at line 619) line 619
121. instance OAI.KummerAffineExtra.(instance at line 620) line 620
122. instance OAI.KummerAffineExtra.(instance at line 622) line 622
123. instance OAI.KummerAffineExtra.(instance at line 624) line 624
124. instance OAI.KummerAffineExtra.(instance at line 626) line 626
125. lemma OAI.KummerAffineExtra.bDenominator_unit_in_L line 628
126. instance OAI.KummerAffineExtra.(instance at line 632) line 632
127. instance OAI.KummerAffineExtra.(instance at line 634) line 634
128. instance OAI.KummerAffineExtra.(instance at line 637) line 637
129. instance OAI.KummerAffineExtra.(instance at line 645) line 645
130. instance OAI.KummerAffineExtra.(instance at line 646) line 646
131. instance OAI.KummerAffineExtra.(instance at line 648) line 648
132. lemma OAI.KummerAffineExtra.remaining_dvd line 653
133. lemma OAI.KummerAffineExtra.remaining_unit line 658
134. lemma OAI.KummerAffineExtra.exponent_unit line 661
135. def OAI.KummerAffineExtra.remainingRoots line 666
136. abbrev OAI.KummerAffineExtra.chartRootAlgebra line 669
137. theorem OAI.KummerAffineExtra.chartRootAlgebra_finiteFreeEtale line 671
138. theorem OAI.KummerAffineExtra.chartRootAlgebra_regular line 684
139. def OAI.KummerAffineExtra.T line 700

     Source documentation

     The two other explicit affine opens of the original plane.

     def T := Localization.Away (chartDenominator j)

     Mentions: OAI.KummerAffineExtra.chartDenominator

140. instance OAI.KummerAffineExtra.(instance at line 701) line 701
141. instance OAI.KummerAffineExtra.(instance at line 702) line 702
142. instance OAI.KummerAffineExtra.(instance at line 704) line 704
143. instance OAI.KummerAffineExtra.coordinateMappedLocalization line 705
144. instance OAI.KummerAffineExtra.(instance at line 710) line 710
145. instance OAI.KummerAffineExtra.(instance at line 711) line 711
146. instance OAI.KummerAffineExtra.(instance at line 713) line 713
147. instance OAI.KummerAffineExtra.(instance at line 714) line 714
148. instance OAI.KummerAffineExtra.(instance at line 716) line 716
149. instance OAI.KummerAffineExtra.(instance at line 720) line 720
150. instance OAI.KummerAffineExtra.(instance at line 721) line 721
151. instance OAI.KummerAffineExtra.(instance at line 725) line 725
152. instance OAI.KummerAffineExtra.(instance at line 727) line 727
153. instance OAI.KummerAffineExtra.(instance at line 729) line 729
154. instance OAI.KummerAffineExtra.(instance at line 734) line 734
155. instance OAI.KummerAffineExtra.(instance at line 736) line 736
156. instance OAI.KummerAffineExtra.(instance at line 738) line 738
157. instance OAI.KummerAffineExtra.(instance at line 743) line 743
158. instance OAI.KummerAffineExtra.(instance at line 744) line 744
159. instance OAI.KummerAffineExtra.(instance at line 745) line 745
160. lemma OAI.KummerAffineExtra.coordinateRoot_mem_chartRootAlgebra line 747
161. lemma OAI.KummerAffineExtra.remainingRoot_mem_chartRootAlgebra line 752
162. lemma OAI.KummerAffineExtra.allRoots_mem_chartRootAlgebra line 757
163. instance OAI.KummerAffineExtra.(instance at line 771) line 771
164. theorem OAI.KummerAffineExtra.chart_normalization line 781

     Source documentation

     The entire normalization over this actual affine chart open is the regular algebra of the two ramified coordinates and three unit roots.

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

     Mentions: OAI.KummerAffineExtra.T, OAI.KummerAffineExtra.chartRootAlgebra

165. theorem OAI.KummerAffineExtra.chart_normalization_regular line 798

     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 j) (L p)) := by
     …

     Mentions: OAI.KummerAffineExtra.T

166. def OAI.KummerAffineExtra.chartRestrictionEquiv line 805

     Source documentation

     This same normalization is the actual restriction of the original normalized five-root affine cover, not a newly chosen function field.

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

     Mentions: OAI.KummerAffineExtra.T

167. theorem OAI.KummerAffineExtra.normalization_chart_regular line 812
168. theorem OAI.RegularLocalization.regular line 828

     Source documentation

     Regularity is preserved under an arbitrary localization, proved by identifying every prime local ring rather than asserting smoothness.

     theorem regular (M : Submonoid A) [IsLocalization M S] [IsRegularRing A] :
         IsRegularRing S := by
     …