OAI/AlgebraicGeometry/SurfaceCones/SectionCompletion.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

The coefficient description of the completed section ring after a rational trivialization of the polarization, as in OpenAI's A Complete Local Domain without a Small Cohen–Macaulay Module, Section 2.

  1. def OAI.SectionCompletion.series line 16

    Source documentation

    The product of the graded pieces with graded Cauchy multiplication.

    def series : Subalgebra k (PowerSeries K) where
…
  2. lemma OAI.SectionCompletion.inverse_mem line 41
  3. lemma OAI.SectionCompletion.isUnit_iff_constant_ne_zero line 63
  4. lemma OAI.SectionCompletion.isLocalRing line 75
  5. lemma OAI.SectionCompletion.zero_piece_closed_inv line 86
  6. lemma OAI.SectionCompletion.maximal_mem_iff line 93
  7. lemma OAI.SectionCompletion.residue_bijective line 100
  8. def OAI.ExplicitCone.polynomialGenerator line 124
  9. abbrev OAI.ExplicitCone.polynomialAlgebra line 125
  10. instance OAI.ExplicitCone.polynomialFiniteType line 127
  11. lemma OAI.ExplicitCone.polynomialAlgebra_map line 130
  12. def OAI.ExplicitCone.polynomialEquiv line 140
  13. lemma OAI.ExplicitCone.polynomialEquiv_coe line 145
  14. instance OAI.ExplicitCone.polynomialFractionRing line 148
  15. abbrev OAI.ExplicitCone.pieces line 159
  16. abbrev OAI.ExplicitCone.completedRing line 160
  17. lemma OAI.ExplicitCone.integral_polynomial_mem_cartierChart line 162
  18. theorem OAI.ExplicitCone.normalized_coefficient_mem_sectionChart line 172

    Source documentation

    Every degree of the WHOLE normalization has regular coefficients on the original H-chart, not merely the eighteen generating sections.

    theorem normalized_coefficient_mem_sectionChart (n : ℕ) (a : L) (ha : a ∈ pieces n) :
    a / sectionCoefficient (0,0) ^ n ∈ sectionChart := by
