OAI/AlgebraicGeometry/SurfaceCones/KummerSectionAffineOpen.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KummerAffineExtra.remainingRoot_inv_mem line 12
2. lemma OAI.FieldPrincipalOpen.inv_mem_of_dvd_mem line 29
3. lemma OAI.FieldPrincipalOpen.away_regular line 39
4. def OAI.ExplicitCone.affineRegularAlgebra line 46
5. lemma OAI.ExplicitCone.y_mem_affineRegular line 54
6. lemma OAI.ExplicitCone.affineUnitRoot_inv_mem line 56
7. instance OAI.ExplicitCone.affineRegular_fractionRing line 59
8. lemma OAI.ExplicitCone.affineRegular_regular line 61
9. def OAI.ExplicitCone.affineFirstRoot line 64
10. lemma OAI.ExplicitCone.affineFirstRoot_ne_zero line 65
11. def OAI.ExplicitCone.affinePuncturedRegular line 68
12. lemma OAI.ExplicitCone.affineRegular_le_punctured line 70
13. lemma OAI.ExplicitCone.y_mem_affinePunctured line 72
14. lemma OAI.ExplicitCone.y0_inv_mem_affinePunctured line 74
15. lemma OAI.ExplicitCone.y3_inv_mem_affinePunctured line 76
16. lemma OAI.ExplicitCone.affinePunctured_regular line 81
17. lemma OAI.ExplicitCone.sectionChart_le_affinePunctured line 85
18. def OAI.ExplicitCone.affineSectionIndex line 101
19. def OAI.ExplicitCone.affineSectionRoot line 102
20. def OAI.ExplicitCone.affineSectionDenominator line 104
21. lemma OAI.ExplicitCone.affineSectionDenominator_ne_zero line 105
22. def OAI.ExplicitCone.affineSectionOpen line 109
23. lemma OAI.ExplicitCone.sectionChart_le_affineOpen line 111
24. lemma OAI.ExplicitCone.y_mem_affineOpen line 113
25. lemma OAI.ExplicitCone.affineSectionRoot_inv_mem line 115
26. lemma OAI.ExplicitCone.affineSectionOpen_le line 125
27. lemma OAI.ExplicitCone.affine_B_mem_sectionOpen line 137
28. lemma OAI.ExplicitCone.affine_bDenominator_image line 142
29. lemma OAI.ExplicitCone.affine_bDenominator_inv_mem line 150
30. lemma OAI.ExplicitCone.affine_S_mem_sectionOpen line 157
31. lemma OAI.ExplicitCone.affineRegular_le_sectionOpen line 162
32. lemma OAI.ExplicitCone.affinePunctured_le_sectionOpen line 173
33. theorem OAI.ExplicitCone.affineSectionOpen_eq line 178
34. theorem OAI.ExplicitCone.sectionChart_affineOpen_regular line 180
35. theorem OAI.KummerSectionCover.cover line 196

    Source documentation

    The five literal smooth opens of the chosen H-chart cover every prime, not merely its complex closed points. This is the domain-level calculation used after reduction by an arbitrary prime.

    theorem cover {D : Type*} [CommRing D] [IsDomain D]
        (a b c d e q r : D)
        (hac : a ^ 7 - c ^ 7 = 1) (hbd : b ^ 7 - d ^ 7 = 1)
        (he : e ^ 7 = a ^ 7 - b ^ 7) (hqr : q ^ 7 - r ^ 7 = 1)
        (hp : a * d * q = b * c) :
        c * d * r ≠ 0 ∨ c * d * q ≠ 0 ∨
          a * b * r ≠ 0 ∨ a * b * q ≠ 0 ∨ a * a * d * e ≠ 0 := by
    …

36. theorem OAI.RegularOnPrincipalOpen.away_of_tensor line 239

    Source documentation

    Transfer regularity from the base-changed principal open to its canonical localization.

    theorem away_of_tensor {R T : Type*} [CommRing R] [CommRing T]
        [Algebra R A] [Algebra R T] (d : R) [IsLocalization.Away d T]
        [IsRegularRing (T ⊗[R] A)] :
        IsRegularRing (Localization.Away (algebraMap R A d)) := by
    …

