OAI/AlgebraicGeometry/SurfaceCones/KummerTripleOpen.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KummerTriple.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.KummerTriple.C

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

    Source documentation

    A subalgebra of the same function field containing the original finite field generators has that field as its fraction field. The subalgebra is allowed to contain additional polynomial coordinates and inverted units.

    theorem fractionRing_of_generators (C : Subalgebra R L) (s : Set L)
    (hs : Algebra.adjoin K s = ⊤) (hC : s ⊆ C) : IsFractionRing C L := by
…
  35. instance OAI.KummerTriple.(instance at line 202) line 202
  36. instance OAI.KummerTriple.(instance at line 203) line 203
  37. def OAI.KummerTriple.T line 207

    Source documentation

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

    def T := Localization.Away chartDenominator

    Mentions: OAI.KummerTriple.chartDenominator

  38. instance OAI.KummerTriple.(instance at line 208) line 208
  39. instance OAI.KummerTriple.(instance at line 209) line 209
  40. instance OAI.KummerTriple.(instance at line 211) line 211
  41. instance OAI.KummerTriple.coordinateMappedLocalization line 212
  42. instance OAI.KummerTriple.(instance at line 217) line 217
  43. instance OAI.KummerTriple.(instance at line 218) line 218
  44. instance OAI.KummerTriple.(instance at line 220) line 220
  45. instance OAI.KummerTriple.(instance at line 221) line 221
  46. instance OAI.KummerTriple.(instance at line 223) line 223
  47. instance OAI.KummerTriple.(instance at line 227) line 227
  48. instance OAI.KummerTriple.(instance at line 228) line 228
  49. instance OAI.KummerTriple.(instance at line 232) line 232
  50. instance OAI.KummerTriple.(instance at line 234) line 234
  51. instance OAI.KummerTriple.(instance at line 236) line 236
  52. instance OAI.KummerTriple.(instance at line 241) line 241
  53. instance OAI.KummerTriple.(instance at line 243) line 243
  54. instance OAI.KummerTriple.(instance at line 245) line 245
  55. instance OAI.KummerTriple.(instance at line 250) line 250
  56. instance OAI.KummerTriple.(instance at line 251) line 251
  57. instance OAI.KummerTriple.(instance at line 252) line 252
  58. lemma OAI.KummerTriple.coordinateRoot_mem_chartRootAlgebra line 254
  59. lemma OAI.KummerTriple.remainingRoot_mem_chartRootAlgebra line 259
  60. lemma OAI.KummerTriple.allRoots_mem_chartRootAlgebra line 264
  61. instance OAI.KummerTriple.(instance at line 284) line 284

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

  62. instance OAI.KummerTriple.(instance at line 286) line 286
  63. instance OAI.KummerTriple.(instance at line 288) line 288
  64. instance OAI.KummerTriple.(instance at line 292) line 292
  65. instance OAI.KummerTriple.(instance at line 294) line 294
  66. instance OAI.KummerTriple.(instance at line 296) line 296
  67. instance OAI.KummerTriple.(instance at line 301) line 301
  68. theorem OAI.KummerTriple.chart_normalization line 310

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

  69. theorem OAI.KummerTriple.chart_normalization_regular line 327

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

  70. def OAI.KummerTriple.chartRestrictionEquiv line 334

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

  71. theorem OAI.KummerTriple.normalization_chart_regular line 341
  72. abbrev OAI.ExplicitCone.L line 358
  73. abbrev OAI.ExplicitCone.R line 359
  74. abbrev OAI.ExplicitCone.K line 360
  75. abbrev OAI.ExplicitCone.y line 361
  76. def OAI.ExplicitCone.z line 363
  77. def OAI.ExplicitCone.pairs line 365
  78. lemma OAI.ExplicitCone.y_ne_zero line 367
  79. lemma OAI.ExplicitCone.z_ne_zero line 377
  80. lemma OAI.ExplicitCone.roots_generate_over_complex line 382
  81. def OAI.ExplicitCone.sectionCoefficient line 418

    Source documentation

    The eighteen degree-one sections in the chosen rational trivialization of H. The original y-indexing is shifted by one, so z₀=1 is the sixth line.

    def sectionCoefficient (i : Fin 6 × Fin 3) : L :=