…

    Mentions: OAI.ExplicitCone.L, OAI.ExplicitCone.pieces, OAI.ExplicitCone.sectionCoefficient, OAI.ExplicitCone.sectionChart

  19. instance OAI.KummerTriple.coordinateSmooth line 186
  20. instance OAI.KummerTriple.planeSmooth line 190
  21. instance OAI.KummerTriple.(instance at line 193) line 193
  22. instance OAI.KummerTriple.(instance at line 195) line 195
  23. instance OAI.KummerTriple.(instance at line 197) line 197
  24. instance OAI.KummerTriple.localizationSmooth line 203
  25. theorem OAI.KummerTriple.chartRootAlgebra_smooth line 206
  26. theorem OAI.ExplicitCone.tripleRegularAlgebra_smooth line 213
  27. instance OAI.KummerTripleDiagonal.coordinateSmooth line 223
  28. instance OAI.KummerTripleDiagonal.planeSmooth line 227
  29. instance OAI.KummerTripleDiagonal.(instance at line 230) line 230
  30. instance OAI.KummerTripleDiagonal.(instance at line 232) line 232
  31. instance OAI.KummerTripleDiagonal.(instance at line 234) line 234
  32. instance OAI.KummerTripleDiagonal.localizationSmooth line 240
  33. theorem OAI.KummerTripleDiagonal.chartRootAlgebra_smooth line 243
  34. theorem OAI.ExplicitCone.diagonalRegularAlgebra_smooth line 250
  35. instance OAI.KummerShifted.coordinateSmooth line 258
  36. instance OAI.KummerShifted.planeSmooth line 262
  37. instance OAI.KummerShifted.(instance at line 265) line 265
  38. instance OAI.KummerShifted.(instance at line 267) line 267
  39. instance OAI.KummerShifted.(instance at line 269) line 269
  40. instance OAI.KummerShifted.localizationSmooth line 275
  41. theorem OAI.KummerShifted.chartRootAlgebra_smooth line 278
  42. theorem OAI.ExplicitCone.shiftedRegularAlgebra_smooth line 285
  43. instance OAI.KummerShiftedDiagonal.coordinateSmooth line 293
  44. instance OAI.KummerShiftedDiagonal.planeSmooth line 297
  45. instance OAI.KummerShiftedDiagonal.(instance at line 300) line 300
  46. instance OAI.KummerShiftedDiagonal.(instance at line 302) line 302
  47. instance OAI.KummerShiftedDiagonal.(instance at line 304) line 304
  48. instance OAI.KummerShiftedDiagonal.localizationSmooth line 310
  49. theorem OAI.KummerShiftedDiagonal.chartRootAlgebra_smooth line 313
  50. theorem OAI.ExplicitCone.shiftedDiagonalRegularAlgebra_smooth line 320
  51. instance OAI.KummerAffineExtra.coordinateSmooth line 328
  52. instance OAI.KummerAffineExtra.planeSmooth line 332
  53. instance OAI.KummerAffineExtra.(instance at line 335) line 335
  54. instance OAI.KummerAffineExtra.(instance at line 337) line 337
  55. instance OAI.KummerAffineExtra.(instance at line 339) line 339
  56. instance OAI.KummerAffineExtra.localizationSmooth line 345
  57. theorem OAI.KummerAffineExtra.chartRootAlgebra_smooth line 348
  58. theorem OAI.ExplicitCone.affineRegularAlgebra_smooth line 355
  59. instance OAI.FieldPrincipalOpen.scalarTower line 363
  60. lemma OAI.FieldPrincipalOpen.away_smooth line 366
  61. lemma OAI.FieldPrincipalOpen.smooth_away_of_eq line 370
  62. lemma OAI.ExplicitCone.sectionChart_tripleOpen_smooth line 380
  63. lemma OAI.ExplicitCone.sectionChart_diagonalOpen_smooth line 386
  64. lemma OAI.ExplicitCone.sectionChart_shiftedOpen_smooth line 392
  65. lemma OAI.ExplicitCone.sectionChart_shiftedDiagonalOpen_smooth line 398
  66. lemma OAI.ExplicitCone.affinePunctured_smooth line 404
  67. lemma OAI.ExplicitCone.sectionChart_affineOpen_smooth line 407
  68. theorem OAI.ExplicitCone.sectionChart_smooth line 413
  69. def OAI.SectionCompletion.polynomials line 435

    Source documentation

    The uncompleted graded section algebra in a rational trivialization.

    def polynomials : Subalgebra k (Polynomial K) where
…
  70. lemma OAI.SectionCompletion.monomial_mem_polynomials line 459
  71. def OAI.SectionCompletion.homogeneous line 481

    Source documentation

    Degree-n polynomials inside the coefficient section algebra.

    def homogeneous (n : ℕ) : Submodule k (polynomials T) where
…

    Mentions: OAI.SectionCompletion.polynomials

  72. lemma OAI.SectionCompletion.homogeneous_eq_monomial line 493
  73. instance OAI.SectionCompletion.homogeneousGradedMonoid line 502
  74. def OAI.SectionCompletion.homogeneousPart line 510
  75. lemma OAI.SectionCompletion.homogeneousPart_coe line 514
  76. def OAI.SectionCompletion.decomposePolynomial line 519

    Source documentation

    Finite support is the actual polynomial support, not an assumption of a formal infinite homogeneous decomposition.

    noncomputable def decomposePolynomial (p : polynomials T) :
    ⨁ n, homogeneous T n :=
…

    Mentions: OAI.SectionCompletion.polynomials, OAI.SectionCompletion.homogeneous

  77. lemma OAI.SectionCompletion.decomposePolynomial_apply line 523
  78. lemma OAI.SectionCompletion.coeff_recompose line 535
  79. instance OAI.SectionCompletion.polynomialGradedRing line 550
  80. def OAI.SectionCompletion.proj line 570

    Source documentation

    The projective scheme of the actual section-coefficient algebra.

    noncomputable def proj : AlgebraicGeometry.Scheme :=