37. theorem OAI.RegularOnPrincipalOpen.atPrime line 248

    Source documentation

    A prime in a regular principal open has regular local ring.

    theorem atPrime (q : Ideal A) [q.IsPrime] (f : A) (hf : f ∉ q)
        [IsRegularRing (Localization.Away f)] : IsRegularLocalRing (Localization.AtPrime q) := by
    …

38. theorem OAI.RegularOnPrincipalOpen.atPrime_of_equiv line 270

    Source documentation

    Transfer a regular prime local ring across an actual ring isomorphism.

    theorem atPrime_of_equiv {B : Type*} [CommRing B] (e : A ≃+* B)
        (q : Ideal A) [q.IsPrime]
        [IsRegularLocalRing (Localization.AtPrime (q.comap e.symm.toRingHom))] :
        IsRegularLocalRing (Localization.AtPrime q) := by
    …

39. theorem OAI.RegularOnPrincipalOpen.atPrime_of_equiv_away line 277

    Source documentation

    A principal open on an isomorphic ring suffices for local regularity.

    theorem atPrime_of_equiv_away {B : Type*} [CommRing B] (e : A ≃+* B)
        (q : Ideal A) [q.IsPrime] (f : B) (hf : e.symm f ∉ q)
        [IsRegularRing (Localization.Away f)] :
        IsRegularLocalRing (Localization.AtPrime q) := by
    …

40. def OAI.ExplicitCone.sRoot line 295

    Source documentation

    The original five roots and the two literal section ratios, as functions in the actual affine chart of the eighteen source sections.

    def sRoot (i : Fin 5) : sectionChart := ⟨y i,y_mem_sectionChart i⟩

    Mentions: OAI.ExplicitCone.sectionChart, OAI.ExplicitCone.y, OAI.ExplicitCone.y_mem_sectionChart

41. def OAI.ExplicitCone.sQ line 296
42. def OAI.ExplicitCone.sR line 297
43. lemma OAI.ExplicitCone.sRoot_fermat₀ line 298
44. lemma OAI.ExplicitCone.sRoot_fermat₁ line 303
45. lemma OAI.ExplicitCone.sRoot_diagonal line 308
46. lemma OAI.ExplicitCone.sRatio_fermat line 311
47. lemma OAI.ExplicitCone.sRatio_product line 312
48. lemma OAI.ExplicitCone.tripleSectionDenominator_eq line 314
49. lemma OAI.ExplicitCone.diagonalSectionDenominator_eq line 315
50. lemma OAI.ExplicitCone.shiftedSectionDenominator_eq line 316
51. lemma OAI.ExplicitCone.shiftedDiagonalSectionDenominator_eq line 317
52. lemma OAI.ExplicitCone.affineSectionDenominator_zero_eq line 318
53. theorem OAI.ExplicitCone.sectionChart_open_cover line 326

    Source documentation

    The exact five normalization opens cover every prime of the literal polarization chart; no closed-point restriction is imposed.

    theorem sectionChart_open_cover (P : Ideal sectionChart) [P.IsPrime] :
        tripleSectionDenominator ∉ P ∨ diagonalSectionDenominator ∉ P ∨
          shiftedSectionDenominator ∉ P ∨ shiftedDiagonalSectionDenominator ∉ P ∨
            affineSectionDenominator 0 ∉ P := by
    …

    Mentions: OAI.ExplicitCone.sectionChart, OAI.ExplicitCone.tripleSectionDenominator, OAI.ExplicitCone.diagonalSectionDenominator, OAI.ExplicitCone.shiftedSectionDenominator, OAI.ExplicitCone.shiftedDiagonalSectionDenominator, OAI.ExplicitCone.affineSectionDenominator

54. instance OAI.ExplicitCone.sectionChart_noetherian line 350
55. theorem OAI.ExplicitCone.sectionChart_regular line 355

    Source documentation

    The ENTIRE affine chart of the fixed source section z₀z₁z₄ is regular, including all primes above both resolved triple points.

    theorem sectionChart_regular : IsRegularRing sectionChart := by
    …

    Mentions: OAI.ExplicitCone.sectionChart

56. theorem OAI.NormalOnPrincipalOpen.atPrime line 377

    Source documentation

    Normality of a principal open implies normality at each prime in it.

    theorem atPrime (q : Ideal A) [q.IsPrime] (f : A) (hf : f ∉ q)
        [IsIntegrallyClosed (Localization.Away f)] :
        IsIntegrallyClosed (Localization.AtPrime q) := by
    …