…

    Mentions: OAI.ExplicitCone.L

  82. def OAI.ExplicitCone.generator line 421
  83. abbrev OAI.ExplicitCone.algebra line 424
  84. instance OAI.ExplicitCone.finiteType line 426
  85. instance OAI.ExplicitCone.noetherian line 429
  86. lemma OAI.ExplicitCone.generators_field line 431
  87. instance OAI.ExplicitCone.fractionRing line 477
  88. def OAI.ExplicitCone.sectionRatio line 495

    Source documentation

    The literal affine coordinate functions for the degree-one section z₀z₁z₄ in the fixed H=3J−E linear system.

    def sectionRatio (i : Fin 6 × Fin 3) : L :=
…

    Mentions: OAI.ExplicitCone.L

  89. def OAI.ExplicitCone.sectionChart line 497
  90. def OAI.ExplicitCone.ratioQ line 498
  91. def OAI.ExplicitCone.ratioR line 499
  92. lemma OAI.ExplicitCone.sectionCoefficient_base line 501
  93. lemma OAI.ExplicitCone.sectionCoefficient_base_ne_zero line 504
  94. lemma OAI.ExplicitCone.sectionRatio_zero line 507
  95. lemma OAI.ExplicitCone.sectionRatio_one line 512
  96. lemma OAI.ExplicitCone.sectionRatio_two line 517
  97. lemma OAI.ExplicitCone.y_mem_sectionChart line 522
  98. lemma OAI.ExplicitCone.ratioQ_mem_sectionChart line 526
  99. lemma OAI.ExplicitCone.ratioR_mem_sectionChart line 530
  100. theorem OAI.ExplicitCone.sectionChart_eq line 537

    Source documentation

    Equality for the actual coefficient ratios, with no change of roots, polarization, field, or exponent.

    theorem sectionChart_eq : sectionChart =
    Algebra.adjoin ℂ (Set.range y ∪ {ratioQ, ratioR}) := by
…

    Mentions: OAI.ExplicitCone.sectionChart, OAI.ExplicitCone.y, OAI.ExplicitCone.ratioQ, OAI.ExplicitCone.ratioR

  101. lemma OAI.ExplicitCone.ratioQ_product line 566

    Source documentation

    The two redundant-looking coordinates record the resolved triple points, and the Fermat identity guarantees their opens cover.

    lemma ratioQ_product : y 0 * y 3 * ratioQ = y 1 * y 2 := by
…

    Mentions: OAI.ExplicitCone.y, OAI.ExplicitCone.ratioQ

  102. lemma OAI.ExplicitCone.ratioR_product line 568
  103. lemma OAI.ExplicitCone.y_power line 570
  104. lemma OAI.ExplicitCone.y_power_zero line 573
  105. lemma OAI.ExplicitCone.y_power_one line 574
  106. lemma OAI.ExplicitCone.y_power_two line 575
  107. lemma OAI.ExplicitCone.y_power_three line 579
  108. lemma OAI.ExplicitCone.y_power_four line 581
  109. lemma OAI.ExplicitCone.ratioQ_power line 583
  110. lemma OAI.ExplicitCone.ratioR_power line 588
  111. lemma OAI.ExplicitCone.ratio_fermat line 592
  112. def OAI.ExplicitCone.chartCoordinates line 602

    Source documentation

    Six functions suffice: the fifth original root is reconstructed.

    def chartCoordinates : Fin 6 → L := ![y 0, y 1, y 2, y 3, ratioQ, ratioR]

    Mentions: OAI.ExplicitCone.L, OAI.ExplicitCone.y, OAI.ExplicitCone.ratioQ, OAI.ExplicitCone.ratioR

  113. lemma OAI.ExplicitCone.chartCoordinates_mem line 603
  114. theorem OAI.ExplicitCone.sectionChart_eq_six line 612
  115. instance OAI.ExplicitCone.sectionChart_finiteType line 632
  116. instance OAI.ExplicitCone.sectionChart_fractionRing line 636
  117. lemma OAI.FieldPrincipalOpen.powers_le line 660
  118. def OAI.FieldPrincipalOpen.away line 665

    Source documentation

    A principal open as an actual subalgebra of the fixed function field.

    def away : Subalgebra k L :=