…
  81. instance OAI.SectionCompletion.degreeZeroNontrivial line 581
  82. instance OAI.SectionCompletion.degreeZeroTower line 587
  83. instance OAI.SectionCompletion.finiteType_over_degreeZero line 592
  84. instance OAI.SectionCompletion.projProper line 597

    Source documentation

    The actual Proj structure morphism is proper.

    instance projProper [Algebra.FiniteType k (polynomials T)] :
    IsProper (Proj.toSpecZero (homogeneous T)) := inferInstance

    Mentions: OAI.SectionCompletion.polynomials, OAI.SectionCompletion.homogeneous

  85. def OAI.SectionCompletion.zeroEquiv line 602

    Source documentation

    When the degree-zero coefficient piece consists of scalars, the Proj base is canonically the original scalar field.

    noncomputable def zeroEquiv
    (h0 : ∀ a ∈ T 0, ∃ c : k, algebraMap k K c = a) :
    k ≃ₐ[k] homogeneous T 0 :=
…

    Mentions: OAI.SectionCompletion.homogeneous

  86. lemma OAI.SectionCompletion.adjoin_mem_ringHom_range line 626
  87. def OAI.SectionCompletion.linearSection line 637

    Source documentation

    The homogeneous degree-one section with coefficient c.

    def linearSection (c : K) (hc : c ∈ T 1) : polynomials T :=
…

    Mentions: OAI.SectionCompletion.polynomials

  88. lemma OAI.SectionCompletion.linearSection_homogeneous line 640
  89. abbrev OAI.SectionCompletion.homogeneousChart line 645
  90. def OAI.SectionCompletion.evaluateOne line 649

    Source documentation

    Evaluation at one, used only on degree-zero homogeneous fractions.

    def evaluateOne : polynomials T →+* K :=
…

    Mentions: OAI.SectionCompletion.polynomials

  91. lemma OAI.SectionCompletion.evaluateOne_linearSection line 652
  92. def OAI.SectionCompletion.homogeneousChartMap line 658
  93. lemma OAI.SectionCompletion.homogeneousChartMap_mk line 663
  94. lemma OAI.SectionCompletion.homogeneousChartMap_injective line 676
  95. lemma OAI.SectionCompletion.scaledCoefficient_mem_range line 697
  96. lemma OAI.SectionCompletion.homogeneousChartMap_mem line 709
  97. def OAI.SectionCompletion.homogeneousChartEquiv line 718

    Source documentation

    A literal basic affine Proj chart, identified by all normalized coefficients.

    def homogeneousChartEquiv (A : Subalgebra k K)
    (hA : ∀ n a, a ∈ T n → a / c ^ n ∈ A)
    (hgen : ∀ a ∈ A, a ∈ RingHom.range (R := homogeneousChart T c hc) (homogeneousChartMap T c hc hn)) :
…

    Mentions: OAI.SectionCompletion.homogeneousChart, OAI.SectionCompletion.homogeneousChartMap

  98. instance OAI.SectionCompletion.homogeneousChartScalarAlgebra line 729
  99. lemma OAI.SectionCompletion.homogeneousChartMap_scalar line 733
  100. def OAI.SectionCompletion.homogeneousChartAlgEquiv line 750
  101. lemma OAI.SectionCompletion.adjoin_le_homogeneousChartMap_range line 758
  102. def OAI.SectionCompletion.homogeneousChartAlgEquivOfAdjoin line 768
  103. lemma OAI.SmallCM.dimension_le_of_integral line 782
  104. lemma OAI.SmallCM.dimension_ge_of_integral line 787
  105. lemma OAI.SmallCM.dimension_eq_of_integral line 798
  106. lemma OAI.SmallCM.dimension_of_trdeg line 806
  107. lemma OAI.SmallCM.trdeg_fractionRing line 824