57. lemma OAI.FieldPrincipalOpen.normal_away line 412
58. lemma OAI.FieldPrincipalOpen.normal_away_of_eq line 414
59. lemma OAI.ExplicitCone.sectionChart_tripleOpen_normal line 424
60. lemma OAI.ExplicitCone.sectionChart_diagonalOpen_normal line 430
61. lemma OAI.ExplicitCone.sectionChart_shiftedOpen_normal line 436
62. lemma OAI.ExplicitCone.sectionChart_shiftedDiagonalOpen_normal line 442
63. lemma OAI.ExplicitCone.affinePunctured_normal line 448
64. lemma OAI.ExplicitCone.sectionChart_affineOpen_normal line 452
65. theorem OAI.ExplicitCone.sectionChart_normal line 460

    Source documentation

    Normality is proved by descent from the actual Kummer normalizations, not assumed as an unformalized consequence of regularity.

    theorem sectionChart_normal : IsIntegrallyClosed sectionChart := by
    …

    Mentions: OAI.ExplicitCone.sectionChart

66. def OAI.PolynomialFieldChart.scale line 483
67. def OAI.PolynomialFieldChart.polynomialMap line 487
68. lemma OAI.PolynomialFieldChart.polynomialMap_C line 491
69. lemma OAI.PolynomialFieldChart.polynomialMap_X line 493
70. lemma OAI.PolynomialFieldChart.polynomialMap_injective line 495
71. def OAI.PolynomialFieldChart.chart line 501

    Source documentation

    The polynomial line chart is an actual subalgebra of the ORIGINAL cone function field, with fibre coordinate cX, not an abstract replacement.

    def chart : Subalgebra k (RatFunc L) := (polynomialMap A c hc).range

    Mentions: OAI.PolynomialFieldChart.polynomialMap

72. def OAI.PolynomialFieldChart.polynomialEquiv line 503
73. lemma OAI.PolynomialFieldChart.constant_mem line 506
74. lemma OAI.PolynomialFieldChart.variable_mem line 508
75. def OAI.PolynomialFieldChart.fiberCoordinate line 511
76. lemma OAI.PolynomialFieldChart.variable_ne_zero line 512
77. lemma OAI.PolynomialFieldChart.chart_le_iff line 518

    Source documentation

    The exact universal membership criterion for this concrete chart.

    lemma chart_le_iff (B : Subalgebra k (RatFunc L)) : chart A c hc ≤ B ↔
        (∀ a : A, RatFunc.C (a : L) ∈ B) ∧ RatFunc.C c * RatFunc.X ∈ B := by
    …

    Mentions: OAI.PolynomialFieldChart.chart

78. lemma OAI.PolynomialFieldChart.regular line 532
79. lemma OAI.PolynomialFieldChart.normal line 534
80. lemma OAI.PolynomialFieldChart.polynomialEquiv_X line 537
81. def OAI.PolynomialFieldChart.exceptionalEquiv line 542

    Source documentation

    The exceptional zero section is the ORIGINAL coefficient chart.

    def exceptionalEquiv :
        (chart A c hc ⧸ Ideal.span {fiberCoordinate A c hc}) ≃ₐ[k] A := by
    …

    Mentions: OAI.PolynomialFieldChart.chart, OAI.PolynomialFieldChart.fiberCoordinate

82. lemma OAI.PolynomialFieldChart.exceptional_prime line 556
83. lemma OAI.PolynomialFieldChart.scaled_coefficient_mem line 562

    Source documentation

    Concrete coefficient test in the original cone function field.

    lemma scaled_coefficient_mem (p : L[X])
        (hp : algebraMap L[X] (RatFunc L) p ∈ chart A c hc) (n : ℕ) :
        p.coeff n / c ^ n ∈ A := by
    …

    Mentions: OAI.PolynomialFieldChart.chart

84. lemma OAI.PolynomialFieldChart.field_generated line 577
85. instance OAI.PolynomialFieldChart.(instance at line 604) line 604
86. lemma OAI.PolynomialFieldChart.integralClosure_le line 614

    Source documentation

    A normal actual polynomial chart containing the cone also contains its WHOLE normalization in the same function field.

    lemma integralClosure_le [IsIntegrallyClosed A] (B : Subalgebra k (RatFunc L))
        (hB : B ≤ chart A c hc) :
        (integralClosure B (RatFunc L)).restrictScalars k ≤ chart A c hc := by
    …

    Mentions: OAI.PolynomialFieldChart.chart