…
  119. instance OAI.FieldPrincipalOpen.(instance at line 668) line 668
  120. instance OAI.FieldPrincipalOpen.(instance at line 671) line 671
  121. lemma OAI.FieldPrincipalOpen.mem_away_iff line 675
  122. lemma OAI.FieldPrincipalOpen.le_away line 685
  123. lemma OAI.FieldPrincipalOpen.inv_mem_away line 688
  124. lemma OAI.FieldPrincipalOpen.away_le_iff line 691
  125. lemma OAI.FieldPrincipalOpen.away_eq_adjoin line 701
  126. lemma OAI.FieldPrincipalOpen.regular_away_of_eq line 711
  127. lemma OAI.KummerTriple.remainingRoot_inv_mem line 729
  128. lemma OAI.FieldPrincipalOpen.inv_left_mem line 744
  129. lemma OAI.FieldPrincipalOpen.localizationImage_mem line 751
  130. lemma OAI.ExplicitCone.ratioR_ne_zero line 768
  131. lemma OAI.ExplicitCone.ratioQ_ne_zero line 770
  132. def OAI.ExplicitCone.tripleSectionDenominator line 774
  133. lemma OAI.ExplicitCone.tripleSectionDenominator_ne_zero line 777
  134. def OAI.ExplicitCone.tripleSectionOpen line 781
  135. def OAI.ExplicitCone.tripleRegularAlgebra line 784
  136. lemma OAI.ExplicitCone.y_mem_tripleRegular line 793
  137. lemma OAI.ExplicitCone.unitRoot_inv_mem_tripleRegular line 795
  138. lemma OAI.ExplicitCone.ratioQ_mem_tripleRegular line 799
  139. lemma OAI.ExplicitCone.ratioR_mem_tripleRegular line 809
  140. lemma OAI.ExplicitCone.sectionChart_le_tripleRegular line 818
  141. lemma OAI.ExplicitCone.ratioR_inv_mem_tripleRegular line 826
  142. lemma OAI.ExplicitCone.tripleSectionOpen_le line 833
  143. lemma OAI.ExplicitCone.sectionChart_le_tripleOpen line 843
  144. lemma OAI.ExplicitCone.y_mem_tripleOpen line 845
  145. lemma OAI.ExplicitCone.ratioQ_mem_tripleOpen line 847
  146. lemma OAI.ExplicitCone.ratioR_mem_tripleOpen line 849
  147. lemma OAI.ExplicitCone.tripleProduct_inv_mem line 851
  148. lemma OAI.ExplicitCone.y2_inv_mem_tripleOpen line 853
  149. lemma OAI.ExplicitCone.y3_inv_mem_tripleOpen line 858
  150. lemma OAI.ExplicitCone.ratioR_inv_mem_tripleOpen line 863
  151. lemma OAI.ExplicitCone.coordinateRoot_mem_tripleOpen line 869
  152. lemma OAI.ExplicitCone.B_mem_tripleOpen line 881
  153. lemma OAI.ExplicitCone.remainingRoot_mem_tripleOpen line 885
  154. lemma OAI.ExplicitCone.remainingRoot_inv_mem_tripleOpen line 896
  155. lemma OAI.ExplicitCone.bDenominator_image line 908
  156. lemma OAI.ExplicitCone.bDenominator_inv_mem_tripleOpen line 918
  157. lemma OAI.ExplicitCone.S_mem_tripleOpen line 924
  158. lemma OAI.ExplicitCone.tripleRegular_le_sectionOpen line 929
  159. theorem OAI.ExplicitCone.tripleSectionOpen_eq line 944

    Source documentation

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

    theorem tripleSectionOpen_eq : tripleSectionOpen = tripleRegularAlgebra :=
…

    Mentions: OAI.ExplicitCone.tripleSectionOpen, OAI.ExplicitCone.tripleRegularAlgebra

  160. theorem OAI.ExplicitCone.sectionChart_tripleOpen_regular line 947