87. def OAI.ExplicitCone.cartierChart line 636

    Source documentation

    The actual polynomial Cartier chart above the fixed section z₀z₁z₄, inside the SAME rational function field used for the source cone.

    def cartierChart : Subalgebra ℂ (RatFunc L) :=
    …

    Mentions: OAI.ExplicitCone.L

88. def OAI.ExplicitCone.cartierParameter line 640
89. lemma OAI.ExplicitCone.cartierParameter_ne_zero line 644
90. lemma OAI.ExplicitCone.constant_mem_cartierChart line 647
91. lemma OAI.ExplicitCone.ratio_mem_sectionChart line 650
92. lemma OAI.ExplicitCone.generator_eq_ratio_mul line 653
93. lemma OAI.ExplicitCone.generator_mem_cartierChart line 661
94. lemma OAI.ExplicitCone.algebra_le_cartierChart line 666
95. def OAI.ExplicitCone.normalizedCone line 673

    Source documentation

    The WHOLE integral closure of the literal section-generated cone in its function field; no smaller radical subalgebra is substituted.

    def normalizedCone : Subalgebra ℂ (RatFunc L) :=
    …

    Mentions: OAI.ExplicitCone.L

96. lemma OAI.ExplicitCone.normalizedCone_le_cartierChart line 676
97. lemma OAI.ExplicitCone.algebra_le_normalizedCone line 680
98. def OAI.ExplicitCone.normalizedBlowupChart line 687

    Source documentation

    The genuine affine blowup-chart algebra: adjoin the original eighteen section ratios to the whole normalization, all in the original function field. This definition is not an interface assuming a Cartier model.

    def normalizedBlowupChart : Subalgebra ℂ (RatFunc L) :=
    …

    Mentions: OAI.ExplicitCone.L

99. lemma OAI.ExplicitCone.generator_ratio_eq line 690
100. lemma OAI.ExplicitCone.constant_mem_normalizedBlowupChart line 697
101. theorem OAI.ExplicitCone.normalizedBlowupChart_eq line 712

     Source documentation

     Exact equality with the normal polynomial-line chart, not merely a finite birational map or equality after discarding the exceptional locus.

     theorem normalizedBlowupChart_eq : normalizedBlowupChart = cartierChart := by
     …

     Mentions: OAI.ExplicitCone.normalizedBlowupChart, OAI.ExplicitCone.cartierChart

102. def OAI.ExplicitCone.cartierPolynomialEquiv line 726
103. theorem OAI.ExplicitCone.cartierChart_regular line 729
104. theorem OAI.ExplicitCone.cartierChart_normal line 732
105. def OAI.ExplicitCone.cartierExceptionalEquiv line 736
106. lemma OAI.ExplicitCone.cartierExceptional_prime line 740
107. def OAI.GradedNormalization.scale line 751
108. lemma OAI.GradedNormalization.scale_monomial line 755
109. lemma OAI.GradedNormalization.scale_eq_sum line 764
110. lemma OAI.GradedNormalization.monomial_mem_of_scale_mem line 770
111. lemma OAI.GradedNormalization.integral_monomial line 789

     Source documentation

     Normalization is homogeneous: scaling invariance of the input algebra forces every homogeneous part of every integral polynomial to be integral.

     lemma integral_monomial (B : Subalgebra k L[X])
         (hB : ∀ a : k, ∀ p ∈ B, scale a p ∈ B)
         {p : L[X]} (hp : IsIntegral B p) (n : ℕ) :
         IsIntegral B (monomial n (p.coeff n)) := by
     …

     Mentions: OAI.GradedNormalization.scale

112. def OAI.GradedNormalization.piece line 808
113. lemma OAI.GradedNormalization.mem_piece line 812
114. instance OAI.GradedNormalization.gradedPiece line 814
115. lemma OAI.GradedNormalization.integral_constant_of_constantCoeffs line 822
116. lemma OAI.GradedNormalization.integral_mem_bot line 841
117. lemma OAI.GradedNormalization.piece_zero line 847